Basic algebras #
A ring A is basic when its quotient by the Jacobson radical, A ⧸ Ring.jacobson A, is a
finite product of division rings. The definition states this as the quotient being semisimple and
reduced, which says the same thing (TauCeti.isBasic_iff_pi_divisionRing): Artin--Wedderburn
writes a semisimple ring as a finite product of matrix algebras over division rings, one block for
each simple module, and a matrix algebra of size at least two is never reduced, the matrix unit
Eᵢⱼ with i ≠ j being nonzero and square-zero. So over a semisimple ring reducedness says
exactly that every block has size one, that is, that the ring is a product of division rings
rather than of matrix algebras over them; equivalently, that no indecomposable projective is
repeated in a decomposition of the regular module.
That reformulation is the main result. Its ring-level form,
TauCeti.isReduced_iff_pi_divisionRing, holds for an arbitrary semisimple ring and mentions no
algebra structure.
The condition is aimed at a finite-dimensional algebra over a field, where the quotient by the
radical is semisimple because the algebra is Artinian. Whenever that quotient is semisimple -- in
particular for every Artinian, or more generally semiprimary, ring -- the semisimplicity clause is
automatic and basicness is reducedness alone (TauCeti.isBasic_iff_isReduced). Outside that
setting the clause has to be asked for: ℤ has zero Jacobson radical and is reduced, but is not a
product of division rings and is not a basic ring.
Basicness is the normalization step of Morita theory: every finite-dimensional algebra is Morita
equivalent to a basic one, obtained by keeping one indecomposable projective per simple module.
That reduction is not proved here. The model example is on the quiver side: the path algebra of a
finite acyclic quiver is basic (TauCeti.PathAlgebra.isBasic).
Main definitions #
TauCeti.IsBasic: a ring whose quotient by the Jacobson radical is semisimple and reduced.
Main results #
TauCeti.isBasic_def: unfolding lemma forTauCeti.IsBasic.RingEquiv.isBasic_iff: basicness is invariant under a ring equivalence.TauCeti.Matrix.isReduced_iff_subsingleton: a matrix ring over a nonzero reduced semiring is reduced exactly when it has at most one index.TauCeti.isReduced_iff_pi_divisionRing: a semisimple ring is reduced if and only if it is a finite product of division rings.TauCeti.isBasic_iff_pi_divisionRing: a ring is basic if and only if its quotient by the Jacobson radical is a finite product of division rings.TauCeti.isBasic_iff_isReduced: a ring whose quotient by the Jacobson radical is semisimple is basic if and only if that quotient is reduced.TauCeti.isBasic_of_commRing: a commutative ring whose quotient by the Jacobson radical is semisimple is basic.
Implementation notes #
Mathlib's Matrix.uniqueRingEquiv fixes the Fintype structure on the one-element index type to
the one manufactured from Unique, so its type does not match a matrix ring formed with a Fintype
structure coming from elsewhere -- the two are equal but not definitionally so, and the
multiplication of a matrix ring depends on which one is used. Both uses below therefore rewrite
along Subsingleton.elim first; the index types in question are a Fin-indexed one, as produced by
Artin--Wedderburn, and one carrying a Fintype hypothesis.
TauCeti.IsBasic keeps its body private; TauCeti.isBasic_def is the unfolding lemma through which
importing modules use the definition.
TauCeti.IsBasic takes only the ring, with no base field and no finite-dimensionality over it:
neither appears in the condition. Dropping them is what puts semisimplicity of the quotient into
the definition: over a finite-dimensional algebra it is automatic, but for a general ring
reducedness alone is strictly weaker than being a product of division rings. The formulation as
reducedness of the quotient is TauCeti.isBasic_iff_isReduced, which asks only for that
semisimplicity, as an instance. A finite-dimensional algebra over a field supplies it through
IsArtinianRing.of_finite and the instances making an Artinian ring semiprimary and the quotient
of a semiprimary ring by its radical semisimple.
References #
This implements the IsBasic target of the "Basic algebras and Morita reduction" item of Layer 3 of
TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, together with the companion
lemma named there: a semisimple ring is a product of division rings if and only if it is reduced.
See I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative
Algebras I, CUP (2006), Ch. I.6.
Reduced products and reduced matrix rings #
A factor of a reduced product is reduced. The witness is Pi.single: a nilpotent element
of one factor extends by zero to a nilpotent element of the product.
A matrix ring of size at least two is never reduced. For i ≠ j the matrix unit Eᵢⱼ is
nonzero and squares to zero, so a reduced matrix ring over a nonzero semiring has at most one
index.
A matrix ring over a nonzero reduced semiring is reduced exactly in size at most one. In
one direction this is TauCeti.Matrix.subsingleton_of_isReduced; in the other, a matrix ring on an
empty index is the zero ring, and on a one-element index it is the base semiring.
Reduced semisimple rings are products of division rings #
A semisimple ring is reduced exactly when it is a finite product of division rings. Read
through Artin--Wedderburn, reducedness says that every block Matₙᵢ(Dᵢ) has nᵢ = 1, a larger
matrix block carrying a nonzero square-zero matrix unit; the converse is immediate, a division ring
having no nonzero nilpotent element.
Basic algebras #
A ring is basic when its quotient by the Jacobson radical is a finite product of division
rings, stated as that quotient being semisimple and reduced; the two readings agree by
TauCeti.isBasic_iff_pi_divisionRing. When the quotient is semisimple anyway, as for a
finite-dimensional algebra over a field, the condition is reducedness alone -- every Wedderburn
block has size one -- which is TauCeti.isBasic_iff_isReduced.
Equations
- TauCeti.IsBasic A = (IsSemisimpleRing (A ⧸ Ring.jacobson A) ∧ IsReduced (A ⧸ Ring.jacobson A))
Instances For
Unfolding lemma for TauCeti.IsBasic: it is semisimplicity together with reducedness of the
quotient by the Jacobson radical.
Basicness is invariant under ring equivalence. A ring equivalence carries the Jacobson radical onto the Jacobson radical, hence descends to an equivalence of the quotients, along which both semisimplicity and reducedness transport.
A ring is basic exactly when its quotient by the Jacobson radical is a finite product of
division rings. This is TauCeti.isReduced_iff_pi_divisionRing, read at that quotient; the
semisimplicity asked for by the definition is what makes the criterion applicable, and it comes
back from a product of division rings, each of which is a semisimple ring.
A ring with semisimple quotient by its Jacobson radical is basic exactly when that quotient
is reduced. The semisimplicity half of TauCeti.IsBasic is then automatic and only reducedness
is a condition. This covers every Artinian, and more generally every semiprimary, ring, in
particular every finite-dimensional algebra over a field.
A commutative ring with semisimple quotient by its Jacobson radical is basic, a commutative semisimple ring being reduced. This covers every commutative Artinian ring, in particular every finite-dimensional commutative algebra over a field.