Stable, periodic, and curved homological algebra

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremHappel's theorem#

The stable category of a Frobenius exact category, with the shift generated by stable suspension and the triangles generated by conflations, is triangulated.

TauCeti.ExactStructure.IsFrobenius.stableIsTriangulated.{v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C]
  {E : TauCeti.ExactStructure C} (hE : E.IsFrobenius) :
  CategoryTheory.IsTriangulated E.ProjectiveStableCategory
Lean

Formalized in Tau Ceti as TauCeti.ExactStructure.IsFrobenius.stableIsTriangulated.

Other forms

Happel's theorem, pretriangulated part. Formalized in Tau Ceti as TauCeti.ExactStructure.IsFrobenius.stablePretriangulated.

TauCeti.ExactStructure.IsFrobenius.stablePretriangulated.{v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C]
  {E : TauCeti.ExactStructure C} (hE : E.IsFrobenius) :
  CategoryTheory.Pretriangulated E.ProjectiveStableCategory
Sources
LeanTauCeti.ExactStructure.IsFrobenius.stableIsTriangulated · TauCeti.ExactStructure.IsFrobenius.stablePretriangulated
Uses 1 · Used by 5
Proof usesThe Noether isomorphism for exact categories
Used byCompression is a triangle functor on derived categories · TauCeti.CurvedDGRightModuleCat.absolutelyAcyclic · The homotopy category of curved right modules is triangulated, with the shift by one given by the cohomological shift · The homotopy category of matrix factorizations is triangulated, with the shift by 1 given by the parity shift · The triangulation of the periodic homotopy category is the mapping-cone triangulation

TheoremThe triangulation of the periodic homotopy category is the mapping-cone triangulation#

A triangle is distinguished exactly when it is isomorphic to the image of a mapping-cone triangle X ⟶ Y ⟶ cone(f) ⟶ X⟦1⟧ of periodic complexes, whose last map is minus the cone projection.

TauCeti.PeriodicComplex.mem_distTriang_iff.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ}
  (T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up (ZMod n)))) :
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔
    ∃ X Y f, Nonempty (T ≅ TauCeti.PeriodicComplex.mappingConeTriangle f)
Lean

Formalized in Tau Ceti as TauCeti.PeriodicComplex.mem_distTriang_iff.

Sources
LeanTauCeti.PeriodicComplex.mem_distTriang_iff
Uses 1
Proof usesHappel's theorem

TheoremThe homotopy category of matrix factorizations is triangulated, with the shift by 1 given by the parity shift# 

TauCeti.MatrixFactorization.HomotopyCategory.instIsTriangulated.{u} (S : Type u) [CommRing S]
  (w : S) : CategoryTheory.IsTriangulated TauCeti.MatrixFactorization.HomotopyCategory
Lean

Formalized in Tau Ceti as TauCeti.MatrixFactorization.HomotopyCategory.instIsTriangulated.

Sources
LeanTauCeti.MatrixFactorization.HomotopyCategory.instIsTriangulated
Uses 3
Proof usesThe dual Noether isomorphism · Happel's theorem · The Noether isomorphism for exact categories

TheoremThe homotopy category of curved right modules is triangulated, with the shift by one given by the cohomological shift# 

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

Formalized in Tau Ceti as TauCeti.CurvedDGRightModuleCat.homotopyIsTriangulated.

Sources
LeanTauCeti.CurvedDGRightModuleCat.homotopyIsTriangulated
Uses 1
Proof usesHappel's theorem

TheoremThe indecomposable finitely generated right modules over A = K[X]/(Xⁿ) are exactly the M_i, up to isomorphism#

such a module is indecomposable exactly when it is isomorphic to A ⧸ (x ^ i) for some 0 < i ≤ n.

TauCeti.isIndecomposableModule_iff_exists_linearEquiv_quotient_span_op_root_X_pow_pow.{u, v}
  {K : Type u} [Field K] {n : ℕ} {M : Type v} [AddCommGroup M]
  [_root_.Module (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ M]
  [Module.Finite (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ M] :
  TauCeti.IsIndecomposableModule (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ M ↔
    ∃ i,
      0 < i ∧
        i ≤ n ∧
          Nonempty
            (M ≃ₗ[(AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ]
              (AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ ⧸
                Ideal.span {MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ i)})
Lean

Formalized in Tau Ceti as TauCeti.isIndecomposableModule_iff_exists_linearEquiv_quotient_span_op_root_X_pow_pow.

Sources
LeanTauCeti.isIndecomposableModule_iff_exists_linearEquiv_quotient_span_op_root_X_pow_pow

DefinitionThe periodic free resolution of M_i over R[X]/(X ^ n)#

With x the class of X and M_i = A ⧸ (x ^ i), the complex ⋯ ⟶ A --x^(n-i)--> A --x^i--> A --x^(n-i)--> A --x^i--> A ⟶ M_i ⟶ 0 is a projective resolution of M_i.

TauCeti.cyclicModuleRootPowProjectiveResolution.{u} (R : Type u) [CommRing R] (n i : ℕ) :
  CategoryTheory.ProjectiveResolution
    ↧((AdjoinRoot (Polynomial.X ^ n))ᵐᵒᵖ ⧸
        Ideal.span {MulOpposite.op (AdjoinRoot.root (Polynomial.X ^ n) ^ i)})
Lean

Formalized in Tau Ceti as TauCeti.cyclicModuleRootPowProjectiveResolution.

Sources
LeanTauCeti.cyclicModuleRootPowProjectiveResolution

DefinitionTauCeti.OrbitCategory.lift#

Keller's descent of an additive functor G with a periodicity isomorphism φ : [n] ⋙ G ≅ G to the orbit category D/[n]. It is G on objects, and acts on morphisms by liftMap G φ.

TauCeti.OrbitCategory.lift.{v, v', u, u'} {D : Type u} [CategoryTheory.Category.{v, u} D]
  [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ]
  [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'}
  [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E]
  (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) :
  CategoryTheory.Functor (TauCeti.OrbitCategory D n) E
Lean

Formalized in Tau Ceti as TauCeti.OrbitCategory.lift.

Sources
LeanTauCeti.OrbitCategory.lift

TheoremCompression is a triangle functor on derived categories# 

TauCeti.PeriodicComplex.instIsTriangulatedBoundedDerivedCategoryDerivedCompressionFunctor.{w, v, u}
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (n : ℕ)
  [HasDerivedCategory C] : (TauCeti.PeriodicComplex.derivedCompressionFunctor n).IsTriangulated
Lean

Formalized in Tau Ceti as TauCeti.PeriodicComplex.instIsTriangulatedBoundedDerivedCategoryDerivedCompressionFunctor.

Sources
LeanTauCeti.PeriodicComplex.instIsTriangulatedBoundedDerivedCategoryDerivedCompressionFunctor
Uses 1
Proof usesHappel's theorem

DefinitionTauCeti.CurvedDGRightModuleCat.absolutelyAcyclic#

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

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

Formalized in Tau Ceti as TauCeti.CurvedDGRightModuleCat.absolutelyAcyclic.

Sources
LeanTauCeti.CurvedDGRightModuleCat.absolutelyAcyclic
Uses 1
Proof usesHappel's theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.