theorem pderiv_X_pow {k : Type u_1} [CommRing k] {σ : Type u_2} [DecidableEq σ] (i j : σ) (d : ℕ) : (MvPolynomial.pderiv i) (MvPolynomial.X j ^ d) = if i = j then ↑d * MvPolynomial.X j ^ (d - 1) else 0

Partial derivative of a pure power of a variable: ∂_i (X_j^d) = d·X_j^{d-1} if i = j, otherwise 0.

theorem homogeneous_euler_vanishing {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (d : ℕ) (hf : f.IsHomogeneous d) (x : Fin (n + 1) → k) (hpd : ∀ (i : Fin (n + 1)), (MvPolynomial.eval x) ((MvPolynomial.pderiv i) f) = 0) : ↑d * (MvPolynomial.eval x) f = 0

Euler's identity: for a homogeneous polynomial f of degree d, the sum ∑ xᵢ ∂_i f = d·f. If all partials vanish at x, then d · f(x) = 0.

theorem homogeneous_singular_implies_zero {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (d : ℕ) (hf : f.IsHomogeneous d) (hd : ↑d ≠ 0) (x : Fin (n + 1) → k) (hpd : ∀ (i : Fin (n + 1)), (MvPolynomial.eval x) ((MvPolynomial.pderiv i) f) = 0) : (MvPolynomial.eval x) f = 0

When d ≠ 0 in k, vanishing of all partial derivatives at x forces f(x) = 0 for a homogeneous polynomial of degree d.

def IsSingularZero {k : Type u_1} [CommRing k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (x : Fin (n + 1) → k) : Prop

A point x is a singular zero of f if f(x) = 0 and all partial derivatives vanish at x. These are the singular points of the hypersurface V(f).

theorem singular_zero_iff_partials_vanish {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (d : ℕ) (hf : f.IsHomogeneous d) (hd : ↑d ≠ 0) (x : Fin (n + 1) → k) : IsSingularZero f x ↔ ∀ (i : Fin (n + 1)), (MvPolynomial.eval x) ((MvPolynomial.pderiv i) f) = 0

For a homogeneous polynomial of degree d with d ≠ 0 in k, being a singular zero is equivalent to all partial derivatives vanishing (Euler's identity makes f(x) = 0 automatic).

noncomputable def fermatPoly (k : Type u_1) [CommSemiring k] (n d : ℕ) : MvPolynomial (Fin (n + 1)) k

The Fermat polynomial of degree d in n+1 variables: x₀^d + x₁^d + … + xₙ^d.

theorem fermatPoly_isHomogeneous (k : Type u_1) [CommSemiring k] (n d : ℕ) : (fermatPoly k n d).IsHomogeneous d

The Fermat polynomial of degree d is homogeneous of degree d.

theorem pderiv_fermatPoly {k : Type u_1} [CommRing k] {n : ℕ} (d : ℕ) (i : Fin (n + 1)) : (MvPolynomial.pderiv i) (fermatPoly k n d) = ↑d * MvPolynomial.X i ^ (d - 1)

Partial derivative of the Fermat polynomial: ∂_i (Σ x_j^d) = d · x_i^{d-1}.

theorem fermat_no_nontrivial_singular {k : Type u_1} [Field k] {n d : ℕ} (hd : ↑d ≠ 0) (hd2 : 2 ≤ d) (x : Fin (n + 1) → k) (hx : x ≠ 0) (hpd : ∀ (i : Fin (n + 1)), (MvPolynomial.eval x) ((MvPolynomial.pderiv i) (fermatPoly k n d)) = 0) : False

The Fermat hypersurface of degree d ≥ 2 (with d ≠ 0 in k) has no nonzero singular points, providing an explicit smooth member of the family of degree-d hypersurfaces.

theorem discriminant_locus_proper {k : Type u_1} [Field k] {n d : ℕ} (hd : ↑d ≠ 0) (hd2 : 2 ≤ d) : ¬∀ (f : MvPolynomial (Fin (n + 1)) k), f.IsHomogeneous d → ∃ (x : Fin (n + 1) → k), x ≠ 0 ∧ IsSingularZero f x

The discriminant locus (where the hypersurface is singular) is a proper subset of the space of degree-d homogeneous polynomials: not every such polynomial is singular.

theorem bertini_smooth_exists {k : Type u_1} [Field k] {n d : ℕ} (hd : ↑d ≠ 0) (hd2 : 2 ≤ d) : ∃ (f : MvPolynomial (Fin (n + 1)) k), f.IsHomogeneous d ∧ ∀ (x : Fin (n + 1) → k), x ≠ 0 → ¬∀ (i : Fin (n + 1)), (MvPolynomial.eval x) ((MvPolynomial.pderiv i) f) = 0

Existence of a smooth degree-d hypersurface: there is a homogeneous polynomial of degree d whose partial derivatives do not all vanish simultaneously at any nonzero point. The Fermat polynomial provides such an example.

theorem smooth_hypersurface_nonempty {k : Type u_1} [Field k] {n d : ℕ} (hd : ↑d ≠ 0) (hd2 : 2 ≤ d) : ∃ (f : MvPolynomial (Fin (n + 1)) k), f.IsHomogeneous d ∧ ∀ (x : Fin (n + 1) → k), x ≠ 0 → ¬IsSingularZero f x

The space of smooth hypersurfaces of degree d ≥ 2 is non-empty: there exists a homogeneous degree-d polynomial with no nonzero singular zeros.

def discriminantLocus (k : Type u_1) [Field k] (n d : ℕ) : Set (MvPolynomial (Fin (n + 1)) k)

The discriminant locus: the set of degree-d homogeneous polynomials whose hypersurface has a singular point.

theorem isSingularZero_iff {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (x : Fin (n + 1) → k) : IsSingularZero f x ↔ (MvPolynomial.eval x) f = 0 ∧ ∀ (i : Fin (n + 1)), (MvPolynomial.eval x) ((MvPolynomial.pderiv i) f) = 0

Unfolding lemma for IsSingularZero.

theorem discriminantLocus_ne_univ (k : Type u_1) [Field k] (n d : ℕ) (hd : ↑d ≠ 0) (hd2 : 2 ≤ d) : discriminantLocus k n d ≠ Set.univ

The discriminant locus is a proper subset of the space of homogeneous polynomials of degree d ≥ 2: it does not contain the Fermat polynomial.

theorem vanishing_at_point_subspace {k : Type u_1} [Field k] {n : ℕ} (x : Fin (n + 1) → k) (f g : MvPolynomial (Fin (n + 1)) k) (c : k) : (MvPolynomial.eval x) f = 0 → (MvPolynomial.eval x) g = 0 → (MvPolynomial.eval x) (f + c • g) = 0

The vanishing condition f(x) = 0 is preserved by k-linear combinations.

theorem singular_at_point_linear {k : Type u_1} [Field k] {n : ℕ} (x : Fin (n + 1) → k) (f g : MvPolynomial (Fin (n + 1)) k) (c : k) : IsSingularZero f x → IsSingularZero g x → IsSingularZero (f + c • g) x

The set of polynomials having x as a singular zero is closed under linear combinations: if f and g are both singular at x, then so is f + c·g.

theorem bertini_generic_smooth {k : Type u_1} [Field k] {n d : ℕ} (hd : ↑d ≠ 0) (hd2 : 2 ≤ d) : (∃ (f : MvPolynomial (Fin (n + 1)) k), f.IsHomogeneous d ∧ ∀ (x : Fin (n + 1) → k), x ≠ 0 → ¬IsSingularZero f x) ∧ ∀ (x : Fin (n + 1) → k) (f g : MvPolynomial (Fin (n + 1)) k) (c : k), IsSingularZero f x → IsSingularZero g x → IsSingularZero (f + c • g) x

Bertini generic smoothness ingredients: there exists a smooth degree-d hypersurface (e.g. the Fermat polynomial), and the locus of polynomials singular at a fixed point is a linear subspace. Together these support the standard genericity argument.

theorem length_additive_submodule {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) : Module.length R M = Module.length R ↥N + Module.length R (M ⧸ N)

Additivity of length on short exact sequences from a submodule: length(M) = length(N) + length(M/N).

theorem length_additive_exact {R : Type u_1} [Ring R] {N : Type u_2} {M : Type u_3} {P : Type u_4} [AddCommGroup N] [AddCommGroup M] [AddCommGroup P] [Module R N] [Module R M] [Module R P] (f : N →ₗ[R] M) (g : M →ₗ[R] P) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (hex : Function.Exact ⇑f ⇑g) : Module.length R M = Module.length R N + Module.length R P

Additivity of length on an arbitrary short exact sequence 0 → N → M → P → 0: length(M) = length(N) + length(P).

theorem length_finite_of_artinian_noetherian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] : Module.length R M ≠ ⊤

A module that is both Artinian and Noetherian has finite length.

def K0LengthRelation (R : Type u_1) [Ring R] (M : Type u_2) (M' : Type u_3) [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] : Prop

Two R-modules are equivalent in K₀ (with the length map) if they have the same length.

theorem degree_map_respects_iso (R : Type u_1) [Ring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) : Module.length R M = Module.length R N

Length is invariant under R-linear isomorphism.

theorem degree_map_wellDefined_on_K0 (R : Type u_1) [Ring R] {N : Type u_2} {M : Type u_3} {P : Type u_4} [AddCommGroup N] [AddCommGroup M] [AddCommGroup P] [Module R N] [Module R M] [Module R P] (f : N →ₗ[R] M) (g : M →ₗ[R] P) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (hex : Function.Exact ⇑f ⇑g) : Module.length R M = Module.length R N + Module.length R P

The length map descends to a well-defined map on K₀: it is additive on short exact sequences.

theorem degree_map_additive_prod (R : Type u_1) [Ring R] (M : Type u_2) (N : Type u_3) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : Module.length R (M × N) = Module.length R M + Module.length R N

Length is additive on direct products: length(M × N) = length(M) + length(N).

theorem degree_map_finite (R : Type u_1) [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] : Module.length R M ≠ ⊤

Length is finite for any module that is both Artinian and Noetherian.

theorem degree_map_zero (R : Type u_1) [Ring R] : Module.length R PUnit.{1} = 0

The zero module has length 0.

theorem degree_map_simple (R : Type u_1) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] [IsSimpleModule R M] : Module.length R M = 1

A simple R-module has length 1.