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.

We also construct the canonical epimorphism K.πTruncGE e : K ⟶ K.truncGE e.

TODO

• show that K.πTruncGE e : K ⟶ K.truncGE e 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'.

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) : 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.

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) : 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.

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 : ι) : X K e i ⟶ X K e j

The d field of truncGE'.

@[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 (d K e i j) (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 : X K e k ⟶ Z) : CategoryTheory.CategoryStruct.comp (d K e i j) (CategoryTheory.CategoryStruct.comp (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.

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.

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.

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.

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.

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.

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.

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') : (truncGE'Map φ e).f i = CategoryTheory.CategoryStruct.comp (K.truncGE'XIsoOpcycles e h hi).hom (CategoryTheory.CategoryStruct.comp (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') : (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'] : 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'] : truncGE'Map (CategoryTheory.CategoryStruct.comp φ φ') e = CategoryTheory.CategoryStruct.comp (truncGE'Map φ e) (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 (truncGE'Map (CategoryTheory.CategoryStruct.comp φ φ') e) h = CategoryTheory.CategoryStruct.comp (truncGE'Map φ e) (CategoryTheory.CategoryStruct.comp (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.

@[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] : 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] : truncGEMap (CategoryTheory.CategoryStruct.comp φ φ') e = CategoryTheory.CategoryStruct.comp (truncGEMap φ e) (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 (truncGEMap (CategoryTheory.CategoryStruct.comp φ φ') e) h = CategoryTheory.CategoryStruct.comp (truncGEMap φ e) (CategoryTheory.CategoryStruct.comp (truncGEMap φ' e) h)

noncomputable def HomologicalComplex.restrictionToTruncGE'.f {ι : 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 : ι) : (K.restriction e).X i ⟶ (K.truncGE' e).X i

Auxiliary definition for HomologicalComplex.restrictionToTruncGE'.

theorem HomologicalComplex.restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv {ι : 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) : f K e i = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi').hom (CategoryTheory.CategoryStruct.comp (K.pOpcycles i') (K.truncGE'XIsoOpcycles e hi' hi).inv)

theorem HomologicalComplex.restrictionToTruncGE'.f_eq_iso_hom_iso_inv {ι : 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) : f K e i = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi').hom (K.truncGE'XIso e hi' hi).inv

@[simp]

theorem HomologicalComplex.restrictionToTruncGE'.comm {ι : 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 : ι) : CategoryTheory.CategoryStruct.comp (f K e i) ((K.truncGE' e).d i j) = CategoryTheory.CategoryStruct.comp ((K.restriction e).d i j) (f K e j)

@[simp]

theorem HomologicalComplex.restrictionToTruncGE'.comm_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 : ι) {Z : C} (h : (K.truncGE' e).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (f K e i) (CategoryTheory.CategoryStruct.comp ((K.truncGE' e).d i j) h) = CategoryTheory.CategoryStruct.comp ((K.restriction e).d i j) (CategoryTheory.CategoryStruct.comp (f K e j) h)

noncomputable def HomologicalComplex.restrictionToTruncGE' {ι : 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'] : K.restriction e ⟶ K.truncGE' e

The canonical morphism K.restriction e ⟶ K.truncGE' e.

theorem HomologicalComplex.restrictionToTruncGE'_hasLift {ι : 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'] : e.HasLift (K.restrictionToTruncGE' e)

theorem HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv {ι : 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.restrictionToTruncGE' e).f i = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi').hom (CategoryTheory.CategoryStruct.comp (K.pOpcycles i') (K.truncGE'XIsoOpcycles e hi' hi).inv)

theorem HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_iso_inv {ι : 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.restrictionToTruncGE' e).f i = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi').hom (K.truncGE'XIso e hi' hi).inv

theorem HomologicalComplex.isIso_restrictionToTruncGE' {ι : 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 : ι) (hi : ¬e.BoundaryGE i) : CategoryTheory.IsIso ((K.restrictionToTruncGE' e).f i)

K.restrictionToTruncGE' e).f i is an isomorphism when ¬ e.BoundaryGE i.

@[simp]

theorem HomologicalComplex.restrictionToTruncGE'_naturality {ι : 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.CategoryStruct.comp (K.restrictionToTruncGE' e) (truncGE'Map φ e) = CategoryTheory.CategoryStruct.comp (restrictionMap φ e) (L.restrictionToTruncGE' e)

@[simp]

theorem HomologicalComplex.restrictionToTruncGE'_naturality_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 : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] {Z : HomologicalComplex C c} (h : L.truncGE' e ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.restrictionToTruncGE' e) (CategoryTheory.CategoryStruct.comp (truncGE'Map φ e) h) = CategoryTheory.CategoryStruct.comp (restrictionMap φ e) (CategoryTheory.CategoryStruct.comp (L.restrictionToTruncGE' e) h)

instance HomologicalComplex.instEpiFRestrictionToTruncGE' {ι : 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 : ι) : CategoryTheory.Epi ((K.restrictionToTruncGE' e).f i)

instance HomologicalComplex.instIsIsoFRestrictionToTruncGE'OfIsStrictlySupported {ι : 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'] [K.IsStrictlySupported e] (i : ι) : CategoryTheory.IsIso ((K.restrictionToTruncGE' e).f i)

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] : K ⟶ K.truncGE e

The canonical morphism K ⟶ K.truncGE e when e is an embedding of complex shapes which satisfy e.IsTruncGE.

instance HomologicalComplex.instEpiFπ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] (i' : ι') : CategoryTheory.Epi ((K.πTruncGE e).f i')

instance HomologicalComplex.instEpiπ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] : CategoryTheory.Epi (K.πTruncGE e)

instance HomologicalComplex.instIsStrictlySupportedTruncGE {ι : 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] : (K.truncGE e).IsStrictlySupported e

@[simp]

theorem HomologicalComplex.πTruncGE_naturality {ι : 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] : CategoryTheory.CategoryStruct.comp (K.πTruncGE e) (truncGEMap φ e) = CategoryTheory.CategoryStruct.comp φ (L.πTruncGE e)

@[simp]

theorem HomologicalComplex.πTruncGE_naturality_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 : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] {Z : HomologicalComplex C c'} (h : L.truncGE e ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.πTruncGE e) (CategoryTheory.CategoryStruct.comp (truncGEMap φ e) h) = CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (L.πTruncGE e) h)

instance HomologicalComplex.instIsStrictlySupportedTruncGE_1 {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_5, 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] {ι'' : Type u_4} {c'' : ComplexShape ι''} (e' : c''.Embedding c') [K.IsStrictlySupported e'] : (K.truncGE e).IsStrictlySupported e'

instance HomologicalComplex.instIsIsoπTruncGEOfIsStrictlySupported {ι : 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] [K.IsStrictlySupported e] : CategoryTheory.IsIso (K.πTruncGE e)

theorem HomologicalComplex.isIso_πTruncGE_iff {ι : 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] : CategoryTheory.IsIso (K.πTruncGE e) ↔ K.IsStrictlySupported e

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.

@[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

@[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

noncomputable def ComplexShape.Embedding.restrictionToTruncGE'NatTrans {ι : 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] : e.restrictionFunctor C ⟶ e.truncGE'Functor C

The natural transformation K.restriction e ⟶ K.truncGE' e for all K.

@[simp]

theorem ComplexShape.Embedding.restrictionToTruncGE'NatTrans_app {ι : 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.restrictionToTruncGE'NatTrans C).app K = K.restrictionToTruncGE' 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'.

@[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

noncomputable def ComplexShape.Embedding.πTruncGENatTrans {ι : 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.id (HomologicalComplex C c') ⟶ e.truncGEFunctor C

The natural transformation K.πTruncGE e : K ⟶ K.truncGE e for all K.

@[simp]

theorem ComplexShape.Embedding.πTruncGENatTrans_app {ι : 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.πTruncGENatTrans C).app K = K.πTruncGE e