instance
CategoryTheory.endScalarTower
(k : Type w)
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
(P : C)
:
IsScalarTower k (End P) (End P)
The k-action on End P commutes with right-composition by an endomorphism, so
End P carries a scalar tower over k with itself as the inner ring.
theorem
CategoryTheory.endRing_isArtinian
(k : Type w)
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
{P : C}
[FiniteDimensional k (End P)]
:
IsArtinianRing (End P)
A finite-dimensional endomorphism algebra over a field is Artinian as a ring,
obtained by transferring the Artinian property from k-modules.
def
CategoryTheory.postCompEndMap
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
{P : C}
(g : End P)
:
Module.End k (End P)
Post-composition by a fixed endomorphism g : End P, viewed as a k-linear
endomorphism of the k-vector space End P.
Instances For
class
CategoryTheory.FiniteAbelianCategory.HasLocalEndOfIndecomposable
(k : Type w)
[Field k]
(C : Type u)
[Category.{v, u} C]
[Abelian C]
[Linear k C]
:
A k-linear abelian category satisfies the Fitting property if every indecomposable
object has a local endomorphism ring. This holds in finite abelian categories.
- isLocalRing_end_of_indecomposable (P : C) : Indecomposable P → IsLocalRing (End P)