opaque BertiniGeometric.IsSmoothSubvariety (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (d : ℕ) : Set (Projectivization k V) → Prop

Opaque predicate: a subset of the projective space ℙ(V) is a smooth subvariety of dimension d.

opaque BertiniGeometric.IsZariskiDenseOpen (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] : Set (Projectivization k (Module.Dual k V)) → Prop

Opaque predicate: a subset of the dual projective space ℙ(V*) of hyperplanes is Zariski dense open.

def BertiniGeometric.projectiveHyperplane (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (H : Projectivization k (Module.Dual k V)) : Set (Projectivization k V)

The projective hyperplane V(H) ⊂ ℙ(V) corresponding to a class H ∈ ℙ(V*): the locus of points where a representative linear functional vanishes.

theorem BertiniGeometric.bertini_theorem_projective (k : Type u_3) [Field k] [IsAlgClosed k] (V : Type u_4) [AddCommGroup V] [Module k V] [FiniteDimensional k V] (hV : Module.finrank k V ≥ 2) (X : Set (Projectivization k V)) (d : ℕ) (hd : d ≥ 1) (hX : IsSmoothSubvariety k V d X) : ∃ (U : Set (Projectivization k (Module.Dual k V))), IsZariskiDenseOpen k V U ∧ ∀ H ∈ U, IsSmoothSubvariety k V (d - 1) (X ∩ projectiveHyperplane k V H)

Bertini's theorem (Thm 22.1, Lec 22), projective form: for a smooth subvariety X ⊆ ℙ(V) of dimension d ≥ 1 over an algebraically closed field, there is a Zariski dense open set of hyperplanes H such that X ∩ V(H) is again smooth of dimension d - 1.

theorem BertiniGeometric.bertini_smooth_section_exists (k : Type u_3) [Field k] [IsAlgClosed k] (V : Type u_4) [AddCommGroup V] [Module k V] [FiniteDimensional k V] (hV : Module.finrank k V ≥ 2) (X : Set (Projectivization k V)) (d : ℕ) (hd : d ≥ 1) (hX : IsSmoothSubvariety k V d X) : ∃ (H : Projectivization k (Module.Dual k V)), IsSmoothSubvariety k V (d - 1) (X ∩ projectiveHyperplane k V H)

Existence statement form of Bertini: at least one hyperplane gives a smooth section.