Unramifiedness of a local algebra at its maximal ideal

Algebra.IsUnramifiedAt R q is formal unramifiedness over R of the localization of the ambient algebra at the prime q. When the ambient algebra S is already local and q is its maximal ideal, that localization is S itself, because every element outside the maximal ideal is already a unit. This file records the resulting equivalence, which is what lets a formal unramifiedness statement about a local ring be read by Mathlib's unramified-locus API, and conversely.

When the maximal ideal of S is generated by that of R — as it is for a formally unramified extension, by Algebra.FormallyUnramified.map_maximalIdeal — reduction modulo it loses no generators: the residues of a subset of S span the residue field of S over that of R exactly when the subset spans S over R. This is Mathlib's IsLocalRing.quotient_span_eq_top_iff_span_eq_top read through that generation, and the module-level companion of Mathlib's IsLocalRing.adjoin_residue_eq_top_iff_adjoin_eq_top, which says the same for generation as an algebra by a single element.

Main results

• TauCeti.isUnramifiedAt_maximalIdeal_iff: a local R-algebra is unramified at its maximal ideal exactly when it is formally unramified over R.
• TauCeti.IsLocalRing.span_residue_image_eq_top_iff_span_eq_top: if the maximal ideal of a module-finite local extension is generated by that of the base, then the residues of a subset span the residue extension exactly when the subset spans.

theorem TauCeti.isUnramifiedAt_maximalIdeal_iff (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing S] : Algebra.IsUnramifiedAt R (IsLocalRing.maximalIdeal S) ↔ Algebra.FormallyUnramified R S

A local R-algebra is unramified at its maximal ideal exactly when it is formally unramified over R: localizing a local ring at its maximal ideal inverts only units.

theorem TauCeti.IsLocalRing.span_residue_image_eq_top_iff_span_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing S] [IsLocalRing R] [IsLocalHom (algebraMap R S)] [Module.Finite R S] (h : Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) = IsLocalRing.maximalIdeal S) {s : Set S} : Submodule.span (IsLocalRing.ResidueField R) (⇑(IsLocalRing.residue S) '' s) = ⊤ ↔ Submodule.span R s = ⊤

A subset of a finite local extension spans it exactly when its residues span the residue extension, provided the maximal ideal of S is generated by the maximal ideal of R — as it is when S is formally unramified over R, by Algebra.FormallyUnramified.map_maximalIdeal.