Semisimple degree-zero parts of graded algebras #
This file gives a criterion for the degree-zero part of a graded algebra to be semisimple. If it is spanned over a field by a complete family of orthogonal idempotents, it is a quotient of a finite product of copies of the field and hence is semisimple.
Main results #
TauCeti.isSemisimpleRing_gradeZero_of_completeOrthogonalIdempotents: a degree-zero piece spanned by a complete family of orthogonal idempotents is a semisimple ring.
theorem
TauCeti.isSemisimpleRing_gradeZero_of_completeOrthogonalIdempotents
{k : Type uk}
[Field k]
{A : Type uA}
[Ring A]
[Algebra k A]
{π : β€ β Submodule k A}
{I : Type uI}
{e : I β A}
[Fintype I]
(hcomplete : CompleteOrthogonalIdempotents e)
(heβ : β (i : I), e i β π 0)
(hspan : π 0 β€ Submodule.span k (Set.range e))
[SetLike.GradedMonoid π]
:
IsSemisimpleRing β₯(π 0)
A degree-zero piece spanned by a complete family of orthogonal idempotents is a semisimple
ring: c β¦ β cα΅’ eα΅’ is a surjective ring homomorphism from I β k onto π 0. Thus split
degree-zero parts satisfy the semisimplicity hypothesis of minimal graded resolution theory.