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 Cwhen[e.IsTruncLE].
noncomputable def
HomologicalComplex.stupidTrunc
{ι : 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]
[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
Instances For
instance
HomologicalComplex.instIsStrictlySupportedStupidTrunc
{ι : 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]
[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.{u_4, 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 ⋯
Instances For
theorem
HomologicalComplex.isZero_stupidTrunc_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]
[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.{u_5, 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.{u_4, 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.{u_4, 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
Instances For
@[simp]
theorem
HomologicalComplex.stupidTruncMap_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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c')
(e : c.Embedding c')
[e.IsRelIff]
:
HomologicalComplex.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.{u_4, 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]
:
theorem
HomologicalComplex.stupidTruncMap_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]
[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)
:
@[simp]
theorem
HomologicalComplex.stupidTruncMap_stupidTruncXIso_hom
{ι : 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]
[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 ((HomologicalComplex.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.{u_4, 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 ((HomologicalComplex.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.{u_4, 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.
Instances For
@[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.{u_4, 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.{u_4, 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