Generators of the category of homological complexes #
Let c : ComplexShape ι be a complex shape with no loop.
If a category C has a separator, then HomologicalComplex C c
has a separating family, and a separator when suitable coproducts exist.
noncomputable def HomologicalComplex.separatingFamily {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {α : Type t} (X : α → C) (j : α × ι) :
If X : α → C is a separating family, and c : ComplexShape ι has no loop,
then this is a separating family indexed by α × ι in HomologicalComplex C c,
which consists of homological complexes that are nonzero in at most
two (consecutive) degrees.
Equations
- HomologicalComplex.separatingFamily c X j = HomologicalComplex.evalCompCoyonedaCorepresentative c (X j.1) j.2
Instances For
theorem HomologicalComplex.isSeparating_separatingFamily {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} (c : ComplexShape ι) [c.HasNoLoop] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {α : Type t} {X : α → C} (hX : (CategoryTheory.ObjectProperty.ofObj X).IsSeparating) :
theorem HomologicalComplex.isSeparator_coproduct_separatingFamily {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} (c : ComplexShape ι) [c.HasNoLoop] [CategoryTheory.Limits.HasCoproductsOfShape ι C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (hX : CategoryTheory.IsSeparator X) :
CategoryTheory.IsSeparator (∐ fun (i : ι) => separatingFamily c (fun (x : Unit) => X) (PUnit.unit, i))
instance HomologicalComplex.instHasSeparator {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} (c : ComplexShape ι) [c.HasNoLoop] [CategoryTheory.Limits.HasCoproductsOfShape ι C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasSeparator C] :