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.

Main declarations

• TauCeti.AlgebraicGeometry.isRegularLocalRing_stalk_of_isRegularRing
• TauCeti.AlgebraicGeometry.isRegularRing_iff_isRegularLocalRing_stalk
• TauCeti.AlgebraicGeometry.isRegularLocalRing_stalk_Spec
• TauCeti.AlgebraicGeometry.isRegularRing_iff_isRegularLocalRing_stalk_Spec
• TauCeti.AlgebraicGeometry.isRegularLocalRing_stalk_iff_of_isOpenImmersion

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.

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.

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.

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.

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.