theorem tangentDim_ge_krullDim (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : ringKrullDim R ≤ ↑(Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R))

Tangent space dimension bound (Lem 30): for a Noetherian local ring, the Krull dimension is at most the dimension of the cotangent space m/m² over the residue field, i.e. dim T*_x X ≥ dim_x X.

theorem smooth_iff_tangentDim_eq_krullDim (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ ↑(Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)) = ringKrullDim R

A Noetherian local ring is regular (smooth) iff the dimension of its cotangent space equals its Krull dimension.

theorem tangentDim_gt_krullDim_of_not_smooth (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (h : ¬IsRegularLocalRing R) : ringKrullDim R < ↑(Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R))

At a non-smooth (non-regular) point, the cotangent space dimension is strictly greater than the Krull dimension.

theorem tangentSpace_dim_characterizes_smoothness (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : ringKrullDim R ≤ ↑(Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)) ∧ (IsRegularLocalRing R ↔ ↑(Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)) = ringKrullDim R)

Combined statement: the cotangent dimension always upper-bounds the Krull dimension, with equality characterizing smoothness.