theorem rank_kahler_polynomial (k : Type u) [Field k] (n : ℕ) : Module.finrank (MvPolynomial (Fin (n + 1)) k) Ω[MvPolynomial (Fin (n + 1)) k⁄k] = n + 1

The module of Kähler differentials of k[x₀, …, x_n] over k is free of rank n + 1.

instance kahler_mvpoly_finite (k : Type u) [Field k] (n : ℕ) : Module.Finite (MvPolynomial (Fin (n + 1)) k) Ω[MvPolynomial (Fin (n + 1)) k⁄k]

The Kähler differential module is finitely generated.

theorem det_kahler_rank_one (k : Type u) [Field k] (n : ℕ) : Module.finrank (MvPolynomial (Fin (n + 1)) k) ↥(⋀[MvPolynomial (Fin (n + 1)) k]^(n + 1) Ω[MvPolynomial (Fin (n + 1)) k⁄k]) = 1

The determinant (top exterior power) of the Kähler differential module is free of rank 1, giving the canonical bundle of affine (n+1)-space.

theorem exterior_power_kahler_rank (k : Type u) [Field k] (n p : ℕ) : Module.finrank (MvPolynomial (Fin (n + 1)) k) ↥(⋀[MvPolynomial (Fin (n + 1)) k]^p Ω[MvPolynomial (Fin (n + 1)) k⁄k]) = (n + 1).choose p

The p-th exterior power of the Kähler differential module has rank (n+1 choose p).

theorem canonical_bundle_free (k : Type u) [Field k] (n : ℕ) : Module.Free (MvPolynomial (Fin (n + 1)) k) ↥(⋀[MvPolynomial (Fin (n + 1)) k]^(n + 1) Ω[MvPolynomial (Fin (n + 1)) k⁄k])

The canonical bundle of A^{n+1}_k (top exterior power of Kähler differentials) is free.

noncomputable def exteriorPowerKahlerBasis (k : Type u) [Field k] (n : ℕ) : Module.Basis (Fin 1) (MvPolynomial (Fin (n + 1)) k) ↥(⋀[MvPolynomial (Fin (n + 1)) k]^(n + 1) Ω[MvPolynomial (Fin (n + 1)) k⁄k])

A basis (of cardinality 1) for the top exterior power of Kähler differentials.

noncomputable def canonicalBundleLinearEquiv (k : Type u) [Field k] (n : ℕ) : ↥(⋀[MvPolynomial (Fin (n + 1)) k]^(n + 1) Ω[MvPolynomial (Fin (n + 1)) k⁄k]) ≃ₗ[MvPolynomial (Fin (n + 1)) k] Fin 1 → MvPolynomial (Fin (n + 1)) k

Linear equivalence between the canonical bundle of A^{n+1}_k and the structure sheaf (rank-one free module), arising from the chosen basis.

theorem canonical_bundle_free_rank_one (k : Type u) [Field k] (n : ℕ) : Module.Free (MvPolynomial (Fin (n + 1)) k) ↥(⋀[MvPolynomial (Fin (n + 1)) k]^(n + 1) Ω[MvPolynomial (Fin (n + 1)) k⁄k]) ∧ Module.finrank (MvPolynomial (Fin (n + 1)) k) ↥(⋀[MvPolynomial (Fin (n + 1)) k]^(n + 1) Ω[MvPolynomial (Fin (n + 1)) k⁄k]) = 1

Combined statement: the canonical bundle of A^{n+1}_k is free of rank one.