Preadditive

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

TheoremJacobson's lemma #

𝟙 X - a ≫ b is invertible exactly when 𝟙 Y - b ≫ a is.

CategoryTheory.isIso_id_sub_comp_comm.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Preadditive C] {X Y : C} (a : X ⟶ Y) (b : Y ⟶ X) :
  CategoryTheory.IsIso
      (CategoryTheory.CategoryStruct.id X - CategoryTheory.CategoryStruct.comp a b) ↔
    CategoryTheory.IsIso
      (CategoryTheory.CategoryStruct.id Y - CategoryTheory.CategoryStruct.comp b a)

Lean

Formalized in Tau Ceti as CategoryTheory.isIso_id_sub_comp_comm.

Sources

LeanCategoryTheory.isIso_id_sub_comp_comm

Used by 6

Used byThe graded Cartan matrix of the dual numbers is 1 + q², with ε in degree two, in the bases [A] and [S] · The graded projectives A eᵢ form a basis of K₀^gr(proj A) · The q-Euler matrix of a path algebra is the inverse of its conjugate-transposed graded Cartan matrix · The Auslander–Reiten theorem, existence · TauCeti.gradedCartanMatrix_zigzagAlgebra · The action of the graph's Artin group on K₀^gr(proj Z)

DefinitionSchur's lemma as an identification of algebras #

the endomorphisms of a simple object X with finite-dimensional endomorphisms over an algebraically closed field k are the scalars k. This is the inverse of the structure map algebraMap k (End X), c ↦ c • 𝟙 X.

TauCeti.endAlgEquivOfSimple.{w, v, u} (k : Type w) [Field k] [IsAlgClosed k] {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C]
  [CategoryTheory.Limits.HasKernels C] (X : C) [CategoryTheory.Simple X]
  [FiniteDimensional k (X ⟶ X)] : CategoryTheory.End X ≃ₐ[k] k

Lean

Formalized in Tau Ceti as TauCeti.endAlgEquivOfSimple.

Sources

LeanTauCeti.endAlgEquivOfSimple

Used by 2

Used byThe global dimension does not depend on the pivotal structure · The global dimension of a pivotal fusion category over a field of characteristic zero is nonzero (Etingof–Nikshych–Ostrik)

TheoremTauCeti.isLocalRing_end_of_indecomposable #

Fitting's lemma: an indecomposable object has a local endomorphism ring, in an idempotent-complete linear category over a commutative Artinian ring R when the endomorphisms of the object are finitely generated over R, for instance in a Hom-finite linear category over a field. Indecomposability leaves 0 and 1 as the only idempotents of End X (TauCeti.idempotent_eq_zero_or_id_of_indecomposable).

TauCeti.isLocalRing_end_of_indecomposable.{v, u, u_1} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [CommRing R]
  [IsArtinianRing R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C]
  [CategoryTheory.IsIdempotentComplete C] {X : C} [Module.Finite R (X ⟶ X)]
  (hX : CategoryTheory.Indecomposable X) : IsLocalRing (CategoryTheory.End X)