Category

Results named in Tau Ceti's TauCeti.Algebra.Category modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremFitting's lemma, categorically#

an object of ModuleCat A whose underlying module has finite length is indecomposable exactly when its ring of endomorphisms in the category is local.

TauCeti.indecomposable_iff_isLocalRing_end.{u, v} {A : Type u} [Ring A] (M : ModuleCat A)
  (hM : IsFiniteLength A ↑M) : CategoryTheory.Indecomposable M ↔ IsLocalRing (CategoryTheory.End M)
Lean

Formalized in Tau Ceti as TauCeti.indecomposable_iff_isLocalRing_end.

Other forms

Fitting's lemma in FGModuleCat A. Formalized in Tau Ceti as FGModuleCat.isLocalRing_end_of_indecomposable.

FGModuleCat.isLocalRing_end_of_indecomposable.{w, v} {A : Type v} [Ring A] {X : FGModuleCat A}
  [IsNoetherian A ↑X.obj] [IsArtinian A ↑X.obj] (hX : CategoryTheory.Indecomposable X.obj) :
  IsLocalRing (CategoryTheory.End X)
Sources
LeanTauCeti.indecomposable_iff_isLocalRing_end · FGModuleCat.isLocalRing_end_of_indecomposable
Uses 1 · Used by 1
Proof usesFitting's lemma
Used byThe Auslander–Reiten theorem, existence

TheoremThe general-field Cartan--Poincaré identity#

Let C be the graded Cartan matrix in a projective basis of classes [A eᵢ] and the module basis [Sⱼ], with gdim(eᵢ • Sⱼ) = 0 for i ≠ j. Suppose every pair of finite graded modules is graded Euler-admissible, that every Sᵢ is concentrated in internal degree zero and has a linear graded projective resolution, and that b bounds the cohomological support of Ext between any two Sᵢ. Then Cᵀ · P(-q) = diagonal (fun i ↦ gdim(eᵢ • Sᵢ)), where P is the diagonal Ext Poincaré matrix truncated below b. Concentration makes these diagonal entries constant.

TauCeti.gradedCartanMatrix_transpose_mul_diagonalExtPoincareMatrix_map_eq_diagonal.{uk, uA, uI}
  {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A}
  [GradedAlgebra 𝒜] [Module.Finite k A] [CategoryTheory.HasExt (TauCeti.GradedModuleCat 𝒜)]
  {I : Type uI} [Fintype I] [DecidableEq I]
  (S : I → (TauCeti.gradedFiniteModules 𝒜).FullSubcategory) {e : I → A}
  (he : ∀ (i : I), IsIdempotentElem (e i)) (he₀ : ∀ (i : I), e i ∈ 𝒜 0)
  (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i}))
  (hne : Pairwise fun i j => TauCeti.GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0)
  (bP :
    Module.Basis I (LaurentPolynomial ℤ)
      (TauCeti.LaurentK0 (TauCeti.gradedFiniteProjectiveModulesExactStructure 𝒜)))
  (hbP :
    ∀ (i : I),
      bP i =
        TauCeti.LaurentK0.of (TauCeti.gradedFiniteProjectiveModulesExactStructure 𝒜)
          { obj := TauCeti.GradedModuleCat.ofIdeal 𝒜 (Ideal.span {e i}) ⋯, property := ⋯ })
  (bM :
    Module.Basis I (LaurentPolynomial ℤ)
      (TauCeti.LaurentK0 (TauCeti.gradedFiniteModulesExactStructure 𝒜)))
  (hbM : ∀ (i : I), bM i = TauCeti.LaurentK0.of (TauCeti.gradedFiniteModulesExactStructure 𝒜) (S i))
  (h :
    TauCeti.IsGradedEulerAdmissibleOn (TauCeti.gradedFiniteModules 𝒜)
      (TauCeti.gradedFiniteModules 𝒜))
  (hlin : ∀ (i : I), ∃ r, r.IsLinear)
  (hconc : ∀ (i : I) (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) {b : ℕ}
  (hb :
    ∀ (i j : I),
      TauCeti.IsGradedExtBoundedBy (TauCeti.GradedModuleCat.shift 𝒜) (S i).obj (S j).obj b) :
  (TauCeti.gradedCartanMatrix 𝒜 bP bM).transpose *
      (TauCeti.diagonalExtPoincareMatrix k (fun i => (S i).obj) b).map
        ⇑(Polynomial.eval₂RingHom LaurentPolynomial.C (-LaurentPolynomial.T 1)) =
    Matrix.diagonal fun i => TauCeti.GradedModuleCat.smulGradedDimension (e i) (S i).obj
Lean

Formalized in Tau Ceti as TauCeti.gradedCartanMatrix_transpose_mul_diagonalExtPoincareMatrix_map_eq_diagonal.

Sources
LeanTauCeti.gradedCartanMatrix_transpose_mul_diagonalExtPoincareMatrix_map_eq_diagonal
Uses 4 · Used by 1
Statement usesThe graded Cartan matrix in a projective basis bP and a module basis bM · TauCeti.GradedProjectiveResolution.IsLinear
Proof usesThe dual Noether isomorphism · The Noether isomorphism for exact categories
Used byThe Cartan--Poincare identity over a semisimple degree-zero part

TheoremThe Krull-Schmidt theorem with no ambient object#

an isomorphism between two finite biproducts of indecomposable objects of finite length matches their summands by a bijection of the index sets.

TauCeti.exists_equiv_iso_of_biproduct_iso.{u, v} {A : Type u} [Ring A] {ι κ : Type} [Finite ι]
  [Finite κ] {P : ι → ModuleCat A} {Q : κ → ModuleCat A} [IsNoetherian A ↑(⨁ P)]
  [IsArtinian A ↑(⨁ P)] (e : ⨁ P ≅ ⨁ Q) (hP : ∀ (i : ι), CategoryTheory.Indecomposable (P i))
  (hQ : ∀ (j : κ), CategoryTheory.Indecomposable (Q j)) : ∃ f, ∀ (i : ι), Nonempty (P i ≅ Q (f i))
Lean

Formalized in Tau Ceti as TauCeti.exists_equiv_iso_of_biproduct_iso.

Other forms

The Krull-Schmidt theorem for biproducts in ModuleCat A. Formalized in Tau Ceti as TauCeti.exists_equiv_iso_of_iso_biproduct.

TauCeti.exists_equiv_iso_of_iso_biproduct.{u, v} {A : Type u} [Ring A] {ι κ : Type} [Finite ι]
  [Finite κ] {P : ι → ModuleCat A} {Q : κ → ModuleCat A} {X : ModuleCat A} [IsNoetherian A ↑X]
  [IsArtinian A ↑X] (eP : X ≅ ⨁ P) (eQ : X ≅ ⨁ Q)
  (hP : ∀ (i : ι), CategoryTheory.Indecomposable (P i))
  (hQ : ∀ (j : κ), CategoryTheory.Indecomposable (Q j)) : ∃ e, ∀ (i : ι), Nonempty (P i ≅ Q (e i))
Sources
LeanTauCeti.exists_equiv_iso_of_biproduct_iso · TauCeti.exists_equiv_iso_of_iso_biproduct
Uses 1 · Used by 1
Proof usesThe Krull-Schmidt theorem
Used byThe Krull-Schmidt theorem for quiver representations

TheoremThe module-category Frobenius theorem#

For a finite-dimensional algebra A over a field which is self-injective on both sides, the canonical exact structure on the category of finitely generated (equivalently, finite-dimensional) A-modules is Frobenius.

FGModuleCat.abelian_isFrobenius.{u, v, w} (k : Type w) [Field k] {A : Type u} [Ring A] [Algebra k A]
  [FiniteDimensional k A] [Small.{v, u} A] [IsNoetherianRing A] (hl : Module.Injective A A)
  (hr : Module.Injective Aᵐᵒᵖ A) : (TauCeti.ExactStructure.abelian (FGModuleCat A)).IsFrobenius
Lean

Formalized in Tau Ceti as FGModuleCat.abelian_isFrobenius.

Sources
LeanFGModuleCat.abelian_isFrobenius

DefinitionThe resolution theorem for modules#

If every finitely generated R-module admits a finite resolution by finitely generated projective modules, then the Cartan map K₀(proj R) ⟶ G₀(mod R) is an isomorphism; its inverse sends the class of a module to the alternating class of any such resolution.

TauCeti.cartanEquiv.{u} (R : Type u) [Ring R]
  (h :
    ModuleCat.isFG R ≤
      (TauCeti.ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution
        (TauCeti.finiteProjectiveModules R)) :
  TauCeti.ExactK0 (TauCeti.finiteProjectiveModulesExactStructure R) ≃+
    TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure R)
Lean

Formalized in Tau Ceti as TauCeti.cartanEquiv.

Sources
LeanTauCeti.cartanEquiv
Uses 4 · Used by 1
Statement usesThe resolution theorem for modules admitting finite resolutions by finitely generated projectives
Proof usesThe dual Noether isomorphism · The Noether isomorphism for exact categories · The resolution theorem for finite projective resolutions
Used byCartan-matrix unimodularity

DefinitionThe resolution theorem for modules admitting finite resolutions by finitely generated projectives#

their exact K₀ is the exact K₀ of the finitely generated projective modules. This is TauCeti.ExactStructure.resolutionEquiv in ModuleCat R; its inverse sends the class of a module to the alternating class of any such resolution.

TauCeti.moduleResolutionEquiv.{u} (R : Type u) [Ring R] :
  TauCeti.ExactK0 (TauCeti.finiteProjectiveModulesExactStructure R) ≃+
    TauCeti.ExactK0 (TauCeti.finiteProjectiveResolutionExactStructure R)
Lean

Formalized in Tau Ceti as TauCeti.moduleResolutionEquiv.

Sources
LeanTauCeti.moduleResolutionEquiv
Uses 3 · Used by 2
Statement usesThe resolution theorem for finite projective resolutions
Proof usesThe dual Noether isomorphism · The Noether isomorphism for exact categories
Used byThe resolution theorem for modules · Cartan-matrix unimodularity

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.