Dimension and regularity at a rational point

For an augmentation f : A →ₐ[k] k, the Module.finrank of ker(f) / ker(f)² over k equals the Module.finrank of the local ring's cotangent space over its native residue field. When this local ring is Noetherian, this common value is its embedding dimension and bounds its Krull dimension, with equality exactly when the local ring is regular. These statements allow tangent-space calculations in the coordinate algebra to detect regularity of the affine scheme.

References

• M. F. Atiyah and I. G. Macdonald, Introduction to Commutative Algebra, Chapter 11.

@[simp]

theorem AlgHom.finrank_kernelCotangent_eq_finrank_residueFieldCotangent {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] (f : A →ₐ[k] k) : Module.finrank k (RingHom.ker ↑f).Cotangent = Module.finrank (IsLocalRing.ResidueField ↑((AlgebraicGeometry.Spec ↧A).presheaf.stalk (TauCeti.AlgHom.kernelPoint f))) (IsLocalRing.CotangentSpace ↑((AlgebraicGeometry.Spec ↧A).presheaf.stalk (TauCeti.AlgHom.kernelPoint f)))

The Module.finrank of the augmentation cotangent space over the ground field equals the Module.finrank of the local cotangent space over the native residue field.

theorem AlgHom.ringKrullDim_kernelStalk_le_finrank_kernelCotangent {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] (f : A →ₐ[k] k) [IsNoetherianRing ↑((AlgebraicGeometry.Spec ↧A).presheaf.stalk (TauCeti.AlgHom.kernelPoint f))] : ringKrullDim ↑((AlgebraicGeometry.Spec ↧A).presheaf.stalk (TauCeti.AlgHom.kernelPoint f)) ≤ ↑(Module.finrank k (RingHom.ker ↑f).Cotangent)

At a rational point with Noetherian local ring, local dimension is bounded by the dimension of the augmentation cotangent space.

theorem AlgHom.isRegularLocalRing_kernelStalk_iff {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] (f : A →ₐ[k] k) [IsNoetherianRing ↑((AlgebraicGeometry.Spec ↧A).presheaf.stalk (TauCeti.AlgHom.kernelPoint f))] : IsRegularLocalRing ↑((AlgebraicGeometry.Spec ↧A).presheaf.stalk (TauCeti.AlgHom.kernelPoint f)) ↔ ↑(Module.finrank k (RingHom.ker ↑f).Cotangent) = ringKrullDim ↑((AlgebraicGeometry.Spec ↧A).presheaf.stalk (TauCeti.AlgHom.kernelPoint f))

A Noetherian local ring at a rational point of an affine scheme is regular exactly when its dimension equals the dimension of the augmentation cotangent space.