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