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}
[DecidableEq ι]
(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}
[DecidableEq ι]
(c : ComplexShape ι)
[c.HasNoLoop]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{α : Type t}
{X : α → C}
(hX : CategoryTheory.IsSeparating (Set.range X))
:
theorem
HomologicalComplex.isSeparator_coproduct_separatingFamily
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type w}
[DecidableEq ι]
(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}
[DecidableEq ι]
(c : ComplexShape ι)
[c.HasNoLoop]
[CategoryTheory.Limits.HasCoproductsOfShape ι C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.HasSeparator C]
: