LineRestriction.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Line restriction of homogeneous equations and arrangement products

theorem OAI.Nagata.Workers.W24.product_linear_factors_dvd_of_eval_zero line 21

Source documentation

Distinct linear factors divide a polynomial which vanishes at all their roots, over an arbitrary integral-domain coefficient ring.

theorem product_linear_factors_dvd_of_eval_zero {A ι : Type*} [CommRing A] [IsDomain A]
    (a : ι → A) (ha : Function.Injective a) (s : Finset ι) (R : A[X])
    (hzero : ∀ i ∈ s, R.eval (a i) = 0) :
    (∏ i ∈ s, (X - C (a i))) ∣ R := by
…

def OAI.Nagata.Workers.W24.affineLineGraph line 47
Source documentation
The actual affine graph polynomial of line i, using U=-x.
```
def affineLineGraph (K : Type*) [CommRing K] (i : ℕ) : K[X] :=
…
```
theorem OAI.Nagata.Workers.W24.affineLineGraph_injective line 51
Source documentation
Distinct integer line labels give distinct graph polynomials in characteristic zero.
```
theorem affineLineGraph_injective {K : Type*} [CommRing K] [CharZero K] :
    Function.Injective (affineLineGraph K) := by
…
```
Mentions: OAI.Nagata.Workers.W24.affineLineGraph
def OAI.Nagata.Workers.W24.lineUnionEquation line 61
Source documentation
Equation of the entire reduced line union in the actual affine plane ring.
```
def lineUnionEquation (K : Type*) [CommRing K] (k : ℕ) : Polynomial (Polynomial K) :=
…
```
def OAI.Nagata.Workers.W24.lineRestriction line 65
Source documentation
Actual polynomial restriction to an affine line.
```
def lineRestriction {K : Type*} [CommRing K] (R : Polynomial (Polynomial K))
    (i : ℕ) : Polynomial K := R.eval (affineLineGraph K i)
```
Mentions: OAI.Nagata.Workers.W24.affineLineGraph
theorem OAI.Nagata.Workers.W24.lineUnion_dvd_iff_restrictions_zero line 70
Source documentation
Divisibility by the reduced line-union equation is exactly vanishing of all component restrictions, without requiring the global curve to be irreducible.
```
theorem lineUnion_dvd_iff_restrictions_zero {K : Type*} [Field K] [CharZero K]
    (k : ℕ) (R : Polynomial (Polynomial K)) :
    lineUnionEquation K k ∣ R ↔ ∀ i : Fin k, lineRestriction R i.val = 0 := by
…
```
Mentions: OAI.Nagata.Workers.W24.lineUnionEquation, OAI.Nagata.Workers.W24.lineRestriction
theorem OAI.Nagata.Workers.W24.exists_nonzero_lineRestriction line 86
Source documentation
The algebraic noncancellation bridge needed by reducible normal specialization.
```
theorem exists_nonzero_lineRestriction {K : Type*} [Field K] [CharZero K]
    (k : ℕ) (R : Polynomial (Polynomial K)) (hR : ¬ lineUnionEquation K k ∣ R) :
    ∃ i : Fin k, lineRestriction R i.val ≠ 0 := by
…
```
Mentions: OAI.Nagata.Workers.W24.lineUnionEquation, OAI.Nagata.Workers.W24.lineRestriction

theorem OAI.Nagata.Workers.W24.linear_product_dvd_iff line 108

Source documentation

A product of distinct monic graph equations divides precisely when every component evaluation vanishes.

theorem linear_product_dvd_iff {A ι : Type*} [CommRing A] [IsDomain A] [Fintype ι]
    (a : ι → A) (ha : Function.Injective a) (R : A[X]) :
    (∏ i, (X - C (a i))) ∣ R ↔ ∀ i, R.eval (a i) = 0 := by
…

theorem OAI.Nagata.Workers.W24.nonzero_component_of_not_linear_product_dvd line 120

Source documentation

A nonzero residue modulo the line union has a nonzero component restriction.

theorem nonzero_component_of_not_linear_product_dvd {A ι : Type*}
    [CommRing A] [IsDomain A] [Fintype ι]
    (a : ι → A) (ha : Function.Injective a) (R : A[X])
    (hR : ¬ (∏ i, (X - C (a i))) ∣ R) :
    ∃ i, R.eval (a i) ≠ 0 := by
…

theorem OAI.Nagata.Workers.W24.finThreeCases_one line 143
theorem OAI.Nagata.Workers.W24.finThreeCases_two line 146
def OAI.Nagata.Workers.W24.homogeneousLineGraph line 150
Source documentation
Binary homogeneous graph Y=i² Z-i U; binary coordinates are U,Z.
```
def homogeneousLineGraph (K : Type*) [CommRing K] (i : ℕ) : MvPolynomial (Fin 2) K :=
…
```
def OAI.Nagata.Workers.W24.homogeneousLineEquation line 155
Source documentation
The actual homogeneous linear equation Y-i²Z+iU.
```
def homogeneousLineEquation (K : Type*) [CommRing K] (i : ℕ) : MvPolynomial (Fin 3) K :=
…
```
def OAI.Nagata.Workers.W24.ternaryAsPolynomialInY line 160
Source documentation
Regard the actual ternary ring as polynomials in Y with binary U,Z coefficients.
```
def ternaryAsPolynomialInY (K : Type*) [CommSemiring K] :
    MvPolynomial (Fin 3) K ≃ₐ[K] Polynomial (MvPolynomial (Fin 2) K) :=
…
```
def OAI.Nagata.Workers.W24.homogeneousLineRestriction line 166
Source documentation
Binary restrictions are ordinary ring evaluations in the Y variable.
```
def homogeneousLineRestriction {K : Type*} [CommRing K]
    (R : MvPolynomial (Fin 3) K) (i : ℕ) : MvPolynomial (Fin 2) K :=
…
```
def OAI.Nagata.Workers.W24.homogeneousLineSubstitution line 171
Source documentation
Explicit homogeneous coordinate substitution (U,Y,Z)=(U,i²Z-iU,Z).
```
def homogeneousLineSubstitution (K : Type*) [CommRing K] (i : ℕ) :
    Fin 3 → MvPolynomial (Fin 2) K :=
…
```
def OAI.Nagata.Workers.W24.homogeneousLineUnion line 176
Source documentation
Homogeneous equation of the reduced union of k lines.
```
def homogeneousLineUnion (K : Type*) [CommRing K] (k : ℕ) : MvPolynomial (Fin 3) K :=
…
```
theorem OAI.Nagata.Workers.W24.homogeneousLineGraph_homogeneous line 179
theorem OAI.Nagata.Workers.W24.homogeneousLineRestriction_eq_eval₂ line 185
Source documentation
The polynomial-ring restriction agrees with the actual homogeneous coordinate map.
```
theorem homogeneousLineRestriction_eq_eval₂ {K : Type*} [CommRing K]
    (R : MvPolynomial (Fin 3) K) (i : ℕ) :
    homogeneousLineRestriction R i = MvPolynomial.eval₂ MvPolynomial.C
      (homogeneousLineSubstitution K i) R := by
…
```
Mentions: OAI.Nagata.Workers.W24.homogeneousLineRestriction, OAI.Nagata.Workers.W24.homogeneousLineSubstitution
theorem OAI.Nagata.Workers.W24.homogeneousLineRestriction_homogeneous line 204
Source documentation
Restricting a homogeneous form to any component preserves its homogeneous degree.
```
theorem homogeneousLineRestriction_homogeneous {K : Type*} [CommRing K]
    (R : MvPolynomial (Fin 3) K) (i d : ℕ) (hR : R.IsHomogeneous d) :
    (homogeneousLineRestriction R i).IsHomogeneous d := by
…
```
Mentions: OAI.Nagata.Workers.W24.homogeneousLineRestriction
theorem OAI.Nagata.Workers.W24.homogeneousLineEquation_homogeneous line 217
theorem OAI.Nagata.Workers.W24.homogeneousLineUnion_homogeneous line 223
theorem OAI.Nagata.Workers.W24.homogeneousLineGraph_injective line 231
theorem OAI.Nagata.Workers.W24.ternaryAsPolynomialInY_line line 238
Source documentation
The actual line equation maps to the monic factor used by product restriction.
```
theorem ternaryAsPolynomialInY_line {K : Type*} [CommRing K] (i : ℕ) :
    ternaryAsPolynomialInY K (homogeneousLineEquation K i) =
      Polynomial.X - Polynomial.C (homogeneousLineGraph K i) := by
…
```
Mentions: OAI.Nagata.Workers.W24.ternaryAsPolynomialInY, OAI.Nagata.Workers.W24.homogeneousLineEquation, OAI.Nagata.Workers.W24.homogeneousLineGraph
theorem OAI.Nagata.Workers.W24.ternaryAsPolynomialInY_union line 245
theorem OAI.Nagata.Workers.W24.homogeneousUnion_dvd_iff_restrictions_zero line 251
Source documentation
Genuine global component noncancellation, before affine dehomogenization.
```
theorem homogeneousUnion_dvd_iff_restrictions_zero {K : Type*} [Field K] [CharZero K]
    (k : ℕ) (R : MvPolynomial (Fin 3) K) :
    homogeneousLineUnion K k ∣ R ↔ ∀ i : Fin k, homogeneousLineRestriction R i.val = 0 := by
…
```
Mentions: OAI.Nagata.Workers.W24.homogeneousLineUnion, OAI.Nagata.Workers.W24.homogeneousLineRestriction
theorem OAI.Nagata.Workers.W24.exists_nonzero_homogeneousLineRestriction line 258
theorem OAI.Nagata.Workers.W24.binaryAffine_homogeneousLineRestriction line 278
Source documentation
Dehomogenizing the genuine binary component restriction is exactly the literal substitution (U,Y,Z)=(U,i²-iU,1).
```
theorem binaryAffine_homogeneousLineRestriction
    (R : MvPolynomial (Fin 3) ℂ) (i : ℕ) :
    Nagata.W16.binaryAffine (homogeneousLineRestriction R i) =
      Nagata.W04.ReducibleSquare.lineRestriction (i : ℂ) R := by
…
```
Mentions: OAI.Nagata.W16.binaryAffine, OAI.Nagata.Workers.W24.homogeneousLineRestriction, OAI.Nagata.W04.ReducibleSquare.lineRestriction
theorem OAI.Nagata.Workers.W24.affine_lineRestriction_eq_zero_iff line 301
Source documentation
Vanishing of one actual affine component restriction is equivalent to vanishing of its binary homogeneous restriction for a fixed-degree form.
```
theorem affine_lineRestriction_eq_zero_iff
    (R : MvPolynomial (Fin 3) ℂ) (i d : ℕ) (hR : R.IsHomogeneous d) :
    Nagata.W04.ReducibleSquare.lineRestriction (i : ℂ) R = 0 ↔
      homogeneousLineRestriction R i = 0 := by
…
```
Mentions: OAI.Nagata.W04.ReducibleSquare.lineRestriction, OAI.Nagata.Workers.W24.homogeneousLineRestriction
theorem OAI.Nagata.Workers.W24.exists_nonzero_affine_lineRestriction line 316
Source documentation
Nonzero residue modulo the homogeneous union supplies a nonzero actual affine line restriction. Fixed-degree dehomogenization supplies the needed bridge rather than an unproved saturation assertion.
```
theorem exists_nonzero_affine_lineRestriction
    (k d : ℕ) (R : MvPolynomial (Fin 3) ℂ) (hR : R.IsHomogeneous d)
    (hnotdvd : ¬ homogeneousLineUnion ℂ k ∣ R) :
    ∃ i : Fin k, Nagata.W04.ReducibleSquare.lineRestriction (i.val : ℂ) R ≠ 0 := by
…
```
Mentions: OAI.Nagata.Workers.W24.homogeneousLineUnion, OAI.Nagata.W04.ReducibleSquare.lineRestriction
theorem OAI.Nagata.Workers.W24.bivariateToNested_directChart_line line 336
theorem OAI.Nagata.Workers.W24.bivariateToNested_directChart_union line 344
theorem OAI.Nagata.Workers.W24.directChart_union_eq_nestedToBivariate line 350
theorem OAI.Nagata.Workers.W24.planePolynomialEval_directChart line 375
Source documentation
Evaluation of the actual Z=1 dehomogenization is normalized ternary evaluation.
```
theorem planePolynomialEval_directChart (R : MvPolynomial (Fin 3) ℂ) (u y : ℂ) :
    Nagata.Workers.W28.planePolynomialEval (Nagata.W27.directChartHom 2 R) (u, y) =
      MvPolynomial.eval ![u, y, 1] R := by
…
```
Mentions: OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.W27.directChartHom
theorem OAI.Nagata.Workers.W24.planePolynomialEval_directChart_on_line line 392
Source documentation
The analytic-chart plane polynomial on the selected graph is the exact univariate line restriction used in the square obstruction.
```
theorem planePolynomialEval_directChart_on_line
    (R : MvPolynomial (Fin 3) ℂ) (i u : ℂ) :
    Nagata.Workers.W28.planePolynomialEval (Nagata.W27.directChartHom 2 R)
      (u, i ^ 2 - i * u) =
        (Nagata.W04.ReducibleSquare.lineRestriction i R).eval u := by
…
```
Mentions: OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.W27.directChartHom, OAI.Nagata.W04.ReducibleSquare.lineRestriction