The truncated polynomial algebra R[X]/(Xⁿ)

Mathlib builds AdjoinRoot f for any polynomial and, for a monic f, its power basis AdjoinRoot.powerBasis'. It does not record what the quotient by a power of X looks like. This file does: the class of X is nilpotent, and over a local ring R the algebra R[X]/(Xⁿ) is again local when n ≠ 0.

Locality is the useful form of the statement, because it is what pins the idempotents: through TauCeti.IsLocalRing.eq_zero_or_eq_one_of_isIdempotentElem a truncated polynomial algebra has no idempotent besides 0 and 1. That is exactly the input to the indecomposability of a nilpotent Jordan block, whose endomorphism algebra is k[X]/(Xⁿ).

The other half of that indecomposability argument -- that an endomorphism of the Jordan block is multiplication by an element of k[X]/(Xⁿ) -- needs nothing about Xⁿ beyond monicity, so it is stated for an arbitrary monic relator and lives with the rest of the general AdjoinRoot material, as AdjoinRoot.eq_mulRight_of_root_mul in TauCeti.RingTheory.AdjoinRoot.Basic.

Main results

• TauCeti.isNilpotent_root_X_pow: the class of X is nilpotent in R[X]/(Xⁿ).
• TauCeti.isLocalRing_adjoinRoot_X_pow: over a local ring R, so is R[X]/(Xⁿ) for n ≠ 0.

The dimension of R[X]/(Xⁿ) over R is not recorded here: AdjoinRoot f is by definition R[X] ⧸ (f), so Mathlib's finrank_quotient_span_eq_natDegree over a field, and finrank_quotient_span_eq_natDegree' for a monic relator over a ring, already give it.

Implementation notes

The evaluation R[X]/(Xⁿ) → R reading off the constant term is AdjoinRoot.lift of the identity of R at the root 0, and AdjoinRoot.lift_mk computes it on a class. It is a step in the proof of locality rather than API, so the two lemmas phrased against that unnamed map -- that its kernel consists of nilpotents, and that an element it sends to a unit is a unit -- are private.

Locality is proved from IsLocalRing.of_isUnit_or_isUnit_one_sub_self, splitting an element as its constant term plus an element of the kernel: the constant term is a unit or its complement is (IsLocalRing.isUnit_or_isUnit_one_sub_self in R), and adding a nilpotent to a unit leaves a unit (IsNilpotent.isUnit_add_left_of_commute). Nontriviality, which that criterion needs, is RingHom.domain_nontrivial applied to the constant-term map, R itself being nontrivial.

Everything is stated over a commutative ring; locality of course asks in addition that R be local, which for the base field of the intended application is automatic.

Locality genuinely needs the hypothesis n ≠ 0: R[X]/(X⁰) is the zero ring, which is not local.

theorem TauCeti.isNilpotent_root_X_pow {R : Type u_1} [CommRing R] (n : ℕ) : IsNilpotent (AdjoinRoot.root (Polynomial.X ^ n))

The class of X is nilpotent in R[X]/(Xⁿ): its n-th power vanishes.

instance TauCeti.isLocalRing_adjoinRoot_X_pow {R : Type u_1} [CommRing R] [IsLocalRing R] (n : ℕ) [NeZero n] : IsLocalRing (AdjoinRoot (Polynomial.X ^ n))

The truncated polynomial algebra R[X]/(Xⁿ) over a local ring is local when n ≠ 0.