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.

TODO (@joelriou)

• define the inclusion e.stupidTruncFunctor C ⟶ 𝟭 _ when [e.IsTruncGE];
• define the projection 𝟭 _ ⟶ e.stupidTruncFunctor C when [e.IsTruncLE].

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.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.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 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_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

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