The stupid truncation of homological complexes

Given an embedding e : c.Embedding c' of complex shapes, we define a functor stupidTruncFunctor : HomologicalComplex C c' ⥤ HomologicalComplex C c' which sends K to K.stupidTrunc e which is defined as (K.restriction e).extend e.

@[implicit_reducible]

noncomputable def HomologicalComplex.stupidTrunc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] : HomologicalComplex C c'

The stupid truncation of a complex K : HomologicalComplex C c' relatively to an embedding e : c.Embedding c' of complex shapes.

Equations

• K.stupidTrunc e = (K.restriction e).extend e

instance HomologicalComplex.instIsStrictlySupportedStupidTrunc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] : (K.stupidTrunc e).IsStrictlySupported e

noncomputable def HomologicalComplex.stupidTruncXIso {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] {i : ι} {i' : ι'} (hi' : e.f i = i') : (K.stupidTrunc e).X i' ≅ K.X i'

The isomorphism (K.stupidTrunc e).X i' ≅ K.X i' when i is in the image of e.f.

Equations

• K.stupidTruncXIso e hi' = (K.restriction e).extendXIso e hi' ≪≫ CategoryTheory.eqToIso ⋯

theorem HomologicalComplex.congr_stupidTruncXIso {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] {i₁ i₂ : ι} {i' : ι'} (hi₁ : e.f i₁ = i') (hi₂ : e.f i₂ = i') : K.stupidTruncXIso e hi₁ = K.stupidTruncXIso e hi₂

theorem HomologicalComplex.stupidTruncXIso_rfl {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] (i : ι) : K.stupidTruncXIso e ⋯ = (K.restriction e).extendXIso e ⋯

theorem HomologicalComplex.isZero_stupidTrunc_X {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i') : CategoryTheory.Limits.IsZero ((K.stupidTrunc e).X i')

instance HomologicalComplex.instIsStrictlySupportedStupidTrunc_1 {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] {ι'' : Type u_4} {c'' : ComplexShape ι''} (e' : c''.Embedding c') [K.IsStrictlySupported e'] : (K.stupidTrunc e).IsStrictlySupported e'

theorem HomologicalComplex.IsStrictlySupportedOutside.stupidTrunc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {ι'' : Type u_4} {c'' : ComplexShape ι''} {e' : c''.Embedding c'} (hK : K.IsStrictlySupportedOutside e') (e : c.Embedding c') [e.IsRelIff] : (K.stupidTrunc e).IsStrictlySupportedOutside e'

theorem HomologicalComplex.isZero_stupidTrunc_iff {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] : CategoryTheory.Limits.IsZero (K.stupidTrunc e) ↔ K.IsStrictlySupportedOutside e

noncomputable def HomologicalComplex.stupidTruncMap {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsRelIff] : K.stupidTrunc e ⟶ L.stupidTrunc e

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

Equations

• HomologicalComplex.stupidTruncMap φ e = HomologicalComplex.extendMap (HomologicalComplex.restrictionMap φ e) e

@[simp]

theorem HomologicalComplex.stupidTruncMap_id {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] : stupidTruncMap (CategoryTheory.CategoryStruct.id K) e = CategoryTheory.CategoryStruct.id (K.stupidTrunc e)

@[simp]

theorem HomologicalComplex.stupidTruncMap_comp {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [e.IsRelIff] : stupidTruncMap (CategoryTheory.CategoryStruct.comp φ φ') e = CategoryTheory.CategoryStruct.comp (stupidTruncMap φ e) (stupidTruncMap φ' e)

theorem HomologicalComplex.stupidTruncMap_comp_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [e.IsRelIff] {Z : HomologicalComplex C c'} (h : M.stupidTrunc e ⟶ Z) : CategoryTheory.CategoryStruct.comp (stupidTruncMap (CategoryTheory.CategoryStruct.comp φ φ') e) h = CategoryTheory.CategoryStruct.comp (stupidTruncMap φ e) (CategoryTheory.CategoryStruct.comp (stupidTruncMap φ' e) h)

@[simp]

theorem HomologicalComplex.stupidTruncMap_stupidTruncXIso_hom {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsRelIff] {i : ι} {i' : ι'} (hi : e.f i = i') : CategoryTheory.CategoryStruct.comp ((stupidTruncMap φ e).f i') (L.stupidTruncXIso e hi).hom = CategoryTheory.CategoryStruct.comp (K.stupidTruncXIso e hi).hom (φ.f i')

@[simp]

theorem HomologicalComplex.stupidTruncMap_stupidTruncXIso_hom_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsRelIff] {i : ι} {i' : ι'} (hi : e.f i = i') {Z : C} (h : L.X i' ⟶ Z) : CategoryTheory.CategoryStruct.comp ((stupidTruncMap φ e).f i') (CategoryTheory.CategoryStruct.comp (L.stupidTruncXIso e hi).hom h) = CategoryTheory.CategoryStruct.comp (K.stupidTruncXIso e hi).hom (CategoryTheory.CategoryStruct.comp (φ.f i') h)

noncomputable def HomologicalComplex.ιStupidTruncf {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] (i' : ι') : (K.stupidTrunc e).X i' ⟶ K.X i'

Auxiliary definition for ιStupidTrunc.

Equations

• K.ιStupidTruncf e i' = if h : ∃ (i : ι), e.f i = i' then (K.stupidTruncXIso e ⋯).hom else 0

theorem HomologicalComplex.ιStupidTruncf_eq {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] (i : ι) : K.ιStupidTruncf e (e.f i) = ((K.restriction e).extendXIso e ⋯).hom

theorem HomologicalComplex.ιStupidTruncf'_eq {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] {i : ι} {i' : ι'} (h : e.f i = i') : K.ιStupidTruncf e i' = CategoryTheory.CategoryStruct.comp ((K.restriction e).extendXIso e h).hom (K.restrictionXIso e h).hom

noncomputable def HomologicalComplex.ιStupidTrunc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] : K.stupidTrunc e ⟶ K

The monomorphism K.stupidTrunc e ⟶ K when the embedding e of complex shapes satisfies e.IsTruncGE.

Equations

• K.ιStupidTrunc e = { f := K.ιStupidTruncf e, comm' := ⋯ }

theorem HomologicalComplex.ιStupidTrunc_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] (i' : ι') : (K.ιStupidTrunc e).f i' = K.ιStupidTruncf e i'

theorem HomologicalComplex.isIso_ιStupidTrunc_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] {i' : ι'} {i : ι} (h : e.f i = i') : CategoryTheory.IsIso ((K.ιStupidTrunc e).f i')

instance HomologicalComplex.instIsIsoFιStupidTruncF {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] (i : ι) : CategoryTheory.IsIso ((K.ιStupidTrunc e).f (e.f i))

instance HomologicalComplex.instMonoFιStupidTrunc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] (i' : ι') : CategoryTheory.Mono ((K.ιStupidTrunc e).f i')

instance HomologicalComplex.instMonoιStupidTrunc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] : CategoryTheory.Mono (K.ιStupidTrunc e)

theorem HomologicalComplex.isIso_ιStupidTrunc_iff {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] : CategoryTheory.IsIso (K.ιStupidTrunc e) ↔ K.IsStrictlySupported e

instance HomologicalComplex.instIsIsoιStupidTruncOfIsStrictlySupported {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncGE] [K.IsStrictlySupported e] : CategoryTheory.IsIso (K.ιStupidTrunc e)

@[simp]

theorem HomologicalComplex.ιStupidTrunc_naturality {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncGE] : CategoryTheory.CategoryStruct.comp (stupidTruncMap φ e) (L.ιStupidTrunc e) = CategoryTheory.CategoryStruct.comp (K.ιStupidTrunc e) φ

@[simp]

theorem HomologicalComplex.ιStupidTrunc_naturality_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncGE] {Z : HomologicalComplex C c'} (h : L ⟶ Z) : CategoryTheory.CategoryStruct.comp (stupidTruncMap φ e) (CategoryTheory.CategoryStruct.comp (L.ιStupidTrunc e) h) = CategoryTheory.CategoryStruct.comp (K.ιStupidTrunc e) (CategoryTheory.CategoryStruct.comp φ h)

@[simp]

theorem HomologicalComplex.ιStupidTrunc_f_naturality {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncGE] (i' : ι') : CategoryTheory.CategoryStruct.comp ((stupidTruncMap φ e).f i') ((L.ιStupidTrunc e).f i') = CategoryTheory.CategoryStruct.comp ((K.ιStupidTrunc e).f i') (φ.f i')

@[simp]

theorem HomologicalComplex.ιStupidTrunc_f_naturality_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncGE] (i' : ι') {Z : C} (h : L.X i' ⟶ Z) : CategoryTheory.CategoryStruct.comp ((stupidTruncMap φ e).f i') (CategoryTheory.CategoryStruct.comp ((L.ιStupidTrunc e).f i') h) = CategoryTheory.CategoryStruct.comp ((K.ιStupidTrunc e).f i') (CategoryTheory.CategoryStruct.comp (φ.f i') h)

noncomputable def HomologicalComplex.πStupidTruncf {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] (i' : ι') : K.X i' ⟶ (K.stupidTrunc e).X i'

Auxiliary definition for πStupidTrunc.

Equations

• K.πStupidTruncf e i' = if h : ∃ (i : ι), e.f i = i' then (K.stupidTruncXIso e ⋯).inv else 0

theorem HomologicalComplex.πStupidTruncf_eq {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] (i : ι) : K.πStupidTruncf e (e.f i) = ((K.restriction e).extendXIso e ⋯).inv

theorem HomologicalComplex.πStupidTruncf_eq' {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] {i : ι} {i' : ι'} (h : e.f i = i') : K.πStupidTruncf e i' = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e h).inv ((K.restriction e).extendXIso e h).inv

noncomputable def HomologicalComplex.πStupidTrunc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] : K ⟶ K.stupidTrunc e

The epimorphism K ⟶ K.stupidTrunc e when the embedding e of complex shapes satisfies e.IsTruncLE.

Equations

• K.πStupidTrunc e = { f := K.πStupidTruncf e, comm' := ⋯ }

theorem HomologicalComplex.πStupidTrunc_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] (i' : ι') : (K.πStupidTrunc e).f i' = K.πStupidTruncf e i'

theorem HomologicalComplex.isIso_πStupidTrunc_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] {i' : ι'} {i : ι} (h : e.f i = i') : CategoryTheory.IsIso ((K.πStupidTrunc e).f i')

instance HomologicalComplex.instIsIsoFπStupidTruncF {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] (i : ι) : CategoryTheory.IsIso ((K.πStupidTrunc e).f (e.f i))

instance HomologicalComplex.instEpiFπStupidTrunc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] (i' : ι') : CategoryTheory.Epi ((K.πStupidTrunc e).f i')

instance HomologicalComplex.instEpiπStupidTrunc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] : CategoryTheory.Epi (K.πStupidTrunc e)

theorem HomologicalComplex.isIso_πStupidTrunc_iff {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] : CategoryTheory.IsIso (K.πStupidTrunc e) ↔ K.IsStrictlySupported e

instance HomologicalComplex.instIsIsoπStupidTruncOfIsStrictlySupported {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] [K.IsStrictlySupported e] : CategoryTheory.IsIso (K.πStupidTrunc e)

@[simp]

theorem HomologicalComplex.πStupidTrunc_naturality {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncLE] : CategoryTheory.CategoryStruct.comp (K.πStupidTrunc e) (stupidTruncMap φ e) = CategoryTheory.CategoryStruct.comp φ (L.πStupidTrunc e)

@[simp]

theorem HomologicalComplex.πStupidTrunc_naturality_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncLE] {Z : HomologicalComplex C c'} (h : L.stupidTrunc e ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.πStupidTrunc e) (CategoryTheory.CategoryStruct.comp (stupidTruncMap φ e) h) = CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (L.πStupidTrunc e) h)

@[simp]

theorem HomologicalComplex.πStupidTrunc_f_naturality {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncLE] (i' : ι') : CategoryTheory.CategoryStruct.comp ((K.πStupidTrunc e).f i') ((stupidTruncMap φ e).f i') = CategoryTheory.CategoryStruct.comp (φ.f i') ((L.πStupidTrunc e).f i')

@[simp]

theorem HomologicalComplex.πStupidTrunc_f_naturality_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsTruncLE] (i' : ι') {Z : C} (h : (L.stupidTrunc e).X i' ⟶ Z) : CategoryTheory.CategoryStruct.comp ((K.πStupidTrunc e).f i') (CategoryTheory.CategoryStruct.comp ((stupidTruncMap φ e).f i') h) = CategoryTheory.CategoryStruct.comp (φ.f i') (CategoryTheory.CategoryStruct.comp ((L.πStupidTrunc e).f i') h)

@[implicit_reducible]

noncomputable def ComplexShape.Embedding.stupidTruncFunctor {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [e.IsRelIff] : CategoryTheory.Functor (HomologicalComplex C c') (HomologicalComplex C c')

The stupid truncation functor HomologicalComplex C c' ⥤ HomologicalComplex C c' given by an embedding e : Embedding c c' of complex shapes.

Equations

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

@[simp]

theorem ComplexShape.Embedding.stupidTruncFunctor_obj {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [e.IsRelIff] (K : HomologicalComplex C c') : (e.stupidTruncFunctor C).obj K = K.stupidTrunc e

@[simp]

theorem ComplexShape.Embedding.stupidTruncFunctor_map {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [e.IsRelIff] {X✝ Y✝ : HomologicalComplex C c'} (φ : X✝ ⟶ Y✝) : (e.stupidTruncFunctor C).map φ = HomologicalComplex.stupidTruncMap φ e

noncomputable def ComplexShape.Embedding.ιStupidTruncNatTrans {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [e.IsTruncGE] : e.stupidTruncFunctor C ⟶ CategoryTheory.Functor.id (HomologicalComplex C c')

When e : Embedding c c' satisfies [e.IsTruncGE], this is the natural transformation K.ιStupidTrunc e : K.stupidTrunc e ⟶ K for all K : HomologicalComplex C c'.

Equations

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

@[simp]

theorem ComplexShape.Embedding.ιStupidTruncNatTrans_app {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [e.IsTruncGE] (K : HomologicalComplex C c') : (e.ιStupidTruncNatTrans C).app K = K.ιStupidTrunc e

noncomputable def ComplexShape.Embedding.πStupidTruncNatTrans {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [e.IsTruncLE] : CategoryTheory.Functor.id (HomologicalComplex C c') ⟶ e.stupidTruncFunctor C

When e : Embedding c c' satisfies [e.IsTruncLE], this is the natural transformation K.πStupidTrunc e : K ⟶ K.stupidTrunc e for all K : HomologicalComplex C c'.

Equations

• e.πStupidTruncNatTrans C = { app := fun (K : HomologicalComplex C c') => K.πStupidTrunc e, naturality := ⋯ }

@[simp]

theorem ComplexShape.Embedding.πStupidTruncNatTrans_app {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [e.IsTruncLE] (K : HomologicalComplex C c') : (e.πStupidTruncNatTrans C).app K = K.πStupidTrunc e