The canonical truncation

Given an embedding e : Embedding c c' of complex shapes which satisfies e.IsTruncGE and K : HomologicalComplex C c', we define K.truncGE' e : HomologicalComplex C c and K.truncGE e : HomologicalComplex C c' which are the canonical truncations of K relative to e.

For example, if e is the embedding embeddingUpIntGE p of ComplexShape.up ℕ in ComplexShape.up ℤ which sends n : ℕ to p + n and K : CochainComplex C ℤ, then K.truncGE' e : CochainComplex C ℕ is the following complex:

Q ⟶ K.X (p + 1) ⟶ K.X (p + 2) ⟶ K.X (p + 3) ⟶ ...

where in degree 0, the object Q identifies to the cokernel of K.X (p - 1) ⟶ K.X p (this is K.opcycles p). Then, the cochain complex K.truncGE e is indexed by ℤ, and has the following shape:

... ⟶ 0 ⟶ 0 ⟶ 0 ⟶ Q ⟶ K.X (p + 1) ⟶ K.X (p + 2) ⟶ K.X (p + 3) ⟶ ...

where Q is in degree p.

TODO

• construct a morphism K.πTruncGE e : K ⟶ K.truncGE e and show that it induces an isomorphism in homology in degrees in the image of e.f.

noncomputable def HomologicalComplex.truncGE'.X {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [∀ (i' : ι'), K.HasHomology i'] (i : ι) : C

The X field of truncGE'.

Equations

• HomologicalComplex.truncGE'.X K e i = if e.BoundaryGE i then K.opcycles (e.f i) else K.X (e.f i)

noncomputable def HomologicalComplex.truncGE'.XIsoOpcycles {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [∀ (i' : ι'), K.HasHomology i'] {i : ι} (hi : e.BoundaryGE i) : HomologicalComplex.truncGE'.X K e i ≅ K.opcycles (e.f i)

The isomorphism truncGE'.X K e i ≅ K.opcycles (e.f i) when e.BoundaryGE i holds.

Equations

• HomologicalComplex.truncGE'.XIsoOpcycles K e hi = CategoryTheory.eqToIso ⋯

noncomputable def HomologicalComplex.truncGE'.XIso {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [∀ (i' : ι'), K.HasHomology i'] {i : ι} (hi : ¬e.BoundaryGE i) : HomologicalComplex.truncGE'.X K e i ≅ K.X (e.f i)

The isomorphism truncGE'.X K e i ≅ K.X (e.f i) when e.BoundaryGE i does not hold.

Equations

• HomologicalComplex.truncGE'.XIso K e hi = CategoryTheory.eqToIso ⋯

noncomputable def HomologicalComplex.truncGE'.d {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] (i j : ι) : HomologicalComplex.truncGE'.X K e i ⟶ HomologicalComplex.truncGE'.X K e j

The d field of truncGE'.

Equations

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

@[simp]

theorem HomologicalComplex.truncGE'.d_comp_d {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] (i j k : ι) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'.d K e i j) (HomologicalComplex.truncGE'.d K e j k) = 0

@[simp]

theorem HomologicalComplex.truncGE'.d_comp_d_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] (i j k : ι) {Z : C} (h : HomologicalComplex.truncGE'.X K e k ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'.d K e i j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'.d K e j k) h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def HomologicalComplex.truncGE' {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] : HomologicalComplex C c

The canonical truncation of a homological complex relative to an embedding of complex shapes e which satisfies e.IsTruncGE.

Equations

• K.truncGE' e = { X := HomologicalComplex.truncGE'.X K e, d := HomologicalComplex.truncGE'.d K e, shape := ⋯, d_comp_d' := ⋯ }

noncomputable def HomologicalComplex.truncGE'XIso {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : ¬e.BoundaryGE i) : (K.truncGE' e).X i ≅ K.X i'

The isomorphism (K.truncGE' e).X i ≅ K.X i' when e.f i = i' and e.BoundaryGE i does not hold.

Equations

• K.truncGE'XIso e hi' hi = HomologicalComplex.truncGE'.XIso K e hi ≪≫ CategoryTheory.eqToIso ⋯

noncomputable def HomologicalComplex.truncGE'XIsoOpcycles {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : e.BoundaryGE i) : (K.truncGE' e).X i ≅ K.opcycles i'

The isomorphism (K.truncGE' e).X i ≅ K.opcycles i' when e.f i = i' and e.BoundaryGE i holds.

Equations

• K.truncGE'XIsoOpcycles e hi' hi = HomologicalComplex.truncGE'.XIsoOpcycles K e hi ≪≫ CategoryTheory.eqToIso ⋯

theorem HomologicalComplex.truncGE'_d_eq {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] {i j : ι} (hij : c.Rel i j) {i' j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hi : ¬e.BoundaryGE i) : (K.truncGE' e).d i j = CategoryTheory.CategoryStruct.comp (K.truncGE'XIso e hi' hi).hom (CategoryTheory.CategoryStruct.comp (K.d i' j') (K.truncGE'XIso e hj' ⋯).inv)

theorem HomologicalComplex.truncGE'_d_eq_fromOpcycles {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] {i j : ι} (hij : c.Rel i j) {i' j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hi : e.BoundaryGE i) : (K.truncGE' e).d i j = CategoryTheory.CategoryStruct.comp (K.truncGE'XIsoOpcycles e hi' hi).hom (CategoryTheory.CategoryStruct.comp (K.fromOpcycles i' j') (K.truncGE'XIso e hj' ⋯).inv)

noncomputable def HomologicalComplex.truncGE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] : HomologicalComplex C c'

The canonical truncation of a homological complex relative to an embedding of complex shapes e which satisfies e.IsTruncGE.

Equations

• K.truncGE e = (K.truncGE' e).extend e

noncomputable def HomologicalComplex.truncGEXIso {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : ¬e.BoundaryGE i) : (K.truncGE e).X i' ≅ K.X i'

The isomorphism (K.truncGE e).X i' ≅ K.X i' when e.f i = i' and e.BoundaryGE i does not hold.

Equations

• K.truncGEXIso e hi' hi = (K.truncGE' e).extendXIso e hi' ≪≫ K.truncGE'XIso e hi' hi

noncomputable def HomologicalComplex.truncGEXIsoOpcycles {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : e.BoundaryGE i) : (K.truncGE e).X i' ≅ K.opcycles i'

The isomorphism (K.truncGE e).X i' ≅ K.opcycles i' when e.f i = i' and e.BoundaryGE i holds.

Equations

• K.truncGEXIsoOpcycles e hi' hi = (K.truncGE' e).extendXIso e hi' ≪≫ K.truncGE'XIsoOpcycles e hi' hi

noncomputable def HomologicalComplex.truncGE'Map {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] : K.truncGE' e ⟶ L.truncGE' e

The morphism K.truncGE' e ⟶ L.truncGE' e induced by a morphism K ⟶ L.

Equations

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

theorem HomologicalComplex.truncGE'Map_f_eq_opcyclesMap {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] {i : ι} (hi : e.BoundaryGE i) {i' : ι'} (h : e.f i = i') : (HomologicalComplex.truncGE'Map φ e).f i = CategoryTheory.CategoryStruct.comp (K.truncGE'XIsoOpcycles e h hi).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i') (L.truncGE'XIsoOpcycles e h hi).inv)

theorem HomologicalComplex.truncGE'Map_f_eq {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] {i : ι} (hi : ¬e.BoundaryGE i) {i' : ι'} (h : e.f i = i') : (HomologicalComplex.truncGE'Map φ e).f i = CategoryTheory.CategoryStruct.comp (K.truncGE'XIso e h hi).hom (CategoryTheory.CategoryStruct.comp (φ.f i') (L.truncGE'XIso e h hi).inv)

@[simp]

theorem HomologicalComplex.truncGE'Map_id {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] : HomologicalComplex.truncGE'Map (CategoryTheory.CategoryStruct.id K) e = CategoryTheory.CategoryStruct.id (K.truncGE' e)

@[simp]

theorem HomologicalComplex.truncGE'Map_comp {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] [∀ (i' : ι'), M.HasHomology i'] : HomologicalComplex.truncGE'Map (CategoryTheory.CategoryStruct.comp φ φ') e = CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'Map φ e) (HomologicalComplex.truncGE'Map φ' e)

theorem HomologicalComplex.truncGE'Map_comp_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] [∀ (i' : ι'), M.HasHomology i'] {Z : HomologicalComplex C c} (h : M.truncGE' e ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'Map (CategoryTheory.CategoryStruct.comp φ φ') e) h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'Map φ e) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'Map φ' e) h)

noncomputable def HomologicalComplex.truncGEMap {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] : K.truncGE e ⟶ L.truncGE e

The morphism K.truncGE e ⟶ L.truncGE e induced by a morphism K ⟶ L.

Equations

• HomologicalComplex.truncGEMap φ e = (e.extendFunctor C).map (HomologicalComplex.truncGE'Map φ e)

@[simp]

theorem HomologicalComplex.truncGEMap_id {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] : HomologicalComplex.truncGEMap (CategoryTheory.CategoryStruct.id K) e = CategoryTheory.CategoryStruct.id (K.truncGE e)

@[simp]

theorem HomologicalComplex.truncGEMap_comp {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] [∀ (i' : ι'), M.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] : HomologicalComplex.truncGEMap (CategoryTheory.CategoryStruct.comp φ φ') e = CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGEMap φ e) (HomologicalComplex.truncGEMap φ' e)

theorem HomologicalComplex.truncGEMap_comp_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] [∀ (i' : ι'), M.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] {Z : HomologicalComplex C c'} (h : M.truncGE e ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGEMap (CategoryTheory.CategoryStruct.comp φ φ') e) h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGEMap φ e) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGEMap φ' e) h)

noncomputable def ComplexShape.Embedding.truncGE'Functor {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncGE] (C : Type u_4) [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] : CategoryTheory.Functor (HomologicalComplex C c') (HomologicalComplex C c)

Given an embedding e : Embedding c c' of complex shapes which satisfy e.IsTruncGE, this is the (canonical) truncation functor HomologicalComplex C c' ⥤ HomologicalComplex C c.

Equations

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

@[simp]

theorem ComplexShape.Embedding.truncGE'Functor_map {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncGE] (C : Type u_4) [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] {X✝ Y✝ : HomologicalComplex C c'} (φ : X✝ ⟶ Y✝) : (e.truncGE'Functor C).map φ = HomologicalComplex.truncGE'Map φ e

@[simp]

theorem ComplexShape.Embedding.truncGE'Functor_obj {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncGE] (C : Type u_4) [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c') : (e.truncGE'Functor C).obj K = K.truncGE' e

noncomputable def ComplexShape.Embedding.truncGEFunctor {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncGE] (C : Type u_4) [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.CategoryWithHomology C] : CategoryTheory.Functor (HomologicalComplex C c') (HomologicalComplex C c')

Given an embedding e : Embedding c c' of complex shapes which satisfy e.IsTruncGE, this is the (canonical) truncation functor HomologicalComplex C c' ⥤ HomologicalComplex C c'.

Equations

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

@[simp]

theorem ComplexShape.Embedding.truncGEFunctor_map {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncGE] (C : Type u_4) [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.CategoryWithHomology C] {X✝ Y✝ : HomologicalComplex C c'} (φ : X✝ ⟶ Y✝) : (e.truncGEFunctor C).map φ = HomologicalComplex.truncGEMap φ e

@[simp]

theorem ComplexShape.Embedding.truncGEFunctor_obj {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncGE] (C : Type u_4) [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c') : (e.truncGEFunctor C).obj K = K.truncGE e