The Hom-built Euler form

χ(X, Y) = Σᵢ (-1)ⁱ · dimₖ Hom(X, Y⟦i⟧), built from the long exact Hom sequences of LinearYoneda and LinearCoyoneda and the ℤ-indexed Euler-characteristic additivity of Algebra/Homology/EulerCharacteristic.

The additive pairing itself is the generic K₀.EulerForm abbreviation in this file. K₀.EulerForm.ofLinear constructs it from the Hom-built form; geometric Riemann--Roch comparisons consume that root separately.

Restrictions, stated up front

k is a division ring, not a field and not an arbitrary ring. That is exactly what the arithmetic needs and no more: rank--nullity (LinearMap.finrank_range_add_finrank_ker) lives in a section DivisionRing, and the support bounds go through LinearMap.finrank_range_le, which needs StrongRankCondition. Commutativity is used nowhere, which is why Field is not assumed — Mathlib states the same alternating-sum corollary at DivisionRing (Module.sum_neg_one_pow_finrank_eq_zero_of_exact). The generality is deliberate and currently unexercised: nothing in this repository instantiates k at a noncommutative division ring, and IsRiemannRoch lands in a ℚ-algebra, so every intended instantiation is a field. Mathlib's weaker HasRankNullity is declined — it does not supply StrongRankCondition, its universe parameter would have to be threaded against the category's morphism universe, and over a domain finrank is torsion-blind, so the resulting pairing would be additive but not the χ that Hirzebruch--Riemann--Roch compares against.

The two variables carry different hypotheses, deliberately. Additivity in the second variable needs no linearity of the shift; additivity in the first does. This is not an oversight: linearCoyoneda is covariant with source C and its shift sequence is Functor.ShiftSequence.tautological, whereas linearYoneda is contravariant and its shift sequence has to cross op, which is what requires [∀ n, (shiftFunctor C n).Linear k]. chiHom itself carries neither hypothesis; chiK₀ carries the shift-linearity one.

chiHom is junk-total, and that is deliberate

Module.finrank is 0 on a module that is not finite, and finsum is 0 on a family with infinite support. So chiHom is a plain function defined for every pair of objects in any k-linear pretriangulated category, carrying no data and no well-definedness obligation — and returning a meaningless number when HomFiniteBounded fails. Only the additivity theorems and everything downstream of them require that hypothesis. A reader must not take availability of chiHom as evidence that a category has an Euler form.

What this file does not assert

• Nothing in this file constructs a HomFiniteBounded instance; at this generality it is unprovable, see its docstring. A concrete model lives in GrothendieckGroup/HomFiniteWitness.lean (#543).
• No relation to any geometric Euler characteristic, to chi₂, or to Riemann--Roch. Those comparisons remain supplied in the numerical track.
• Serre duality's twisted χ identity is in SerreFunctor/Euler.lean; no unconditional symmetry or non-degeneracy is asserted here.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.K₀.EulerForm (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Type u

A biadditive integer-valued form on the triangulated Grothendieck group. This is an abbreviation for the canonical nested additive-homomorphism type, not a parallel one-field structure.

Equations

• CategoryTheory.Triangulated.K₀.EulerForm C = (CategoryTheory.Triangulated.K₀ C →+ CategoryTheory.Triangulated.K₀ C →+ ℤ)

def CategoryTheory.Triangulated.K₀.EulerForm.Preserves {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (E : EulerForm C) (E' : EulerForm D) (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : Prop

A triangulated functor preserves two Euler forms when its K₀ map preserves their values.

Equations

• E.Preserves E' F = ∀ (x y : CategoryTheory.Triangulated.K₀ C), (E' ((CategoryTheory.Triangulated.K₀.map F) x)) ((CategoryTheory.Triangulated.K₀.map F) y) = (E x) y

class CategoryTheory.Triangulated.HomFiniteBounded (k : Type w) [DivisionRing k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] : Prop

Hom-finiteness and finite Ext-amplitude.

Every Hom(X, Y⟦i⟧) is a finite-dimensional k-module, and for each pair only finitely many i contribute. This is the "properness" input: there is no Euler form without it.

Genuinely supplied, and unprovable at this generality. In an arbitrary k-linear pretriangulated category the Hom-spaces are arbitrary k-modules and nothing in Pretriangulated bounds them; nor need Hom(X, Y⟦i⟧) vanish for large |i|, and it does not in an unbounded derived category. It is not vacuous either: GrothendieckGroup/HomFiniteWitness.lean proves it for the bounded homotopy category of any Hom-finite k-linear category, with Kᵇ(FGModuleCat k) the named concrete model (#543).

The two fields are independent: finrank returns 0 for a non-finite module, so finiteness of the rank support says nothing about the modules themselves without finite.

On the spelling of support_finite. Given finite, this is equivalent to a vanishing bound ∃ N, ∀ |i| > N, Subsingleton (X ⟶ Y⟦i⟧) — over a division ring finrank = 0 ↔ Subsingleton for a finite module, and a finite subset of ℤ is bounded. Finite support is chosen for ergonomics, not generality: it is the form finsum_add_distrib consumes directly, and it avoids the max-of-three-bounds bookkeeping a common window forces at every triangle. It is not a weaker hypothesis and is not claimed to be.

• finite (X Y : C) (i : ℤ) : Module.Finite k (X ⟶ (shiftFunctor C i).obj Y)

  Each shifted Hom-space is a finite-dimensional k-module.

• support_finite (X Y : C) : (Function.support fun (i : ℤ) => ↑(Module.finrank k (X ⟶ (shiftFunctor C i).obj Y))).Finite

  For each pair, only finitely many shifts contribute.

noncomputable def CategoryTheory.Triangulated.chiHom (k : Type w) [DivisionRing k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (X Y : C) : ℤ

The Euler form on objects, Σᵢ (-1)ⁱ dimₖ Hom(X, Y⟦i⟧).

Junk-total: see the module docstring. Carries no hypothesis beyond the ambient k-linear pretriangulated structure.

Equations

• CategoryTheory.Triangulated.chiHom k C X Y = ∑ᶠ (i : ℤ), ↑i.negOnePow * ↑(Module.finrank k (X ⟶ (CategoryTheory.shiftFunctor C i).obj Y))

theorem CategoryTheory.Triangulated.chiHom_eq_eulerChar {k : Type w} [DivisionRing k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (X Y : C) : chiHom k C X Y = GradedObject.eulerChar (ComplexShape.up ℤ) fun (i : ℤ) => ModuleCat.of k (X ⟶ (shiftFunctor C i).obj Y)

theorem CategoryTheory.Triangulated.exact_hom_of_shortComplex_exact {k : Type w} [DivisionRing k] {S : ShortComplex (ModuleCat k)} (hS : S.Exact) : Function.Exact ⇑(ModuleCat.Hom.hom S.f) ⇑(ModuleCat.Hom.hom S.g)

A ShortComplex exact in ModuleCat k gives Function.Exact of the underlying linear maps. The bridge from the categorical homology sequence to GradedObject.eulerChar_eq_add_of_exact.

theorem CategoryTheory.Triangulated.chiHom_additive_right {k : Type w} [DivisionRing k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HomFiniteBounded k C] (X : C) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) : chiHom k C X T.obj₂ = chiHom k C X T.obj₁ + chiHom k C X T.obj₃

The Euler form is additive in its second variable.

No linearity of the shift is required: linearCoyoneda is covariant with source C, so its shift sequence is tautological. See the module docstring on the deliberate asymmetry with chiHom_additive_left.

theorem CategoryTheory.Triangulated.chiHom_additive_left {k : Type w} [DivisionRing k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HomFiniteBounded k C] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] (Y : C) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) : chiHom k C T.obj₂ Y = chiHom k C T.obj₁ Y + chiHom k C T.obj₃ Y

The Euler form is additive in its first variable.

Unlike chiHom_additive_right this needs [∀ n, (shiftFunctor C n).Linear k], because linearYoneda is contravariant and its shift sequence has to cross op. See the module docstring.

Note the wiring: triangleOpEquivalence sends X ⟶ Y ⟶ Z to op Z ⟶ op Y ⟶ op X, so the arithmetic's A family is Hom(T.obj₃, −) and its C family is Hom(T.obj₁, −) — reversed relative to the statement. The closing add_comm is that reversal and nothing else; a swapped wiring would still typecheck against the symmetric-looking goal, so it is worth saying.

instance CategoryTheory.Triangulated.isTriangleAdditive_chiHom (k : Type w) [DivisionRing k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HomFiniteBounded k C] (X : C) : IsTriangleAdditive (chiHom k C X)

Additivity in the second variable, as the class K₀.lift consumes.

noncomputable def CategoryTheory.Triangulated.chiRight (k : Type w) [DivisionRing k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HomFiniteBounded k C] (X : C) : K₀ C →+ ℤ

χ(X, −) on the Grothendieck group.

The second variable descends with no linearity-of-shift hypothesis; see the module docstring.

Equations

• CategoryTheory.Triangulated.chiRight k C X = CategoryTheory.Triangulated.K₀.lift C (CategoryTheory.Triangulated.chiHom k C X)

@[simp]

theorem CategoryTheory.Triangulated.chiRight_of (k : Type w) [DivisionRing k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HomFiniteBounded k C] (X Y : C) : (chiRight k C X) (K₀.of C Y) = chiHom k C X Y

instance CategoryTheory.Triangulated.isTriangleAdditive_chiRight (k : Type w) [DivisionRing k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HomFiniteBounded k C] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] : IsTriangleAdditive (chiRight k C)

Additivity in the first variable, now valued in K₀ C →+ ℤ. This is the step that needs the shift to be k-linear.

noncomputable def CategoryTheory.Triangulated.chiK₀ (k : Type w) [DivisionRing k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HomFiniteBounded k C] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] : K₀ C →+ K₀ C →+ ℤ

The Euler form on K₀.

χ : K₀ C →+ K₀ C →+ ℤ, biadditive by construction: the second variable descended in chiRight, the first descends here.

Equations

• CategoryTheory.Triangulated.chiK₀ k C = CategoryTheory.Triangulated.K₀.lift C (CategoryTheory.Triangulated.chiRight k C)

@[simp]

theorem CategoryTheory.Triangulated.chiK₀_of (k : Type w) [DivisionRing k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HomFiniteBounded k C] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] (X : C) : (chiK₀ k C) (K₀.of C X) = chiRight k C X

theorem CategoryTheory.Triangulated.chiK₀_of_of (k : Type w) [DivisionRing k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HomFiniteBounded k C] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] (X Y : C) : ((chiK₀ k C) (K₀.of C X)) (K₀.of C Y) = chiHom k C X Y

Not @[simp]: chiK₀_of and chiRight_of already rewrite the left-hand side, so marking this fails simpNF. Kept as the readable two-object statement, which is the form every consumer reasons with.

noncomputable def CategoryTheory.Triangulated.K₀.EulerForm.ofLinear (k : Type w) [DivisionRing k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HomFiniteBounded k C] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] : EulerForm C

Package the Hom-built Euler pairing as the generic Euler-form alias.

Equations

• CategoryTheory.Triangulated.K₀.EulerForm.ofLinear k C = CategoryTheory.Triangulated.chiK₀ k C

theorem CategoryTheory.Triangulated.K₀.EulerForm.ofLinear_eq_chiK₀ (k : Type w) [DivisionRing k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HomFiniteBounded k C] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] : ofLinear k C = chiK₀ k C

A fully faithful k-linear functor preserves χ

The classical argument, and the reason k-linearity is the hypothesis rather than additivity: a fully faithful functor matches the summands Hom(X, Y⟦i⟧) ≅ Hom(ΦX, ΦY⟦i⟧) one by one, and it is k-linearity that makes the matched summands equal as k-dimensions. An additive fully faithful functor gives a bijection of Hom-groups, which fixes finrank ℤ but not finrank k.

For the Hom-built form, full faithfulness and linearity prove the generic K₀.EulerForm.Preserves predicate below.

noncomputable def CategoryTheory.Triangulated.homLinearEquivOfFullyFaithful {k : Type w} [DivisionRing k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] (Φ : Functor C D) [Φ.Additive] [Functor.Linear k Φ] (hΦ : Φ.FullyFaithful) (X Y : C) : (X ⟶ Y) ≃ₗ[k] Φ.obj X ⟶ Φ.obj Y

The Hom-bijection of a fully faithful k-linear functor, as a k-linear equivalence.

Mathlib has Functor.FullyFaithful.homEquiv (a bare Equiv) and Functor.Linear.map_smul, but not the two combined. Written here in the ForMathlib pattern: nothing about it is specific to this development.

Equations

• CategoryTheory.Triangulated.homLinearEquivOfFullyFaithful Φ hΦ X Y = { toFun := Φ.map, map_add' := ⋯, map_smul' := ⋯, invFun := hΦ.preimage, left_inv := ⋯, right_inv := ⋯ }

noncomputable def CategoryTheory.Triangulated.homShiftLinearEquiv {k : Type w} [DivisionRing k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] (Φ : Functor C D) [Φ.Additive] [Functor.Linear k Φ] [Φ.CommShift ℤ] (hΦ : Φ.FullyFaithful) (X Y : C) (i : ℤ) : (X ⟶ (shiftFunctor C i).obj Y) ≃ₗ[k] Φ.obj X ⟶ (shiftFunctor D i).obj (Φ.obj Y)

The shifted Hom-spaces are k-linearly equivalent under a fully faithful k-linear functor commuting with the shift.

Two linear equivalences composed: full faithfulness moves Hom(X, Y⟦i⟧) to Hom(ΦX, Φ(Y⟦i⟧)), and the CommShift isomorphism moves that to Hom(ΦX, (ΦY)⟦i⟧).

This was inline inside finrank_hom_shift_map. It is named because equality of dimensions is not enough to transport HomFiniteBounded — finite-dimensionality has to travel too, and for that the equivalence itself is needed.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.finrank_hom_shift_map {k : Type w} [DivisionRing k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] (Φ : Functor C D) [Φ.Additive] [Functor.Linear k Φ] [Φ.CommShift ℤ] (hΦ : Φ.FullyFaithful) (X Y : C) (i : ℤ) : Module.finrank k (Φ.obj X ⟶ (shiftFunctor D i).obj (Φ.obj Y)) = Module.finrank k (X ⟶ (shiftFunctor C i).obj Y)

The shifted Hom-spaces have the same k-dimension. The dimension shadow of homShiftLinearEquiv.

theorem CategoryTheory.Triangulated.chiHom_map {k : Type w} [DivisionRing k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] (Φ : Functor C D) [Φ.Additive] [Functor.Linear k Φ] [Φ.CommShift ℤ] (hΦ : Φ.FullyFaithful) (X Y : C) : chiHom k D (Φ.obj X) (Φ.obj Y) = chiHom k C X Y

χ is preserved on objects.

Term by term: finrank_hom_shift_map under the finsum. No finiteness hypothesis is needed — the two families are equal pointwise, so their finsums agree whether or not either is finitely supported.

noncomputable def CategoryTheory.Triangulated.homShiftLinearEquivOfEssSurj {k : Type w} [DivisionRing k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] (Φ : Functor C D) [Φ.Additive] [Functor.Linear k Φ] [Φ.CommShift ℤ] (hΦ : Φ.FullyFaithful) [Φ.EssSurj] (Y Y' : D) (i : ℤ) : (Y ⟶ (shiftFunctor D i).obj Y') ≃ₗ[k] Φ.objPreimage Y ⟶ (shiftFunctor C i).obj (Φ.objPreimage Y')

The shifted Hom-spaces of D, carried back to C along a comparison that is also essentially surjective.

homShiftLinearEquiv only reaches objects of the form Φ.obj X. Essential surjectivity supplies, for an arbitrary Y : D, a preimage and an isomorphism Φ.obj (Φ.objPreimage Y) ≅ Y; conjugating by it — and by its shift in the second variable — extends the equivalence to every pair of objects of D.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.HomFiniteBounded.of_essSurj {k : Type w} [DivisionRing k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Linear k D] [HasShift D ℤ] (Φ : Functor C D) [Φ.Additive] [Functor.Linear k Φ] [Φ.CommShift ℤ] (hΦ : Φ.FullyFaithful) [Φ.EssSurj] [HomFiniteBounded k C] : HomFiniteBounded k D

HomFiniteBounded transports along a k-linear triangulated equivalence.

If Φ is fully faithful, k-linear, commutes with the shift and is essentially surjective — an equivalence, presented by the data an equivalence gives — then D inherits the property from C. Both fields move across homShiftLinearEquivOfEssSurj: finite-dimensionality by Module.Finite.equiv, and the support because the two dimension functions are equal, not merely both finite.

This is what finrank_hom_shift_map alone could not do. Equality of dimensions says nothing about finiteness — finrank is junk-valued at 0 on an infinite- dimensional space, so two infinite-dimensional Hom-spaces have equal finrank and neither is finite. The equivalence itself has to travel, which is why homShiftLinearEquiv was factored out of that proof.

The intended use

A concrete HomFiniteBounded category is built where the statement is elementary — Kᵇ of a Hom-finite linear category, in GrothendieckGroup/HomFiniteWitness.lean — and then moved to a category where proving it directly would be a theorem about a localization. Supplying the equivalence is the caller's problem and is not made easier here.

theorem CategoryTheory.Triangulated.chiK₀_map (k : Type w) [DivisionRing k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (D : Type u') [Category.{v', u'} D] [Preadditive D] [Linear k D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [HomFiniteBounded k C] [HomFiniteBounded k D] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] [∀ (n : ℤ), Functor.Linear k (shiftFunctor D n)] (Φ : Functor C D) [Φ.Additive] [Functor.Linear k Φ] [Φ.CommShift ℤ] [Φ.IsTriangulated] (hΦ : Φ.FullyFaithful) (x y : K₀ C) : ((chiK₀ k D) ((K₀.map Φ) x)) ((K₀.map Φ) y) = ((chiK₀ k C) x) y

χ is preserved on K₀.

The object-level statement descended in both variables. AddMonoidHom.compHom' is precomposition-as-a-homomorphism, which is what lets the outer variable be handled by K₀.hom_ext rather than by hand.

theorem CategoryTheory.Triangulated.K₀.EulerForm.ofLinear_preserves (k : Type w) [DivisionRing k] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (D : Type u') [Category.{v', u'} D] [Preadditive D] [Linear k D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [HomFiniteBounded k C] [HomFiniteBounded k D] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] [∀ (n : ℤ), Functor.Linear k (shiftFunctor D n)] (F : Functor C D) [F.Additive] [Functor.Linear k F] [F.CommShift ℤ] [F.IsTriangulated] (hF : F.FullyFaithful) : (ofLinear k C).Preserves (ofLinear k D) F

A fully faithful linear triangulated functor preserves the Hom-built Euler forms on its source and target.