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']
:
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
Instances For
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
Instances For
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
Instances For
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
Instances For
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
Instances For
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
Instances For
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
Instances For
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
Instances For
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')
:
(HomologicalComplex.truncLE'Map φ e).f i = CategoryTheory.CategoryStruct.comp (K.truncLE'XIsoCycles e h hi).hom
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.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')
:
(HomologicalComplex.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']
:
HomologicalComplex.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']
:
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)
:
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
Instances For
@[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]
:
@[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]
:
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)
:
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
Instances For
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 (HomologicalComplex.truncLE'Map φ e) (L.truncLE'ToRestriction e) = CategoryTheory.CategoryStruct.comp (K.truncLE'ToRestriction e) (HomologicalComplex.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 (HomologicalComplex.truncLE'Map φ e)
(CategoryTheory.CategoryStruct.comp (L.truncLE'ToRestriction e) h) = CategoryTheory.CategoryStruct.comp (K.truncLE'ToRestriction e)
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.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
Instances For
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 (HomologicalComplex.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 (HomologicalComplex.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.
Instances For
@[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 := ⋯ }
Instances For
@[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.
Instances For
@[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 := ⋯ }
Instances For
@[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