def BertiniArithmetic.fiberDim (d n : ℕ) : ℕ

Dimension of a generic fiber in the Bertini dimension count: n - d - 1.

def BertiniArithmetic.incidenceDim (d n : ℕ) : ℕ

Dimension of the incidence variety in the Bertini argument: dimension of the base plus the generic fiber dimension.

def BertiniArithmetic.dualDim (n : ℕ) : ℕ

Dimension of the dual projective space (ℙⁿ)ⱽ of hyperplanes: n.

theorem BertiniArithmetic.incidence_dim_eq (d n : ℕ) (hdn : d < n) : incidenceDim d n = n - 1

For d < n, the incidence variety has dimension n - 1.

theorem BertiniArithmetic.incidence_dim_lt_dual (d n : ℕ) (hdn : d < n) : incidenceDim d n < dualDim n

Dimension comparison: dim(incidence) < dim(dual projective space) for d < n. This is the gap that produces a generic smooth hyperplane section in Bertini.

theorem BertiniArithmetic.bertini_codimension_bound (d n : ℕ) (hdn : d < n) : dualDim n - incidenceDim d n ≥ 1

The codimension of the image of the incidence variety in the dual space is at least 1.

theorem BertiniArithmetic.pred_lt_of_pos (n : ℕ) (hn : 0 < n) : n - 1 < n

Helper: for n > 0, n - 1 < n.

theorem exists_not_mem_of_ne_univ {X : Type u_1} {Z : Set X} (hne : Z ≠ Set.univ) : ∃ (x : X), x ∉ Z

A set that is not the whole space has a point outside it.

theorem bertini_projective_chevalley_gap {HyperplaneIndex : Type} (isBadLocus : HyperplaneIndex → Prop) (n d : ℕ) (hdn : d < n) (h_incidence_dim : d + (n - d - 1) = n - 1) (h_incidence_lt : n - 1 < n) (h_bad_proper : {H : HyperplaneIndex | isBadLocus H} ≠ Set.univ) : ∃ (H : HyperplaneIndex), ¬isBadLocus H

Bertini via Chevalley's theorem + dimension gap: if the "bad" locus of singular hyperplane sections is a proper subset of the dual projective space, then there exists a good hyperplane.

structure SmoothSubvariety : Type 1

An abstract bundle of data for a smooth subvariety of ℙⁿ of dimension d together with its space of hyperplanes — used to state Bertini's theorem combinatorially.

• n : ℕ
• d : ℕ
• HyperplaneIndex : Type
• hdn : self.d < self.n

opaque SmoothSubvariety.isSmoothSection (X : SmoothSubvariety) : X.HyperplaneIndex → Prop

Opaque predicate: a hyperplane gives a smooth section of X.

theorem bertini_generic_hyperplane_smooth (X : SmoothSubvariety) : ∃ (H : X.HyperplaneIndex), X.isSmoothSection H

Bertini's theorem (abstract): for any smooth subvariety X ⊆ ℙⁿ, there exists a hyperplane giving a smooth section (Thm 22.1, Lec 22).

structure BertiniThm221 (X : SmoothSubvariety) : Prop

Packaging of the three ingredients of Bertini's theorem (Thm 22.1): the incidence dimension count, the strict-inequality gap with the dual space, and existence of a smooth hyperplane section.

• incidence_dim : X.d + (X.n - X.d - 1) = X.n - 1
• incidence_lt_dual : X.n - 1 < X.n
• smooth_section_exists : ∃ (H : X.HyperplaneIndex), X.isSmoothSection H

def BertiniThm221.mk' (X : SmoothSubvariety) : BertiniThm221 X

Builder for BertiniThm221, assembling the dimension count and Bertini's smoothness existence statement.