theorem kaehlerDifferential_universalProperty (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] : Nonempty ((Ω[S⁄R] →ₗ[S] M) ≃ₗ[S] Derivation R S M)

Universal property of Kähler differentials (Def 34, Lec 18): S-linear maps Ω[S⁄R] →ₗ[S] M are in (S-linear) bijection with R-derivations Der R S M.

noncomputable def kaehlerDifferentialEquivDerivation (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] : (Ω[S⁄R] →ₗ[S] M) ≃ₗ[S] Derivation R S M

The explicit S-linear equivalence (Ω[S⁄R] →ₗ[S] M) ≃ₗ[S] Der R S M witnessing the universal property of Kähler differentials.

theorem kaehlerDifferential_lift_comp (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D' : Derivation R S M) : D'.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S) = D'

Existence half of the universal property: every derivation D' factors through the universal derivation d : S → Ω[S⁄R] via liftKaehlerDifferential.

theorem kaehlerDifferential_lift_unique (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (f g : Ω[S⁄R] →ₗ[S] M) (hf : f.compDer (KaehlerDifferential.D R S) = g.compDer (KaehlerDifferential.D R S)) : f = g

Uniqueness half of the universal property: two S-linear maps out of Ω[S⁄R] that agree on the image of the universal derivation are equal.

theorem kaehlerDifferential_span_range (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) = ⊤

The module of Kähler differentials Ω[S⁄R] is generated as an S-module by the image of the universal derivation d : S → Ω[S⁄R].

noncomputable def kaehlerDifferential_polynomial_equiv (k : Type u) [CommRing k] : Ω[Polynomial k⁄k] ≃ₗ[Polynomial k] Polynomial k

For the polynomial algebra k[X], the Kähler differentials are a free rank-one module: Ω[k[X]⁄k] ≃ₗ[k[X]] k[X], with dX corresponding to 1.

theorem kaehlerDifferential_polynomial_free (k : Type u) [CommRing k] : Module.Free (Polynomial k) Ω[Polynomial k⁄k]

Ω[k[X]⁄k] is a free k[X]-module (in fact free of rank one).

theorem kaehlerDifferential_polynomial_rank (k : Type u) [CommRing k] [Nontrivial k] : Module.finrank (Polynomial k) Ω[Polynomial k⁄k] = 1

The rank of Ω[k[X]⁄k] over k[X] is 1 whenever k is nontrivial.

theorem kaehlerDifferential_polynomial_D (k : Type u) [CommRing k] (P : Polynomial k) : (KaehlerDifferential.D k (Polynomial k)) P = Polynomial.derivative P • (KaehlerDifferential.D k (Polynomial k)) Polynomial.X

Explicit formula for the universal derivation on polynomials: dP = P' · dX, where P' is the usual formal derivative.

theorem kaehlerDifferential_mvPolynomial_free (k : Type u) [CommRing k] (σ : Type u_1) : Module.Free (MvPolynomial σ k) Ω[MvPolynomial σ k⁄k]

For the polynomial ring k[Xᵢ : i ∈ σ], the module Ω[k[σ]⁄k] is free as a k[σ]-module, with basis {dXᵢ}.

noncomputable def kaehlerDifferential_mvPolynomial_basis (k : Type u) [CommRing k] (σ : Type u_1) : Module.Basis σ (MvPolynomial σ k) Ω[MvPolynomial σ k⁄k]

Canonical basis {dXᵢ}ᵢ of Ω[k[σ]⁄k] as a free k[σ]-module indexed by σ.

theorem cotangentSequence_exact (R : Type u) [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] : Function.Exact ⇑(KaehlerDifferential.mapBaseChange R A B) ⇑(KaehlerDifferential.map R A B B)

Exactness of the relative cotangent sequence: B ⊗_A Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0 is exact at the middle term.

theorem cotangentSequence_surjective (R : Type u) [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] : Function.Surjective ⇑(KaehlerDifferential.map R A B B)

Surjectivity in the relative cotangent sequence: the map Ω[B⁄R] → Ω[B⁄A] is surjective.

theorem cotangentExactSequence_with_kernel (R : Type u) [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Exact ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ⇑(KaehlerDifferential.mapBaseChange R A B)

Conormal/cotangent exactness for a surjection A → B with kernel I: the sequence I/I² → B ⊗_A Ω[A⁄R] → Ω[B⁄R] is exact at the middle term.

theorem cotangent_mapBaseChange_surjective (R : Type u) [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Surjective ⇑(KaehlerDifferential.mapBaseChange R A B)

For a surjection A → B, the base-change map B ⊗_A Ω[A⁄R] → Ω[B⁄R] is itself surjective.

theorem proposition33_cotangent_exact_sequence (R : Type u) [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Exact ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ⇑(KaehlerDifferential.mapBaseChange R A B) ∧ Function.Surjective ⇑(KaehlerDifferential.mapBaseChange R A B)

Proposition 33 (first half): for a surjection A ↠ B with kernel I, the conormal sequence I/I² → B ⊗_A Ω[A⁄R] → Ω[B⁄R] → 0 is exact and the right map is surjective.

theorem proposition33_part2_short_exact (R : Type u) [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [Algebra.FormallySmooth R A] [Algebra.FormallySmooth R B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Injective ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ∧ Function.Exact ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ⇑(KaehlerDifferential.mapBaseChange R A B) ∧ Function.Surjective ⇑(KaehlerDifferential.mapBaseChange R A B)

Proposition 33 (second half): if both R → A and R → B are formally smooth and A ↠ B is surjective, then the conormal sequence 0 → I/I² → B ⊗_A Ω[A⁄R] → Ω[B⁄R] → 0 is short exact.

theorem proposition33_part2_conormal_rank {R : Type u} [CommRing R] {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [Algebra.FormallySmooth R A] [Algebra.FormallySmooth R B] (h : Function.Surjective ⇑(algebraMap A B)) (n m : ℕ) (hΩmid : Module.finrank B (TensorProduct A B Ω[A⁄R]) = n) (hΩB : Module.finrank B Ω[B⁄R] = n - m) : Module.finrank (A ⧸ RingHom.ker (algebraMap A B)) (RingHom.ker (algebraMap A B)).Cotangent = m

Numerical consequence of Proposition 33: the rank of the conormal module I/I² equals the difference between the ranks of B ⊗_A Ω[A⁄R] and Ω[B⁄R].

theorem cotangent_finite_over_R {R : Type u_1} [CommRing R] [IsNoetherianRing R] (I : Ideal R) : Module.Finite R I.Cotangent

For a Noetherian ring R, the cotangent module I/I² of any ideal I is finitely generated over R.

theorem cotangentSpace_finiteDimensional (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : FiniteDimensional (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)

For a Noetherian local ring R with maximal ideal 𝔪 and residue field κ, the Zariski cotangent space 𝔪/𝔪² is a finite-dimensional κ-vector space.

theorem cotangentSpace_zero_iff_field (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : Subsingleton (IsLocalRing.CotangentSpace R) ↔ IsField R

The cotangent space 𝔪/𝔪² of a Noetherian local ring vanishes if and only if the ring is a field.

theorem finrank_cotangentSpace_eq_zero_iff (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) = 0 ↔ IsField R

Numerical version: dim_κ (𝔪/𝔪²) = 0 iff R is a field.

theorem cotangentSpace_dim_le_one_iff_principal (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (IsLocalRing.maximalIdeal R)

The cotangent space has dimension at most one iff the maximal ideal is principal (equivalently, R is a DVR or a field).

theorem cotangentSpace_generators_iff_ideal_generators (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (s : Set ↥(IsLocalRing.maximalIdeal R)) : Submodule.span (IsLocalRing.ResidueField R) (⇑(IsLocalRing.maximalIdeal R).toCotangent '' s) = ⊤ ↔ Submodule.span R s = ⊤

Nakayama-type criterion: a set s ⊂ 𝔪 generates 𝔪 over R iff its image in 𝔪/𝔪² spans the cotangent space over the residue field.

theorem cotangentSpace_map_eq_top_iff (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {M : Submodule R ↥(IsLocalRing.maximalIdeal R)} : Submodule.map (IsLocalRing.maximalIdeal R).toCotangent M = ⊤ ↔ M = ⊤

Submodule version of Nakayama: a submodule M ≤ 𝔪 equals all of 𝔪 iff its image in the cotangent space is the whole space.