The canonical truncation

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

In order to achieve this, we dualize the constructions from the file Embedding.TruncGE.

noncomputable def HomologicalComplex.truncLE' {ι : 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.IsTruncLE] [∀ (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.IsTruncLE.

Equations

• K.truncLE' e = (K.op.truncGE' e.op).unop

noncomputable def HomologicalComplex.truncLE'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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : ¬e.BoundaryLE i) : (K.truncLE' e).X i ≅ K.X i'

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

Equations

• K.truncLE'XIso e hi' hi = (K.op.truncGE'XIso e.op hi' ⋯).symm.unop

noncomputable def HomologicalComplex.truncLE'XIsoCycles {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : e.BoundaryLE i) : (K.truncLE' e).X i ≅ K.cycles i'

The isomorphism (K.truncLE' e).X i ≅ K.cycles i' when e.f i = i' and e.BoundaryLE i holds.

Equations

• K.truncLE'XIsoCycles e hi' hi = (K.op.truncGE'XIsoOpcycles e.op hi' ⋯).unop.symm ≪≫ (K.opcyclesOpIso i').unop.symm

theorem HomologicalComplex.truncLE'_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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] {i j : ι} (hij : c.Rel i j) {i' j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hj : ¬e.BoundaryLE j) : (K.truncLE' e).d i j = CategoryTheory.CategoryStruct.comp (K.truncLE'XIso e hi' ⋯).hom (CategoryTheory.CategoryStruct.comp (K.d i' j') (K.truncLE'XIso e hj' hj).inv)

theorem HomologicalComplex.truncLE'_d_eq_toCycles {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] {i j : ι} (hij : c.Rel i j) {i' j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hj : e.BoundaryLE j) : (K.truncLE' e).d i j = CategoryTheory.CategoryStruct.comp (K.truncLE'XIso e hi' ⋯).hom (CategoryTheory.CategoryStruct.comp (K.toCycles i' j') (K.truncLE'XIsoCycles e hj' hj).inv)

noncomputable def HomologicalComplex.truncLE {ι : 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.IsTruncLE] [∀ (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.IsTruncLE.

Equations

• K.truncLE e = (K.op.truncGE e.op).unop

noncomputable def HomologicalComplex.truncLEIso {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] : K.truncLE e ≅ (K.truncLE' e).extend e

The canonical isomorphism K.truncLE e ≅ (K.truncLE' e).extend e.

Equations

• K.truncLEIso e = (HomologicalComplex.unopFunctor C c'.symm).mapIso ((K.truncLE' e).extendOpIso e).symm.op

noncomputable def HomologicalComplex.truncLEXIso {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : ¬e.BoundaryLE i) : (K.truncLE e).X i' ≅ K.X i'

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

Equations

• K.truncLEXIso e hi' hi = (K.op.truncGEXIso e.op hi' ⋯).unop.symm

noncomputable def HomologicalComplex.truncLEXIsoCycles {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : e.BoundaryLE i) : (K.truncLE e).X i' ≅ K.cycles i'

The isomorphism (K.truncLE e).X i' ≅ K.cycles i' when e.f i = i' and e.BoundaryLE i holds.

Equations

• K.truncLEXIsoCycles e hi' hi = (K.op.truncGEXIsoOpcycles e.op hi' ⋯).unop.symm ≪≫ (K.opcyclesOpIso i').unop.symm

noncomputable def HomologicalComplex.truncLE'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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] : K.truncLE' e ⟶ L.truncLE' e

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

Equations

• HomologicalComplex.truncLE'Map φ e = (HomologicalComplex.unopFunctor C c.symm).map (HomologicalComplex.truncGE'Map ((HomologicalComplex.opFunctor C c').map φ.op) e.op).op

theorem HomologicalComplex.truncLE'Map_f_eq_cyclesMap {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] {i : ι} (hi : e.BoundaryLE i) {i' : ι'} (h : e.f i = i') : (truncLE'Map φ e).f i = CategoryTheory.CategoryStruct.comp (K.truncLE'XIsoCycles e h hi).hom (CategoryTheory.CategoryStruct.comp (cyclesMap φ i') (L.truncLE'XIsoCycles e h hi).inv)

theorem HomologicalComplex.truncLE'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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] {i : ι} (hi : ¬e.BoundaryLE i) {i' : ι'} (h : e.f i = i') : (truncLE'Map φ e).f i = CategoryTheory.CategoryStruct.comp (K.truncLE'XIso e h hi).hom (CategoryTheory.CategoryStruct.comp (φ.f i') (L.truncLE'XIso e h hi).inv)

@[simp]

theorem HomologicalComplex.truncLE'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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] : truncLE'Map (CategoryTheory.CategoryStruct.id K) e = CategoryTheory.CategoryStruct.id (K.truncLE' e)

@[simp]

theorem HomologicalComplex.truncLE'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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] [∀ (i' : ι'), M.HasHomology i'] : truncLE'Map (CategoryTheory.CategoryStruct.comp φ φ') e = CategoryTheory.CategoryStruct.comp (truncLE'Map φ e) (truncLE'Map φ' e)

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

noncomputable def HomologicalComplex.truncLEMap {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] : K.truncLE e ⟶ L.truncLE e

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

Equations

• HomologicalComplex.truncLEMap φ e = (HomologicalComplex.unopFunctor C c'.symm).map (HomologicalComplex.truncGEMap ((HomologicalComplex.opFunctor C c').map φ.op) e.op).op

@[simp]

theorem HomologicalComplex.truncLEMap_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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] : truncLEMap (CategoryTheory.CategoryStruct.id K) e = CategoryTheory.CategoryStruct.id (K.truncLE e)

@[simp]

theorem HomologicalComplex.truncLEMap_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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] [∀ (i' : ι'), M.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] : truncLEMap (CategoryTheory.CategoryStruct.comp φ φ') e = CategoryTheory.CategoryStruct.comp (truncLEMap φ e) (truncLEMap φ' e)

theorem HomologicalComplex.truncLEMap_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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] [∀ (i' : ι'), M.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] {Z : HomologicalComplex C c'} (h : M.truncLE e ⟶ Z) : CategoryTheory.CategoryStruct.comp (truncLEMap (CategoryTheory.CategoryStruct.comp φ φ') e) h = CategoryTheory.CategoryStruct.comp (truncLEMap φ e) (CategoryTheory.CategoryStruct.comp (truncLEMap φ' e) h)

noncomputable def HomologicalComplex.truncLE'ToRestriction {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] : K.truncLE' e ⟶ K.restriction e

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

Equations

• K.truncLE'ToRestriction e = (HomologicalComplex.unopFunctor C c.symm).map (K.op.restrictionToTruncGE' e.op).op

theorem HomologicalComplex.isIso_truncLE'ToRestriction {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] (i : ι) (hi : ¬e.BoundaryLE i) : CategoryTheory.IsIso ((K.truncLE'ToRestriction e).f i)

(K.truncLE'ToRestriction e).f i is an isomorphism when ¬ e.BoundaryLE i.

@[simp]

theorem HomologicalComplex.truncLE'ToRestriction_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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] : CategoryTheory.CategoryStruct.comp (truncLE'Map φ e) (L.truncLE'ToRestriction e) = CategoryTheory.CategoryStruct.comp (K.truncLE'ToRestriction e) (restrictionMap φ e)

@[simp]

theorem HomologicalComplex.truncLE'ToRestriction_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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] {Z : HomologicalComplex C c} (h : L.restriction e ⟶ Z) : CategoryTheory.CategoryStruct.comp (truncLE'Map φ e) (CategoryTheory.CategoryStruct.comp (L.truncLE'ToRestriction e) h) = CategoryTheory.CategoryStruct.comp (K.truncLE'ToRestriction e) (CategoryTheory.CategoryStruct.comp (restrictionMap φ e) h)

instance HomologicalComplex.instMonoFTruncLE'ToRestriction {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] (i : ι) : CategoryTheory.Mono ((K.truncLE'ToRestriction e).f i)

instance HomologicalComplex.instIsIsoFTruncLE'ToRestrictionOfIsStrictlySupported {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [K.IsStrictlySupported e] (i : ι) : CategoryTheory.IsIso ((K.truncLE'ToRestriction e).f i)

noncomputable def HomologicalComplex.ιTruncLE {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] : K.truncLE e ⟶ K

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

Equations

• K.ιTruncLE e = (HomologicalComplex.unopFunctor C c'.symm).map (K.op.πTruncGE e.op).op

instance HomologicalComplex.instMonoFιTruncLE {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] (i' : ι') : CategoryTheory.Mono ((K.ιTruncLE e).f i')

instance HomologicalComplex.instMonoιTruncLE {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Mono (K.ιTruncLE e)

instance HomologicalComplex.instIsStrictlySupportedTruncLE {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] : (K.truncLE e).IsStrictlySupported e

@[simp]

theorem HomologicalComplex.ιTruncLE_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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.CategoryStruct.comp (truncLEMap φ e) (L.ιTruncLE e) = CategoryTheory.CategoryStruct.comp (K.ιTruncLE e) φ

@[simp]

theorem HomologicalComplex.ιTruncLE_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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [∀ (i' : ι'), L.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] {Z : HomologicalComplex C c'} (h : L ⟶ Z) : CategoryTheory.CategoryStruct.comp (truncLEMap φ e) (CategoryTheory.CategoryStruct.comp (L.ιTruncLE e) h) = CategoryTheory.CategoryStruct.comp (K.ιTruncLE e) (CategoryTheory.CategoryStruct.comp φ h)

instance HomologicalComplex.instIsStrictlySupportedTruncLE_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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] {ι'' : Type u_4} {c'' : ComplexShape ι''} (e' : c''.Embedding c') [K.IsStrictlySupported e'] : (K.truncLE e).IsStrictlySupported e'

instance HomologicalComplex.instIsIsoιTruncLEOfIsStrictlySupported {ι : 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.IsTruncLE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] [K.IsStrictlySupported e] : CategoryTheory.IsIso (K.ιTruncLE e)

noncomputable def ComplexShape.Embedding.truncLE'Functor {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE] (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.IsTruncLE, 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.truncLE'Functor_obj {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE] (C : Type u_4) [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c') : (e.truncLE'Functor C).obj K = K.truncLE' e

@[simp]

theorem ComplexShape.Embedding.truncLE'Functor_map {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE] (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.truncLE'Functor C).map φ = HomologicalComplex.truncLE'Map φ e

noncomputable def ComplexShape.Embedding.truncLE'ToRestrictionNatTrans {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE] (C : Type u_4) [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] : e.truncLE'Functor C ⟶ e.restrictionFunctor C

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

Equations

• e.truncLE'ToRestrictionNatTrans C = { app := fun (K : HomologicalComplex C c') => K.truncLE'ToRestriction e, naturality := ⋯ }

@[simp]

theorem ComplexShape.Embedding.truncLE'ToRestrictionNatTrans_app {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE] (C : Type u_4) [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c') : (e.truncLE'ToRestrictionNatTrans C).app K = K.truncLE'ToRestriction e

noncomputable def ComplexShape.Embedding.truncLEFunctor {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE] (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.IsTruncLE, 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.truncLEFunctor_obj {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE] (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.truncLEFunctor C).obj K = K.truncLE e

@[simp]

theorem ComplexShape.Embedding.truncLEFunctor_map {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE] (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.truncLEFunctor C).map φ = HomologicalComplex.truncLEMap φ e

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

The natural transformation K.ιTruncLE e : K.truncLE e ⟶ K for all K.

Equations

• e.ιTruncLENatTrans C = { app := fun (K : HomologicalComplex C c') => K.ιTruncLE e, naturality := ⋯ }

@[simp]

theorem ComplexShape.Embedding.ιTruncLENatTrans_app {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE] (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.ιTruncLENatTrans C).app K = K.ιTruncLE e