theorem smooth_subvariety_char (k : Type u_1) [Field k] (R : Type u_2) [CommRing R] [Algebra k R] [Algebra.FormallySmooth k R] (I : Ideal R) : Algebra.FormallySmooth k (R ⧸ I) ↔ ∃ (l : TensorProduct R (R ⧸ I) Ω[R⁄k] →ₗ[R] (RingHom.ker (algebraMap R (R ⧸ I))).Cotangent), l ∘ₗ KaehlerDifferential.kerCotangentToTensor k R (R ⧸ I) = LinearMap.id

Smoothness of a closed subscheme: if R is a formally smooth k-algebra and I ⊆ R, then the quotient R/I is formally smooth over k iff the natural map I/I² → Ω_{R/k} ⊗_R R/I admits a left-inverse. Geometrically: a closed subscheme of a smooth scheme is smooth iff its conormal sequence splits.