Assigning lines among proper-cut components

This file implements blueprint node C06 of the lower-bound side of the sharp finite-field Nikodym exponent, and combines it with the weighted selection C07.

Let P : PrivateFamily F d E be a private family of L = Fintype.card E lines, all contained in a prime I of quotient dimension at least two, and let g ∉ I be a polynomial of total degree at most T vanishing on every line of the family (the cutting polynomial of node C04, taken here as an input). The proper cut H.proper_cut (B03) produces finitely many prime components J of I + (g) of quotient dimension quotDim I - 1, positive degree and total degree at most T · deg I. Every line ideal P.lineIdeal e is a prime containing I + (g), hence contains some component; we assign each index e one such component c e. The fibers of c partition E, so the assigned counts L_J = #{e | c e = J} sum to L, and the weighted selection C07 yields a component J with L_J > 0 and L · deg J ≤ L_J · (T · deg I).

Main declarations:

• PrivateFamily.restrict_lineIdeal: the line ideals of a subfamily are those of the family;
• PrivateFamily.exists_component: the component J together with the finset s of indices assigned to it (so L_J = #s), with J ≤ P.lineIdeal e for e ∈ s;
• PrivateFamily.exists_component_family: the same, packaged for the induction of node C09 with the private subfamily P.restrict s of #s lines lying on J.

@[simp]

theorem Nikodym.LowerBound.PrivateFamily.restrict_lineIdeal {K : Type u_1} [Field K] {d : ℕ} {F : Type u_2} [Field F] {E : Type u_3} [Fintype E] [Algebra F K] (P : PrivateFamily F d E) (s : Finset E) (e : ↥s) : (P.restrict s).lineIdeal e = P.lineIdeal ↑e

Blueprint C06: the line ideals of the subfamily P.restrict s are the line ideals of P.

theorem Nikodym.LowerBound.PrivateFamily.sup_span_ne_top {K : Type u_1} [Field K] {d : ℕ} {F : Type u_2} [Field F] {E : Type u_3} [Fintype E] [Algebra F K] (P : PrivateFamily F d E) {I : Ideal (MvPolynomial (Fin d) K)} [Nonempty E] (hIP : ∀ (e : E), I ≤ P.lineIdeal e) {g : MvPolynomial (Fin d) K} (hg : ∀ (e : E), g ∈ P.lineIdeal e) : I ⊔ Ideal.span {g} ≠ ⊤

Blueprint C06: if I is contained in every line ideal of a nonempty private family and g vanishes on every line of the family, then I + (g) is a proper ideal.

theorem Nikodym.LowerBound.PrivateFamily.exists_component {K : Type u_1} [Field K] {d : ℕ} {F : Type u_2} [Field F] {E : Type u_3} [Fintype E] [Algebra F K] (P : PrivateFamily F d E) (H : AlgebraInterface K d) {I : Ideal (MvPolynomial (Fin d) K)} (hI : I.IsPrime) (hk : 2 ≤ quotDim I) (hIP : ∀ (e : E), I ≤ P.lineIdeal e) [Nonempty E] {g : MvPolynomial (Fin d) K} {T : ℕ} (hgI : g ∉ I) (hgT : g.totalDegree ≤ T) (hg : ∀ (e : E), g ∈ P.lineIdeal e) : ∃ (J : Ideal (MvPolynomial (Fin d) K)) (s : Finset E), J.IsPrime ∧ quotDim J + 1 = quotDim I ∧ 0 < degree J ∧ s.Nonempty ∧ (∀ e ∈ s, J ≤ P.lineIdeal e) ∧ Fintype.card E * degree J ≤ s.card * (T * degree I)

Blueprint C06 + C07: assigning the lines of a private family among the components of a proper cut and selecting a component. Given a prime I of quotient dimension at least two containing every line of the private family P, and a polynomial g ∉ I of total degree at most T vanishing on every line of P, there are a prime component J of I + (g), of quotient dimension quotDim I - 1 and positive degree, and a nonempty finset s of indices whose lines lie on J, such that L · deg J ≤ #s · (T · deg I) where L = Fintype.card E.

theorem Nikodym.LowerBound.PrivateFamily.exists_component_family {K : Type u_1} [Field K] {d : ℕ} {F : Type u_2} [Field F] {E : Type u_3} [Fintype E] [Algebra F K] (P : PrivateFamily F d E) (H : AlgebraInterface K d) {I : Ideal (MvPolynomial (Fin d) K)} (hI : I.IsPrime) (hk : 2 ≤ quotDim I) (hIP : ∀ (e : E), I ≤ P.lineIdeal e) [Nonempty E] {g : MvPolynomial (Fin d) K} {T : ℕ} (hgI : g ∉ I) (hgT : g.totalDegree ≤ T) (hg : ∀ (e : E), g ∈ P.lineIdeal e) : ∃ (J : Ideal (MvPolynomial (Fin d) K)) (s : Finset E), J.IsPrime ∧ quotDim J + 1 = quotDim I ∧ 0 < degree J ∧ 0 < s.card ∧ (∀ (e : ↥s), J ≤ (P.restrict s).lineIdeal e) ∧ Fintype.card E * degree J ≤ s.card * (T * degree I)

Blueprint C06 + C07, packaged for the induction of node C09: the selected component J carries the private subfamily P.restrict s of #s > 0 lines, with L · deg J ≤ #s · (T · deg I).