Geometrically regular algebras over a field

An algebra B over a field k is geometrically regular if B is Noetherian and the base change L ⊗[k] B is a regular ring for every finite purely inseparable extension L / k (Stacks, Definition 10.166.2, in the form of Lemma 10.166.1). Stacks, Lemma 10.166.1, shows that this is equivalent to regularity of L ⊗[k] B for every finitely generated field extension L / k; that equivalence is not proved here. Geometric regularity of the fibres is the condition defining regular ring maps, G-rings and excellent rings.

Regularity of B itself does not suffice: a nontrivial finite purely inseparable extension L / k is a field, hence regular, but L ⊗[k] L is not reduced, so L is not geometrically regular over k.

Main definitions and results

• TauCeti.Excellence.GeometricallyRegular k B: B is a geometrically regular k-algebra.
• TauCeti.Excellence.GeometricallyRegular.isRegularRing: a geometrically regular algebra is a regular ring.
• TauCeti.Excellence.GeometricallyRegular.isRegularRing_tensorProduct': the base change to a finite purely inseparable extension in any universe is a regular ring.
• AlgEquiv.geometricallyRegular: geometric regularity is invariant under isomorphisms of k-algebras.
• TauCeti.Excellence.GeometricallyRegular.of_smooth: a smooth k-algebra is geometrically regular; this covers k itself, the zero algebra and polynomial rings in finitely many variables.
• TauCeti.Excellence.GeometricallyRegular.of_isSeparable: a finite separable field extension is geometrically regular.
• TauCeti.Excellence.GeometricallyRegular.surjective_algebraMap_of_algHom: a nonzero geometrically regular k-algebra receives no k-algebra map from a nontrivial finite purely inseparable extension of k.
• TauCeti.Excellence.geometricallyRegular_iff_isSeparable: a finite purely inseparable extension is geometrically regular exactly when it is separable, that is, trivial.
• TauCeti.Excellence.geometricallyRegular_tensorProduct_iff_of_bijective: geometric regularity is unchanged by base change along an isomorphism of fields k → K.
• TauCeti.Excellence.GeometricallyRegular.of_isLocalization: a localization of a field is geometrically regular.
• TauCeti.Excellence.not_geometricallyRegular_trivSqZeroExt: the dual numbers k[ε]/(ε²) are not geometrically regular.

References

• The Stacks Project, Section 10.166 (Geometrically regular algebras), Lemma 10.166.1 and Definition 10.166.2.

class TauCeti.Excellence.GeometricallyRegular (k : Type u) (B : Type v) [Field k] [CommRing B] [Algebra k B] : Prop

An algebra B over a field k is geometrically regular if B is Noetherian and L ⊗[k] B is a regular ring for every finite purely inseparable field extension L / k (Stacks, Definition 10.166.2, in the form of Lemma 10.166.1). The extensions L range over the universe of k; GeometricallyRegular.isRegularRing_tensorProduct' removes that restriction.

• isNoetherianRing : IsNoetherianRing B

  A geometrically regular algebra is Noetherian.

• isRegularRing_tensorProduct (L : Type u) [Field L] [Algebra k L] [Module.Finite k L] [IsPurelyInseparable k L] : IsRegularRing (TensorProduct k L B)

  The base change of a geometrically regular algebra to a finite purely inseparable extension of the base field is a regular ring.

theorem TauCeti.Excellence.GeometricallyRegular.isRegularRing (k : Type u) {B : Type v} [Field k] [CommRing B] [Algebra k B] [GeometricallyRegular k B] : IsRegularRing B

A geometrically regular algebra is a regular ring: take L = k.

theorem TauCeti.Excellence.GeometricallyRegular.isRegularRing_tensorProduct' {k : Type u} {B : Type v} [Field k] [CommRing B] [Algebra k B] [GeometricallyRegular k B] (L : Type u_1) [Field L] [Algebra k L] [Module.Finite k L] [IsPurelyInseparable k L] : IsRegularRing (TensorProduct k L B)

The extensions L in the definition range over the universe of k, but the base change to a finite purely inseparable extension L / k in any universe is a regular ring: L has a copy Shrink L in the universe of k.

theorem AlgEquiv.geometricallyRegular {k : Type u} {B : Type v} {B' : Type w} [Field k] [CommRing B] [Algebra k B] [CommRing B'] [Algebra k B'] (e : B ≃ₐ[k] B') [TauCeti.Excellence.GeometricallyRegular k B] : TauCeti.Excellence.GeometricallyRegular k B'

Geometric regularity is invariant under isomorphisms of k-algebras.

@[instance 100]

instance TauCeti.Excellence.GeometricallyRegular.of_smooth {k : Type u} {B : Type v} [Field k] [CommRing B] [Algebra k B] [Algebra.Smooth k B] : GeometricallyRegular k B

A smooth algebra over a field is geometrically regular: its base change to any field is smooth over that field, hence regular.

@[instance 100]

instance TauCeti.Excellence.GeometricallyRegular.of_isSeparable {k : Type u} [Field k] (K : Type v) [Field K] [Algebra k K] [Module.Finite k K] [Algebra.IsSeparable k K] : GeometricallyRegular k K

A finite separable field extension is geometrically regular, being étale over the base.

theorem TauCeti.Excellence.GeometricallyRegular.surjective_algebraMap_of_algHom {k : Type u} {B : Type v} [Field k] [CommRing B] [Algebra k B] [GeometricallyRegular k B] [Nontrivial B] (L : Type u) [Field L] [Algebra k L] [Module.Finite k L] [IsPurelyInseparable k L] (f : L →ₐ[k] B) : Function.Surjective ⇑(algebraMap k L)

A nonzero geometrically regular k-algebra B receives no k-algebra map from a nontrivial finite purely inseparable extension L / k: if f : L →ₐ[k] B exists, then L = k. Indeed L ⊗[k] L embeds into the regular, hence reduced, ring L ⊗[k] B.

theorem TauCeti.Excellence.geometricallyRegular_iff_isSeparable {k : Type u} [Field k] (L : Type u) [Field L] [Algebra k L] [Module.Finite k L] [IsPurelyInseparable k L] : GeometricallyRegular k L ↔ Algebra.IsSeparable k L

A finite purely inseparable extension L / k is geometrically regular if and only if it is separable, that is, if and only if L = k.

theorem TauCeti.Excellence.not_geometricallyRegular_trivSqZeroExt (k : Type u) [Field k] : ¬GeometricallyRegular k (TrivSqZeroExt k k)

The dual numbers k[ε]/(ε²) over a field k are not geometrically regular: they are not even reduced.

theorem TauCeti.Excellence.geometricallyRegular_tensorProduct_iff_of_bijective {k : Type u} {K : Type w} [Field k] [Field K] [Algebra k K] (h : Function.Bijective ⇑(algebraMap k K)) (B : Type v) [CommRing B] [Algebra k B] : GeometricallyRegular K (TensorProduct k K B) ↔ GeometricallyRegular k B

Geometric regularity does not see an isomorphism of base fields: if algebraMap k K is bijective, then K ⊗[k] B is geometrically regular over K if and only if B is geometrically regular over k.

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

A localization of a field k is geometrically regular over k: it is either zero or k itself, and in both cases smooth over k.

Checks