Documentation

TauCeti.AlgebraicGeometry.Scheme.Regular.LocalRing

Regular local rings of schemes #

On an affine open with Noetherian ring of sections, regularity of that ring is equivalent to regularity of the local rings at every point of the open. In particular, a Noetherian ring is regular exactly when the local rings of its spectrum are regular. Open immersions identify local rings, so they preserve and reflect their regularity.

More generally, a flat, formally unramified morphism f : X ⟢ Y locally of finite type (for instance an Γ©tale morphism) induces at each point x a flat local homomorphism π’ͺ_{Y, f x} ⟢ π’ͺ_{X, x} under which the maximal ideal of the source generates the maximal ideal of the target, and which preserves and reflects Noetherianity (AlgebraicGeometry.Scheme.Hom.map_maximalIdeal_stalkMap_of_formallyUnramified, AlgebraicGeometry.Scheme.Hom.isNoetherianRing_stalk_iff_of_flat_of_locallyOfFiniteType). Between Noetherian local rings such a homomorphism both preserves and reflects regularity (TauCeti.isRegularLocalRing_iff_of_flat_of_map_maximalIdeal_eq).

Main declarations #

source
theorem TauCeti.AlgebraicGeometry.isRegularLocalRing_stalk_of_isRegularRing {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) [IsRegularRing ↑(X.presheaf.obj (Opposite.op U))] {x : β†₯X} (hx : x ∈ U) :
IsRegularLocalRing ↑(X.presheaf.stalk x)

If the sections over an affine open U form a regular ring, the local rings at the points of U are regular.

source
theorem TauCeti.AlgebraicGeometry.isRegularRing_iff_isRegularLocalRing_stalk {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) [IsNoetherianRing ↑(X.presheaf.obj (Opposite.op U))] :
IsRegularRing ↑(X.presheaf.obj (Opposite.op U)) ↔ βˆ€ x ∈ U, IsRegularLocalRing ↑(X.presheaf.stalk x)

The sections over an affine open U with Noetherian ring of sections form a regular ring exactly when the local rings at the points of U are regular.

source
instance TauCeti.AlgebraicGeometry.isRegularLocalRing_stalk_Spec (R : CommRingCat) [IsRegularRing ↑R] (x : β†₯(AlgebraicGeometry.Spec R)) :
IsRegularLocalRing ↑((AlgebraicGeometry.Spec R).presheaf.stalk x)

The local rings of the spectrum of a regular ring are regular.

source
theorem TauCeti.AlgebraicGeometry.isRegularRing_iff_isRegularLocalRing_stalk_Spec (R : CommRingCat) [IsNoetherianRing ↑R] :
IsRegularRing ↑R ↔ βˆ€ (x : β†₯(AlgebraicGeometry.Spec R)), IsRegularLocalRing ↑((AlgebraicGeometry.Spec R).presheaf.stalk x)

A Noetherian ring is regular exactly when the local rings of its spectrum are regular.

source
theorem TauCeti.AlgebraicGeometry.isRegularLocalRing_stalk_Spec_iff (R : CommRingCat) (x : PrimeSpectrum ↑R) :
IsRegularLocalRing ↑((AlgebraicGeometry.Spec R).presheaf.stalk x) ↔ IsRegularLocalRing (Localization.AtPrime x.asIdeal)

The local ring of Spec R at x is the localization of R at the prime x (Mathlib AlgebraicGeometry.Spec.stalkIso), so one is regular exactly when the other is.

source
theorem TauCeti.AlgebraicGeometry.isRegularLocalRing_stalk_iff_of_isOpenImmersion {X Y : AlgebraicGeometry.Scheme} (f : X ⟢ Y) [AlgebraicGeometry.IsOpenImmersion f] (x : β†₯X) :
IsRegularLocalRing ↑(Y.presheaf.stalk (f x)) ↔ IsRegularLocalRing ↑(X.presheaf.stalk x)

An open immersion f : X ⟢ Y identifies the local ring of X at x with the local ring of Y at f x, so one is regular exactly when the other is.

source
theorem AlgebraicGeometry.Scheme.Hom.isRegularLocalRing_stalk_iff_of_flat_of_formallyUnramified {X Y : Scheme} (f : X ⟢ Y) [Flat f] [FormallyUnramified f] [LocallyOfFiniteType f] (x : β†₯X) :
IsRegularLocalRing ↑(Y.presheaf.stalk (f x)) ↔ IsRegularLocalRing ↑(X.presheaf.stalk x)

A flat, formally unramified morphism f : X ⟢ Y locally of finite type (in particular an étale morphism) preserves and reflects regularity of local rings: the local ring of Y at f x is regular exactly when the local ring of X at x is.