Primitive idempotents #
An idempotent e of a ring A is primitive when it is nonzero and cannot be split: there is
no way to write e = e₁ + e₂ with e₁ and e₂ nonzero orthogonal idempotents. Primitive
idempotents are the atoms out of which a decomposition of 1 into orthogonal idempotents is
assembled, and the reason they matter is the theorem proved here: e is primitive exactly when
the left ideal Ae is an indecomposable module.
Splitting e is the same as finding an idempotent strictly between 0 and e in the corner ring
eAe, and that reformulation (TauCeti.isPrimitiveIdempotent_iff_eq_zero_or_eq) is what both the
module characterization and the applications consume: the idempotents f with ef = fe = f are
exactly the idempotents of eAe, and each of them splits e as f + (e - f).
Mathlib has IsIdempotentElem, orthogonal families of idempotents
(Mathlib/RingTheory/Idempotents.lean) and the complete orthogonal decompositions of 1 they
generate, but no notion of a primitive idempotent and nothing connecting an idempotent to the
indecomposability of the left ideal it generates.
Main definitions #
TauCeti.IsPrimitiveIdempotent e:eis a nonzero idempotent admitting no decompositione = e₁ + e₂into nonzero orthogonal idempotents.
Main results #
TauCeti.isPrimitiveIdempotent_iff_eq_zero_or_eq: primitivity read in the corner ring, as the statement that0andeare the only idempotentsfwithef = fe = f.TauCeti.isPrimitiveIdempotent_iff_isIndecomposableModule: an idempotent is primitive exactly when the left ideal it generates is an indecomposable module. Both directions run along one dictionary: an idempotent of the corner ring acts onAeby right multiplication, and every endomorphism ofAeis right multiplication by its value ate(TauCeti.coe_apply_eq_mul_apply_generator).TauCeti.isPrimitiveIdempotent_iff_isLocalRing_end: for a left idealAeof finite length, primitivity ofeis the locality ofEnd (Ae); this is Fitting's lemma (TauCeti.isIndecomposableModule_iff_isLocalRing_end) read through the previous theorem.TauCeti.isPrimitiveIdempotent_one_iffandTauCeti.isPrimitiveIdempotent_one:1is primitive exactly when the ring has no idempotents besides0and1, which holds in a local ring.
Implementation notes #
The definition is the textbook one — no decomposition into two nonzero orthogonal idempotents —
rather than the corner-ring reformulation, which is derived. Keeping the two apart matters because
the derivation subtracts: the definition, the sufficient condition
TauCeti.isPrimitiveIdempotent_of_eq_zero_or_eq and the transport
TauCeti.IsPrimitiveIdempotent.map and the API for the left ideal Ae are stated over a semiring,
while the complement e - f that the reformulation needs, and everything after it, ask for a ring.
The left ideal generated by e is spelled Ideal.span {e} throughout. Ideal means left ideal
in Mathlib, which is the side the quiver-representation roadmap pins, its representations being
left modules. TauCeti.mem_span_singleton_iff_mul_eq_self says membership in Ae is exactly
x * e = x, which is the form every proof below uses; in particular e itself is a generator that
every element of Ae is a multiple of, on the nose rather than up to a sum.
References #
This implements the primitive-idempotent half of the finite-dimensional-algebra infrastructure of
Layer 3A in TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md ("a decomposition
of 1 into primitive orthogonal idempotents, the correspondence between primitive idempotents and
simple modules").
See I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.4.
An idempotent of a semiring is primitive when it is nonzero and is not the sum of two nonzero orthogonal idempotents.
- isIdempotentElem : IsIdempotentElem e
A primitive idempotent is an idempotent.
A primitive idempotent is nonzero; without this
0would be primitive in every ring.- eq_zero_or_eq_zero_of_add {e₁ e₂ : A} (h₁ : IsIdempotentElem e₁) (h₂ : IsIdempotentElem e₂) (h₁₂ : e₁ * e₂ = 0) (h₂₁ : e₂ * e₁ = 0) (hsum : e₁ + e₂ = e) : e₁ = 0 ∨ e₂ = 0
A primitive idempotent does not split: in every decomposition of it into two orthogonal idempotents one of the summands vanishes.
Instances For
A semiring carrying a primitive idempotent is nontrivial: that idempotent is nonzero.
An idempotent whose corner ring contains no idempotent besides 0 and e is primitive: both
summands of a decomposition of e lie in that corner ring.
Primitivity transports along a semiring isomorphism: a decomposition of σ e pulls back along
σ.symm to a decomposition of e.
The left ideal generated by an idempotent #
Membership in the left ideal generated by an idempotent: x lies in Ae exactly when e is a
right unit for x.
The generator of the left ideal it generates, as an element of that ideal. The body is not
exposed; consumers go through TauCeti.coe_spanSingletonGenerator and
TauCeti.smul_spanSingletonGenerator, never through the subtype.
Equations
Instances For
The generator of Ae, read in A, is e.
Every element of Ae is the generator scaled by itself.
A homomorphism out of Ae is right multiplication by its value at the generator. For an
endomorphism this is the dictionary between the corner ring eAe and End (Ae), and it is what
makes primitivity of e and indecomposability of Ae the same statement; the arbitrary target
ideal p is what TauCeti.RingTheory.Idempotents.Hom needs to compute Hom (Ae) (Af).
Primitivity seen in the corner ring. The only idempotents f with ef = fe = f, that is
the only idempotents of the corner ring eAe, are 0 and e: the complement e - f is an
idempotent orthogonal to f, and the two sum to e.
Primitivity of an idempotent, spelled entirely inside the corner ring eAe: it is nonzero and
the only idempotents f of eAe are 0 and e.
A primitive idempotent generates an indecomposable left ideal. An idempotent endomorphism
f of Ae is right multiplication by u = f e, which is an idempotent of the corner ring eAe;
primitivity forces u = 0 or u = e, that is, f = 0 or f = 1.
An idempotent generating an indecomposable left ideal is primitive. An idempotent f of
the corner ring eAe gives the idempotent endomorphism x ↦ x * f of Ae, which by
indecomposability is 0 or 1; evaluating at e gives f = 0 or f = e.
An idempotent is primitive exactly when the left ideal it generates is indecomposable.
An idempotent generating a simple left ideal is primitive: a simple module is indecomposable.
An idempotent generating a semisimple left ideal is primitive exactly when that ideal is simple. In particular this applies to every idempotent of a semisimple ring.
Primitivity as a local endomorphism ring. For a left ideal of finite length, e is
primitive exactly when End (Ae) is local; this is Fitting's lemma read through
TauCeti.isPrimitiveIdempotent_iff_isIndecomposableModule.
The unit #
1 is primitive exactly when the ring has no idempotents besides 0 and 1: the corner ring
of 1 is the whole ring.
1 is primitive in a local ring. An idempotent of a local ring is a unit or has a unit
complement, and in either case it is 1 or 0.