Regular ring maps

A ring map R → B is regular if B is flat over R and, for every prime p of R, the fibre κ(p) ⊗[R] B is a geometrically regular κ(p)-algebra (Stacks, Definition 15.42.1). This is the condition imposed on the formal fibres of G-rings, and hence of quasi-excellent and excellent rings.

Main definitions and results

• TauCeti.Excellence.RegularAlgebraMap R B: the structure map R → B is a regular ring map.
• TauCeti.Excellence.regularAlgebraMap_iff_geometricallyRegular: over a field k, a regular k-algebra is the same as a geometrically regular one.
• TauCeti.Excellence.RegularAlgebraMap.of_smooth: smooth algebras are regular, since their fibres are smooth over the residue fields.
• TauCeti.Excellence.RegularAlgebraMap.of_isLocalization: localizations are regular, for instance R → R_p and ℤ → ℚ.
• AlgEquiv.regularAlgebraMap: regularity is invariant under isomorphisms of R-algebras.
• TauCeti.Excellence.RegularAlgebraMap.localization_base: an algebra regular over R is regular over any localization of R through which its structure map factors, for instance over a ring isomorphic to R.
• TauCeti.Excellence.RegularAlgebraMap.isRegularRing: a Noetherian regular algebra over a regular ring is a regular ring.
• RingEquiv.regularAlgebraMap_adicCompletion: regularity of the completion map A → Â along an ideal is transported along a ring isomorphism matching the ideals.
• Ideal.regularAlgebraMap_adicCompletion_of_isAdicComplete: the completion map of a ring along an ideal it is complete for is regular.

References

• The Stacks Project, Section 15.42 (Regular ring maps), Definition 15.42.1.

class TauCeti.Excellence.RegularAlgebraMap (R : Type u) (B : Type v) [CommRing R] [CommRing B] [Algebra R B] : Prop

An R-algebra B is a regular algebra, or R → B is a regular ring map, if B is flat over R and for every prime p of R the fibre κ(p) ⊗[R] B is geometrically regular over the residue field κ(p) (Stacks, Definition 15.42.1).

• flat : Module.Flat R B

  A regular algebra is flat.

• geometricallyRegular_fiber (p : Ideal R) [p.IsPrime] : GeometricallyRegular p.ResidueField (p.Fiber B)

  The fibre of a regular algebra over a prime of the base is geometrically regular over the residue field.

theorem TauCeti.Excellence.regularAlgebraMap_iff_geometricallyRegular (k : Type u) (B : Type v) [Field k] [CommRing B] [Algebra k B] : RegularAlgebraMap k B ↔ GeometricallyRegular k B

Over a field k, a regular k-algebra is the same as a geometrically regular one: flatness is automatic and the only fibre is over the zero ideal, whose residue field is k.

@[instance 100]

instance TauCeti.Excellence.RegularAlgebraMap.of_smooth {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B] [Algebra.Smooth R B] : RegularAlgebraMap R B

A smooth algebra is regular: it is flat, and its fibres are smooth over the residue fields, hence geometrically regular.

theorem TauCeti.Excellence.RegularAlgebraMap.of_isLocalization {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B] (M : Submonoid R) [IsLocalization M B] : RegularAlgebraMap R B

A localization of R is a regular R-algebra: it is flat, and its fibres are localizations of the residue fields.

instance TauCeti.Excellence.RegularAlgebraMap.localization {R : Type u} [CommRing R] (M : Submonoid R) : RegularAlgebraMap R (Localization M)

The localization Localization M is a regular R-algebra.

theorem AlgEquiv.regularAlgebraMap {R : Type u} {B : Type v} {B' : Type w} [CommRing R] [CommRing B] [Algebra R B] [CommRing B'] [Algebra R B'] (e : B ≃ₐ[R] B') [TauCeti.Excellence.RegularAlgebraMap R B] : TauCeti.Excellence.RegularAlgebraMap R B'

Regularity of an algebra is invariant under isomorphisms of R-algebras.

theorem TauCeti.Excellence.RegularAlgebraMap.localization_base {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B] {R' : Type u_1} [CommRing R'] [Algebra R R'] [Algebra R' B] [IsScalarTower R R' B] (M : Submonoid R) [IsLocalization M R'] [RegularAlgebraMap R B] : RegularAlgebraMap R' B

Regularity of an algebra passes to a localization of the base: if R' is a localization of R at M and B is an R'-algebra that is regular over R, then B is regular over R'. Taking M = IsUnit.submonoid R, this covers a ring R' isomorphic to R.

theorem TauCeti.Excellence.RegularAlgebraMap.isRegularRing {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B] [IsRegularRing R] [IsNoetherianRing B] [RegularAlgebraMap R B] : IsRegularRing B

A Noetherian regular algebra over a regular ring is a regular ring: its fibres are geometrically regular, hence regular.

Completion maps

theorem RingEquiv.regularAlgebraMap_adicCompletion {A : Type u} {A' : Type v} [CommRing A] [CommRing A'] (e : A ≃+* A') {I : Ideal A} {I' : Ideal A'} (he : Ideal.map e I = I') [TauCeti.Excellence.RegularAlgebraMap A (AdicCompletion I A)] : TauCeti.Excellence.RegularAlgebraMap A' (AdicCompletion I' A')

Regularity of the completion map A → Â along an ideal I is transported along a ring isomorphism e : A ≃+* A' carrying I onto I': then A' → Â' along I' is regular. For local rings and their maximal ideals, IsLocalRing.map_ringEquiv_maximalIdeal e supplies the hypothesis.

theorem Ideal.regularAlgebraMap_adicCompletion_of_isAdicComplete {A : Type u} [CommRing A] (I : Ideal A) [IsAdicComplete I A] : TauCeti.Excellence.RegularAlgebraMap A (AdicCompletion I A)

The completion map A → Â of a ring along an ideal I for which A is I-adically complete is regular, being an isomorphism.

Checks