Documentation

TauCeti.CategoryTheory.DG.Preadditive

Additive structure on the closed category of a DG category #

The canonical equivalence between closed morphisms and degree-zero cocycles transports the additive group and base-ring module structures to the existing underlying category. Composition is bilinear by the DG composition laws. Taking closed components and passing to their homotopy classes preserve these operations, so the canonical functor to H⁰ is additive and linear. DG functors also induce additive linear functors between the closed categories.

References #

source
@[instance_reducible]
noncomputable instance TauCeti.instAddCommGroupDGClosedHom (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C) :
AddCommGroup (X ⟶ Y)

Closed morphisms form an additive group by the canonical equivalence with cocycles.

source
noncomputable def TauCeti.dgClosedHomAddEquiv (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C) :
(X ⟶ Y) ≃+ ↥(dgCycles R (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) X) (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) Y))

The canonical cocycle equivalence is additive for the transported group structure.

Instances For
    source
    @[instance_reducible]
    noncomputable instance TauCeti.instModuleDGClosedHom (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C) :
    Module R (X ⟶ Y)

    Closed morphisms are a base-ring module by transport through their cocycle equivalence.

    source
    @[simp]
    theorem TauCeti.dgClosedHomAddEquiv_apply_coe (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (f : X ⟶ Y) :
    ↑((dgClosedHomAddEquiv R X Y) f) = dgClosedHom R f

    The additive cocycle equivalence takes a morphism to its closed component.

    source
    @[simp]
    theorem TauCeti.dgClosedHom_zero (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C) :
    dgClosedHom R 0 = 0

    Taking the closed component preserves zero.

    source
    @[simp]
    theorem TauCeti.dgClosedHom_add (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (f g : X ⟶ Y) :
    dgClosedHom R (f + g) = dgClosedHom R f + dgClosedHom R g

    Taking the closed component preserves addition.

    source
    @[simp]
    theorem TauCeti.dgClosedHom_smul (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (r : R) (f : X ⟶ Y) :
    dgClosedHom R (r • f) = r • dgClosedHom R f

    Taking the closed component preserves scalar multiplication.

    source
    @[instance_reducible]
    noncomputable instance TauCeti.instPreadditiveDGClosedCategory (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] :
    CategoryTheory.Preadditive (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C)

    The closed category is preadditive by bilinearity of degree-zero DG composition.

    source
    @[instance_reducible]
    noncomputable instance TauCeti.instLinearDGClosedCategory (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] :
    CategoryTheory.Linear R (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C)

    The closed category is linear over the base ring.

    source
    instance TauCeti.instAdditiveForgetEnrichmentCochainComplexModuleCatIntDGHomotopyCategoryDgClosedToHomotopy (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] :
    (dgClosedToHomotopy R).Additive
    source
    instance TauCeti.instLinearForgetEnrichmentCochainComplexModuleCatIntDGHomotopyCategoryDgClosedToHomotopy (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] :
    CategoryTheory.Functor.Linear R (dgClosedToHomotopy R)
    source
    instance TauCeti.instAdditiveForgetEnrichmentCochainComplexModuleCatIntForget_tauCeti (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {D : Type u'} [DGCategory R D] (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) :
    F.forget.Additive
    source
    instance TauCeti.instLinearForgetEnrichmentCochainComplexModuleCatIntForget_tauCeti (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {D : Type u'} [DGCategory R D] (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) :
    CategoryTheory.Functor.Linear R F.forget