Documentation

TauCeti.CategoryTheory.Exact.HomologicalComplex

The degreewise exact structure on homological complexes #

Let E be a Quillen exact structure on an additive category C and let c be a complex shape. The category HomologicalComplex C c carries the degreewise exact structure E.homologicalComplex c: a short complex of complexes is a conflation when it is a conflation of E in every degree. No limits or colimits are assumed in C: the kernels, cokernels, pushouts and pullbacks that the axioms require are those supplied degreewise by E, assembled into complexes by Mathlib's degreewise (co)limits in HomologicalComplex C c.

Specializing E to the split exact structure ExactStructure.split C gives the componentwise split exact structure (ExactStructure.split C).homologicalComplex c, whose conflations are the short complexes of complexes that split in every degree, though not necessarily compatibly with the differentials (by homologicalComplex_conflation_iff and ExactStructure.split_conflation). These are the short exact sequences studied in Mathlib's Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit. For cochain complexes, and for the n-periodic complexes indexed by ComplexShape.up (ZMod n), it is the exact structure for which Keller shows the category of complexes to be Frobenius, with the homotopy category as its stable category; that comparison is not part of this file.

Main definitions #

Main results #

References #

source
instance TauCeti.instHasBinaryBiproductsHomologicalComplex_tauCeti {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u'} {c : ComplexShape ι} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] :
CategoryTheory.Limits.HasBinaryBiproducts (HomologicalComplex C c)

The category of homological complexes in a preadditive category with binary biproducts has binary biproducts, computed degreewise.

source
theorem TauCeti.IsKernelCokernelPair.of_eval {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u'} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (h : ∀ (i : ι), IsKernelCokernelPair (S.map (HomologicalComplex.eval C c i))) :
IsKernelCokernelPair S

A short complex of homological complexes which is a kernel–cokernel pair in every degree is a kernel–cokernel pair: kernels and cokernels in HomologicalComplex C c may be computed degreewise.

source
theorem TauCeti.hasColimit_span_comp_eval {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u'} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] {K L M : HomologicalComplex C c} {f : K ⟶ L} {g : K ⟶ M} (h : ∀ (i : ι), CategoryTheory.Limits.HasPushout (f.f i) (g.f i)) (i : ι) :
CategoryTheory.Limits.HasColimit ((CategoryTheory.Limits.span f g).comp (HomologicalComplex.eval C c i))

If a span of complexes has a pushout in every degree, then its composite with each evaluation functor has a colimit. Mathlib's degreewise instances then supply its pushout in complexes.

source
theorem TauCeti.hasLimit_cospan_comp_eval {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u'} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] {K L M : HomologicalComplex C c} {f : K ⟶ M} {g : L ⟶ M} (h : ∀ (i : ι), CategoryTheory.Limits.HasPullback (f.f i) (g.f i)) (i : ι) :
CategoryTheory.Limits.HasLimit ((CategoryTheory.Limits.cospan f g).comp (HomologicalComplex.eval C c i))

If a cospan of complexes has a pullback in every degree, then its composite with each evaluation functor has a limit. Mathlib's degreewise instances then supply its pullback in complexes.

source
noncomputable def TauCeti.ExactStructure.homologicalComplex {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u'} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (c : ComplexShape ι) :
ExactStructure (HomologicalComplex C c)

The degreewise exact structure on homological complexes. A short complex of complexes is a conflation when it is a conflation of E in every degree.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.ExactStructure.homologicalComplex_conflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u'} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (c : ComplexShape ι) (S : CategoryTheory.ShortComplex (HomologicalComplex C c)) :
    (E.homologicalComplex c).Conflation S ↔ ∀ (i : ι), E.Conflation (S.map (HomologicalComplex.eval C c i))

    A short complex of complexes is a conflation for the degreewise exact structure exactly when it is a conflation in every degree.

    source
    @[simp]
    theorem TauCeti.ExactStructure.homologicalComplex_isInflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u'} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (c : ComplexShape ι) {K L : HomologicalComplex C c} (f : K ⟶ L) :
    (E.homologicalComplex c).IsInflation f ↔ ∀ (i : ι), E.IsInflation (f.f i)

    A morphism of complexes is an inflation for the degreewise exact structure exactly when it is an inflation in every degree.

    source
    @[simp]
    theorem TauCeti.ExactStructure.homologicalComplex_isDeflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u'} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (c : ComplexShape ι) {K L : HomologicalComplex C c} (f : K ⟶ L) :
    (E.homologicalComplex c).IsDeflation f ↔ ∀ (i : ι), E.IsDeflation (f.f i)

    A morphism of complexes is a deflation for the degreewise exact structure exactly when it is a deflation in every degree.

    source
    theorem TauCeti.ExactStructure.isConflationExact_eval_homologicalComplex {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u'} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (c : ComplexShape ι) (i : ι) :
    (E.homologicalComplex c).IsConflationExact E (HomologicalComplex.eval C c i)

    Evaluation in a fixed degree preserves conflations of the degreewise exact structure.

    source
    theorem TauCeti.ExactStructure.IsConflationExact.mapHomologicalComplex {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u'} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (c : ComplexShape ι) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) :
    (E.homologicalComplex c).IsConflationExact (E'.homologicalComplex c) (F.mapHomologicalComplex c)

    A conflation-exact functor induces, degreewise, a conflation-exact functor between the degreewise exact structures on complexes.