def BertiniVeronese.veroneseMonomialCount (n d : ℕ) : ℕ

The number of monomials of degree d in n+1 variables: C(n+d, d). This is the dimension of the space of degree-d forms used in the Veronese embedding.

def BertiniVeronese.veroneseEmbedDim (n d : ℕ) : ℕ

Dimension of the target projective space of the degree-d Veronese embedding of ℙⁿ.

theorem BertiniVeronese.veroneseMonomialCount_pos (n d : ℕ) : 0 < veroneseMonomialCount n d

There is always at least one monomial of given degree, so veroneseMonomialCount > 0.

theorem BertiniVeronese.choose_two_ge (n : ℕ) (hn : 1 ≤ n) : n + 2 ≤ (n + 2).choose 2

Combinatorial bound: for n ≥ 1, n + 2 ≤ C(n + 2, 2).

theorem BertiniVeronese.choose_add_ge_succ (n d : ℕ) (hd : 1 ≤ d) : n + 1 ≤ (n + d).choose d

For d ≥ 1, n + 1 ≤ C(n + d, d): ensures enough monomials to embed ℙⁿ.

theorem BertiniVeronese.choose_add_ge_add_two (n d : ℕ) (hd : 2 ≤ d) (hn : 1 ≤ n) : n + 2 ≤ (n + d).choose d

For d ≥ 2 and n ≥ 1, n + 2 ≤ C(n + d, d): the dimension gap needed for the Bertini dimension count via the Veronese embedding.

theorem BertiniVeronese.veroneseEmbedDim_ge (n d : ℕ) (hd : 1 ≤ d) : n ≤ veroneseEmbedDim n d

For d ≥ 1, the Veronese embedding dimension is at least n (so it is a genuine embedding, not a degeneration).

def BertiniVeronese.hypersurfaceParamDim (n d : ℕ) : ℕ

Dimension of the parameter space of degree-d hypersurfaces in ℙⁿ.

theorem BertiniVeronese.veronese_hypersurface_is_hyperplane (n d : ℕ) : hypersurfaceParamDim n d = veroneseEmbedDim n d

Via the Veronese embedding, a degree-d hypersurface in ℙⁿ becomes a hyperplane in the target projective space; the parameter spaces have the same dimension.

def BertiniVeronese.smoothnessConditionCount (n : ℕ) : ℕ

Number of conditions imposed by requiring smoothness at a fixed point: the value of f and the n partial derivatives, so n + 1 conditions.

theorem BertiniVeronese.bertini_veronese_dimension_count (n d : ℕ) (hd : 2 ≤ d) (hn : 1 ≤ n) : smoothnessConditionCount n ≤ hypersurfaceParamDim n d

The number of smoothness conditions (n + 1) does not exceed the dimension of the parameter space of degree-d hypersurfaces (for d ≥ 2, n ≥ 1).

theorem BertiniVeronese.incidence_variety_dim (n d : ℕ) (hd : 2 ≤ d) (hn : 1 ≤ n) : n + (hypersurfaceParamDim n d - smoothnessConditionCount n) < veroneseMonomialCount n d

The incidence variety (pairs (x, f) with f singular at x) has dimension strictly less than the total monomial count, giving room for a smooth hypersurface to exist generically.

theorem BertiniVeronese.generic_hypersurface_smooth_codim (n d : ℕ) (hd : 2 ≤ d) (hn : 1 ≤ n) : n + (hypersurfaceParamDim n d - smoothnessConditionCount n) + 1 ≤ hypersurfaceParamDim n d

Codimension count: the dimension of the incidence variety plus one is at most the parameter dimension, so the projection cannot be surjective and the generic fiber is smooth.

theorem BertiniVeronese.discriminant_codimension_pos (n d : ℕ) (hd : 2 ≤ d) (hn : 1 ≤ n) : 1 ≤ hypersurfaceParamDim n d - (n + (hypersurfaceParamDim n d - smoothnessConditionCount n))

The discriminant locus has positive codimension in the parameter space: there is a strict gap of at least 1.

theorem BertiniVeronese.generic_section_smooth_codim (n d k : ℕ) (hd : 2 ≤ d) (hk : k ≤ n) (hn : 1 ≤ n) : k + (hypersurfaceParamDim n d - (k + 1)) + 1 ≤ hypersurfaceParamDim n d

Analogous codimension count for the case of a smooth subvariety X ⊂ ℙⁿ of dimension k, needed to obtain smooth degree-d sections of X.

theorem BertiniVeronese.veronese_bertini_summary (n d : ℕ) (hd : 2 ≤ d) (hn : 1 ≤ n) : n + ((n + d).choose d - 1 - (n + 1)) < (n + d).choose d - 1 ∧ (n + d).choose d - 1 = veroneseEmbedDim n d ∧ n + 1 ≤ (n + d).choose d

Combined summary of the Veronese-based Bertini dimension count: the incidence variety has strictly smaller dimension than the parameter space, hypersurfaces of degree d correspond to hyperplanes via the Veronese embedding, and there are enough monomials.

@[reducible, inline]

abbrev HomogeneousPolys (k : Type) [Field k] (n d : ℕ) : Type

The space of homogeneous polynomials of degree d in n + 1 variables over k.

@[implicit_reducible]

instance zariskiTopologyHomogeneousPolys (k : Type) [Field k] (n d : ℕ) : TopologicalSpace (HomogeneousPolys k n d)

The Zariski topology on the space of degree-d homogeneous polynomials, generated by basic open sets where a specified monomial coefficient is nonzero.

def IsGenericProperty {α : Type u_1} [TopologicalSpace α] (P : α → Prop) : Prop

A property P holds generically on α if it holds on a dense open subset.

def IsSmooth_hypersurface {k : Type} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) : Prop

The hypersurface V(f) ⊂ ℙⁿ is smooth: at every nonzero point where all partial derivatives of f vanish, the value f(x) is nonzero (i.e. x is not on the hypersurface).

structure SmoothProjectiveVariety (k : Type) [Field k] (n : ℕ) : Type

A smooth projective subvariety of ℙⁿ: a finite collection of homogeneous defining polynomials such that at every nonzero point of the variety, the Jacobian condition holds.

• definingPolys : Finset (MvPolynomial (Fin (n + 1)) k)
• polysHomogeneous (p : MvPolynomial (Fin (n + 1)) k) : p ∈ self.definingPolys → ∃ (d : ℕ), p.IsHomogeneous d
• onVariety (x : Fin (n + 1) → k) : Prop
• isSmooth (x : Fin (n + 1) → k) : x ≠ 0 → self.onVariety x → ∀ (v : Fin (n + 1) → k), v ≠ 0 → (∀ p ∈ self.definingPolys, ∀ (i : Fin (n + 1)), (MvPolynomial.eval x) ((MvPolynomial.pderiv i) p) = 0) → False

def IsSmooth_intersection_variety {k : Type} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (X : SmoothProjectiveVariety k n) : Prop

The intersection X ∩ V(f) is smooth (relative to X): at every nonzero point of X with f(x) = 0, some partial derivative of f is nonzero.

def IsSmooth_intersection {k : Type} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (onX smoothX : (Fin (n + 1) → k) → Prop) : Prop

General version of smooth intersection: parameterized by predicates onX (point lies on X) and smoothX (point is a smooth point of X).

def veroneseMap {k : Type} [CommSemiring k] (n d : ℕ) (t : Fin (n + 1) → k) (I : { s : Fin (n + 1) →₀ ℕ // (s.sum fun (x : Fin (n + 1)) => id) = d }) : k

The Veronese map sending (t₀, …, tₙ) to the tuple of all degree-d monomials ∏ tⱼ^{Iⱼ}, indexed by exponent vectors I with |I| = d.

theorem smooth_hypersurface_implies_smooth_intersection {k : Type} [Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (hf : IsSmooth_hypersurface f) (X : SmoothProjectiveVariety k n) : IsSmooth_intersection_variety f X

If V(f) is a smooth hypersurface in ℙⁿ, then for any smooth projective subvariety X, the intersection X ∩ V(f) is smooth.

theorem bertini_theorem {k : Type} [Field k] [IsAlgClosed k] (n : ℕ) (hn : 1 ≤ n) (X : SmoothProjectiveVariety k n) : IsGenericProperty fun (H : HomogeneousPolys k n 1) => IsSmooth_intersection_variety (↑H) X

Bertini's theorem (Thm 22.1, Lec 22) over an algebraically closed field: for a smooth projective variety X ⊂ ℙⁿ, the generic hyperplane (degree-1 homogeneous polynomial) gives a smooth section.

noncomputable def veronese_image_smooth {k : Type} [Field k] [IsAlgClosed k] (n d : ℕ) (hd : 1 ≤ d) (hn : 1 ≤ n) (X : SmoothProjectiveVariety k n) : SmoothProjectiveVariety k (BertiniVeronese.veroneseMonomialCount n d - 1)

Image of a smooth projective variety X ⊂ ℙⁿ under the degree-d Veronese embedding into ℙ^(C(n+d,d)-1): still a smooth projective subvariety.

theorem veronese_parameter_identification {k : Type} [Field k] [IsAlgClosed k] (n d : ℕ) (hd : 1 ≤ d) (hn : 1 ≤ n) (X : SmoothProjectiveVariety k n) : (IsGenericProperty fun (H : HomogeneousPolys k (BertiniVeronese.veroneseMonomialCount n d - 1) 1) => IsSmooth_intersection_variety (↑H) (veronese_image_smooth n d hd hn X)) → IsGenericProperty fun (f : HomogeneousPolys k n d) => IsSmooth_intersection_variety (↑f) X

Parameter identification under the Veronese embedding: degree-d hypersurfaces in ℙⁿ correspond to hyperplanes in the Veronese target, so genericity transfers from one parameter space to the other.

noncomputable def veronese_Pn_smooth {k : Type} [Field k] [IsAlgClosed k] (n d : ℕ) (hd : 1 ≤ d) (hn : 1 ≤ n) : SmoothProjectiveVariety k (BertiniVeronese.veroneseMonomialCount n d - 1)

The image of ℙⁿ under the degree-d Veronese embedding, regarded as a smooth projective subvariety of ℙ^(C(n+d,d)-1).

theorem veronese_Pn_identification {k : Type} [Field k] [IsAlgClosed k] (n d : ℕ) (hd : 1 ≤ d) (hn : 1 ≤ n) : (IsGenericProperty fun (H : HomogeneousPolys k (BertiniVeronese.veroneseMonomialCount n d - 1) 1) => IsSmooth_intersection_variety (↑H) (veronese_Pn_smooth n d hd hn)) → IsGenericProperty fun (f : HomogeneousPolys k n d) => IsSmooth_hypersurface ↑f

Parameter identification specialized to X = ℙⁿ: generic smoothness of hyperplane sections of the Veronese image transfers to generic smoothness of degree-d hypersurfaces in ℙⁿ.

theorem veroneseMonomialCount_ge_two_for_bertini (n d : ℕ) (hd : 1 ≤ d) (hn : 1 ≤ n) : 2 ≤ BertiniVeronese.veroneseMonomialCount n d

For d ≥ 1 and n ≥ 1, the number of degree-d monomials is at least 2, so the Veronese target projective space has positive dimension (needed to apply Bertini there).

theorem corollary28_part_a {k : Type} [Field k] [IsAlgClosed k] (n d : ℕ) (hd : 1 ≤ d) (hn : 1 ≤ n) : IsGenericProperty fun (f : HomogeneousPolys k n d) => IsSmooth_hypersurface ↑f

Corollary 28 (a), Lec 22: over an algebraically closed field, the generic degree-d hypersurface in ℙⁿ is smooth, for any d ≥ 1 and n ≥ 1.

theorem corollary28_part_b {k : Type} [Field k] [IsAlgClosed k] (n d : ℕ) (hd : 1 ≤ d) (hn : 1 ≤ n) (X : SmoothProjectiveVariety k n) : IsGenericProperty fun (f : HomogeneousPolys k n d) => IsSmooth_intersection_variety (↑f) X

Corollary 28 (b), Lec 22: over an algebraically closed field, for any smooth projective variety X ⊂ ℙⁿ, the generic degree-d hypersurface cuts X in a smooth subvariety.

theorem corollary28_generic_hypersurface_smooth {k : Type} [Field k] [IsAlgClosed k] (n d : ℕ) (hd : 1 ≤ d) (hn : 1 ≤ n) : (IsGenericProperty fun (f : HomogeneousPolys k n d) => IsSmooth_hypersurface ↑f) ∧ ∀ (X : SmoothProjectiveVariety k n), IsGenericProperty fun (f : HomogeneousPolys k n d) => IsSmooth_intersection_variety (↑f) X

Corollary 28 (Lec 22), combined: over an algebraically closed field, generic degree-d hypersurfaces in ℙⁿ are smooth, and they cut every fixed smooth projective subvariety X in a smooth subvariety.