Documentation

TauCeti.Algebra.Homology.Curved.Module.Right.Acyclic

Totalizations and the acyclic classes of the second kind #

Let A be a right-convention curved DG algebra. A short exact sequence 0 → K → L → M → 0 in the abelian category of curved right A-modules with closed morphisms has a totalization: the total curved module of the three-term sequence, here realized as the iterated cone cone(cone(K → L) → M) with underlying graded module K[2] × L[1] × M. Curved modules have no homology, so this totalization replaces the homology of the sequence as the basic acyclic object.

Inside the triangulated curved homotopy category this file defines, as closures generated by the class of totalizations,

Each of these, and more generally every isomorphism-closed triangulated subcategory containing all totalizations, satisfies the two-out-of-three property for short exact sequences: if two terms of a short exact sequence of curved modules belong to it, so does the third. In particular its preimage in the closed category is extension-closed in the sense of Mathlib's CategoryTheory.ObjectProperty.IsClosedUnderExtensions.

Main definitions #

Main results #

References #

Totalizations #

source
noncomputable def TauCeti.CurvedDGRightModuleCat.totalization {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (S : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))) :
CurvedDGRightModuleCat h

The totalization of a short complex K ⟶ L ⟶ M of curved right modules: the iterated cone cone(cone(K ⟶ L) ⟶ M), with underlying graded module K[2] × L[1] × M.

Instances For
    source
    theorem TauCeti.CurvedDGRightModuleCat.totalization_eq {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (S : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))) :
    totalization S = cone (coneDesc S.f S.g ⋯)

    The totalization is the cone of the map cone(K ⟶ L) ⟶ M induced by the second map.

    source
    def TauCeti.CurvedDGRightModuleCat.totalizations (R : Type u) {A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} (h : IsCurvedDGAlgebra 𝒜 d w) :
    CategoryTheory.ObjectProperty (DGHomotopyCategory R (CurvedDGRightModuleCat h))

    The objects of the curved homotopy category represented by totalizations of short exact sequences of curved modules.

    Instances For
      source
      theorem TauCeti.CurvedDGRightModuleCat.totalizations_totalization {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {S : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))} (hS : S.ShortExact) :
      totalizations R h (DGHomotopyCategory.of R (totalization S))

      The totalization of a short exact sequence belongs to the class of totalizations.

      source
      theorem TauCeti.CurvedDGRightModuleCat.totalizations_le_iff {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (Q : CategoryTheory.ObjectProperty (DGHomotopyCategory R (CurvedDGRightModuleCat h))) :
      totalizations R h ≤ Q ↔ ∀ (S : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))), S.ShortExact → Q (DGHomotopyCategory.of R (totalization S))

      An object property contains all totalizations exactly when it contains the totalization of every short exact sequence.

      source
      instance TauCeti.CurvedDGRightModuleCat.instNonemptyDGHomotopyCategoryTotalizations {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :
      (totalizations R h).Nonempty
      source
      theorem TauCeti.CurvedDGRightModuleCat.prop_cone_iff_of_shortExact {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (Q : CategoryTheory.ObjectProperty (DGHomotopyCategory R (CurvedDGRightModuleCat h))) [Q.IsTriangulated] [Q.IsClosedUnderIsomorphisms] (hQ : totalizations R h ≤ Q) {S : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))} (hS : S.ShortExact) :
      Q (DGHomotopyCategory.of R (cone S.f)) ↔ Q ((dgClosedToHomotopy R).obj S.X₃)

      In the presence of all totalizations, the cone of the first map of a short exact sequence lies in an isomorphism-closed triangulated subcategory exactly when its last term does.

      source
      theorem TauCeti.CurvedDGRightModuleCat.prop_X₂_of_shortExact {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (Q : CategoryTheory.ObjectProperty (DGHomotopyCategory R (CurvedDGRightModuleCat h))) [Q.IsTriangulated] [Q.IsClosedUnderIsomorphisms] (hQ : totalizations R h ≤ Q) {S : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))} (hS : S.ShortExact) (h₁ : Q ((dgClosedToHomotopy R).obj S.X₁)) (h₃ : Q ((dgClosedToHomotopy R).obj S.X₃)) :
      Q ((dgClosedToHomotopy R).obj S.X₂)

      Closure under extensions. An isomorphism-closed triangulated subcategory of the curved homotopy category containing all totalizations contains the middle term of a short exact sequence whose outer terms it contains.

      source
      theorem TauCeti.CurvedDGRightModuleCat.prop_X₃_of_shortExact {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (Q : CategoryTheory.ObjectProperty (DGHomotopyCategory R (CurvedDGRightModuleCat h))) [Q.IsTriangulated] [Q.IsClosedUnderIsomorphisms] (hQ : totalizations R h ≤ Q) {S : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))} (hS : S.ShortExact) (h₁ : Q ((dgClosedToHomotopy R).obj S.X₁)) (h₂ : Q ((dgClosedToHomotopy R).obj S.X₂)) :
      Q ((dgClosedToHomotopy R).obj S.X₃)

      Closure under cokernels of monomorphisms. An isomorphism-closed triangulated subcategory of the curved homotopy category containing all totalizations contains the last term of a short exact sequence whose first two terms it contains.

      source
      theorem TauCeti.CurvedDGRightModuleCat.prop_X₁_of_shortExact {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (Q : CategoryTheory.ObjectProperty (DGHomotopyCategory R (CurvedDGRightModuleCat h))) [Q.IsTriangulated] [Q.IsClosedUnderIsomorphisms] (hQ : totalizations R h ≤ Q) {S : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))} (hS : S.ShortExact) (h₂ : Q ((dgClosedToHomotopy R).obj S.X₂)) (h₃ : Q ((dgClosedToHomotopy R).obj S.X₃)) :
      Q ((dgClosedToHomotopy R).obj S.X₁)

      Closure under kernels of epimorphisms. An isomorphism-closed triangulated subcategory of the curved homotopy category containing all totalizations contains the first term of a short exact sequence whose last two terms it contains.

      source
      theorem TauCeti.CurvedDGRightModuleCat.isClosedUnderExtensions_inverseImage {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (Q : CategoryTheory.ObjectProperty (DGHomotopyCategory R (CurvedDGRightModuleCat h))) [Q.IsTriangulated] [Q.IsClosedUnderIsomorphisms] (hQ : totalizations R h ≤ Q) :
      (Q.inverseImage (dgClosedToHomotopy R)).IsClosedUnderExtensions

      An isomorphism-closed triangulated subcategory of the curved homotopy category containing all totalizations pulls back to an extension-closed class of curved modules.

      The three acyclic classes #

      source
      def TauCeti.CurvedDGRightModuleCat.absolutelyAcyclic (R : Type u) {A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} (h : IsCurvedDGAlgebra 𝒜 d w) :
      CategoryTheory.ObjectProperty (DGHomotopyCategory R (CurvedDGRightModuleCat h))

      The absolutely acyclic curved right modules: the smallest thick triangulated subcategory of the curved homotopy category containing all totalizations of short exact sequences.

      Instances For
        source
        def TauCeti.CurvedDGRightModuleCat.coacyclic (R : Type u) {A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} (h : IsCurvedDGAlgebra 𝒜 d w) :
        CategoryTheory.ObjectProperty (DGHomotopyCategory R (CurvedDGRightModuleCat h))

        The coacyclic curved right modules: the smallest isomorphism-closed triangulated subcategory of the curved homotopy category containing all totalizations of short exact sequences and closed under coproducts indexed by Type u.

        Instances For
          source
          def TauCeti.CurvedDGRightModuleCat.contraacyclic (R : Type u) {A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} (h : IsCurvedDGAlgebra 𝒜 d w) :
          CategoryTheory.ObjectProperty (DGHomotopyCategory R (CurvedDGRightModuleCat h))

          The contraacyclic curved right modules: the smallest isomorphism-closed triangulated subcategory of the curved homotopy category containing all totalizations of short exact sequences and closed under products indexed by Type u.

          Instances For
            source
            instance TauCeti.CurvedDGRightModuleCat.instIsTriangulatedDGHomotopyCategoryAbsolutelyAcyclic {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :
            (absolutelyAcyclic R h).IsTriangulated
            source
            instance TauCeti.CurvedDGRightModuleCat.instIsStableUnderRetractsDGHomotopyCategoryAbsolutelyAcyclic {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :
            (absolutelyAcyclic R h).IsStableUnderRetracts
            source
            instance TauCeti.CurvedDGRightModuleCat.instIsClosedUnderIsomorphismsDGHomotopyCategoryAbsolutelyAcyclic {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :
            (absolutelyAcyclic R h).IsClosedUnderIsomorphisms
            source
            instance TauCeti.CurvedDGRightModuleCat.instIsTriangulatedDGHomotopyCategoryCoacyclic {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :
            (coacyclic R h).IsTriangulated
            source
            instance TauCeti.CurvedDGRightModuleCat.instIsClosedUnderIsomorphismsDGHomotopyCategoryCoacyclic {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :
            (coacyclic R h).IsClosedUnderIsomorphisms
            source
            instance TauCeti.CurvedDGRightModuleCat.instIsClosedUnderColimitsOfShapeDGHomotopyCategoryCoacyclicDiscrete {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (J : Type u) :
            (coacyclic R h).IsClosedUnderColimitsOfShape (CategoryTheory.Discrete J)
            source
            instance TauCeti.CurvedDGRightModuleCat.instIsStableUnderRetractsDGHomotopyCategoryCoacyclic {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :
            (coacyclic R h).IsStableUnderRetracts

            The coacyclic class is thick, since the curved homotopy category has countable coproducts.

            source
            instance TauCeti.CurvedDGRightModuleCat.instIsTriangulatedDGHomotopyCategoryContraacyclic {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :
            (contraacyclic R h).IsTriangulated
            source
            instance TauCeti.CurvedDGRightModuleCat.instIsClosedUnderIsomorphismsDGHomotopyCategoryContraacyclic {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :
            (contraacyclic R h).IsClosedUnderIsomorphisms
            source
            instance TauCeti.CurvedDGRightModuleCat.instIsClosedUnderLimitsOfShapeDGHomotopyCategoryContraacyclicDiscrete {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (J : Type u) :
            (contraacyclic R h).IsClosedUnderLimitsOfShape (CategoryTheory.Discrete J)
            source
            instance TauCeti.CurvedDGRightModuleCat.instIsStableUnderRetractsDGHomotopyCategoryContraacyclic {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :
            (contraacyclic R h).IsStableUnderRetracts

            The contraacyclic class is thick, since the curved homotopy category has countable products.

            source
            theorem TauCeti.CurvedDGRightModuleCat.totalizations_le_absolutelyAcyclic (R : Type u) {A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} (h : IsCurvedDGAlgebra 𝒜 d w) :
            totalizations R h ≤ absolutelyAcyclic R h

            Totalizations of short exact sequences are absolutely acyclic.

            source
            theorem TauCeti.CurvedDGRightModuleCat.totalizations_le_coacyclic (R : Type u) {A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} (h : IsCurvedDGAlgebra 𝒜 d w) :
            totalizations R h ≤ coacyclic R h

            Totalizations of short exact sequences are coacyclic.

            source
            theorem TauCeti.CurvedDGRightModuleCat.totalizations_le_contraacyclic (R : Type u) {A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} (h : IsCurvedDGAlgebra 𝒜 d w) :
            totalizations R h ≤ contraacyclic R h

            Totalizations of short exact sequences are contraacyclic.

            source
            theorem TauCeti.CurvedDGRightModuleCat.absolutelyAcyclic_le_iff {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {Q : CategoryTheory.ObjectProperty (DGHomotopyCategory R (CurvedDGRightModuleCat h))} [Q.IsTriangulated] [Q.IsStableUnderRetracts] :
            absolutelyAcyclic R h ≤ Q ↔ totalizations R h ≤ Q

            The universal property of the absolutely acyclic class: it is contained in every thick triangulated subcategory of the curved homotopy category containing all totalizations.

            source
            theorem TauCeti.CurvedDGRightModuleCat.coacyclic_le_iff {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {Q : CategoryTheory.ObjectProperty (DGHomotopyCategory R (CurvedDGRightModuleCat h))} [Q.IsTriangulated] [Q.IsClosedUnderIsomorphisms] [∀ (J : Type u), Q.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete J)] :
            coacyclic R h ≤ Q ↔ totalizations R h ≤ Q

            The universal property of the coacyclic class: it is contained in every isomorphism-closed triangulated subcategory of the curved homotopy category containing all totalizations and closed under coproducts indexed by Type u.

            source
            theorem TauCeti.CurvedDGRightModuleCat.contraacyclic_le_iff {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {Q : CategoryTheory.ObjectProperty (DGHomotopyCategory R (CurvedDGRightModuleCat h))} [Q.IsTriangulated] [Q.IsClosedUnderIsomorphisms] [∀ (J : Type u), Q.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete J)] :
            contraacyclic R h ≤ Q ↔ totalizations R h ≤ Q

            The universal property of the contraacyclic class: it is contained in every isomorphism-closed triangulated subcategory of the curved homotopy category containing all totalizations and closed under products indexed by Type u.

            source
            theorem TauCeti.CurvedDGRightModuleCat.absolutelyAcyclic_le_coacyclic (R : Type u) {A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} (h : IsCurvedDGAlgebra 𝒜 d w) :
            absolutelyAcyclic R h ≤ coacyclic R h

            Every absolutely acyclic curved module is coacyclic: the curved homotopy category has countable coproducts, so the coacyclic class is thick.

            source
            theorem TauCeti.CurvedDGRightModuleCat.absolutelyAcyclic_le_contraacyclic (R : Type u) {A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} (h : IsCurvedDGAlgebra 𝒜 d w) :
            absolutelyAcyclic R h ≤ contraacyclic R h

            Every absolutely acyclic curved module is contraacyclic: the curved homotopy category has countable products, so the contraacyclic class is thick.

            source
            instance TauCeti.CurvedDGRightModuleCat.instIsClosedUnderExtensionsForgetEnrichmentCochainComplexModuleCatIntInverseImageDGHomotopyCategoryAbsolutelyAcyclicDgClosedToHomotopy {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :
            ((absolutelyAcyclic R h).inverseImage (dgClosedToHomotopy R)).IsClosedUnderExtensions
            source
            instance TauCeti.CurvedDGRightModuleCat.instIsClosedUnderExtensionsForgetEnrichmentCochainComplexModuleCatIntInverseImageDGHomotopyCategoryCoacyclicDgClosedToHomotopy {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :
            ((coacyclic R h).inverseImage (dgClosedToHomotopy R)).IsClosedUnderExtensions
            source
            instance TauCeti.CurvedDGRightModuleCat.instIsClosedUnderExtensionsForgetEnrichmentCochainComplexModuleCatIntInverseImageDGHomotopyCategoryContraacyclicDgClosedToHomotopy {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :
            ((contraacyclic R h).inverseImage (dgClosedToHomotopy R)).IsClosedUnderExtensions