OAI/AlgebraicGeometry/PlaneCurves/LineObstructions.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Nagata.W04.ReducibleSquare.cycle_products_ne line 38

   Source documentation

   The two positive integral cycle products have different positive powers.

   theorem cycle_products_ne {K : Type*} [Field K] [CharZero K]
       (k t : ℕ) (hk : 0 < k) (ht : 0 < t) :
       (((k : K) + 2) * 3) ^ t ≠ (((k : K) + 3) * 2) ^ t := by
   …

2. theorem OAI.Nagata.W04.ReducibleSquare.cycle_coefficients_zero line 50

   Source documentation

   Three node equations force every scalar on the triangle to vanish.

   theorem cycle_coefficients_zero {K : Type*} [Field K] [CharZero K]
       (k t : ℕ) (hk : 0 < k) (ht : 0 < t) (c₀ c₁ c₂ : K)
       (h₀₁ : c₀ * ((k : K) + 2) ^ t = c₁ * 2 ^ t)
       (h₁₂ : c₁ = c₂)
       (h₂₀ : c₂ * 3 ^ t = c₀ * ((k : K) + 3) ^ t) :
       c₀ = 0 ∧ c₁ = 0 ∧ c₂ = 0 := by
   …

3. theorem OAI.Nagata.W04.ReducibleSquare.polynomial_triangle_zero line 74

   Source documentation

   Node gluing for the explicit common-tail polynomials forces the triangle to vanish.

   theorem polynomial_triangle_zero {K : Type*} [Field K] [CharZero K]
       (k t : ℕ) (hk : 0 < k) (ht : 0 < t) (T : K[X])
       (hT₁ : T.eval 1 ≠ 0) (hT₂ : T.eval 2 ≠ 0) (hT₃ : T.eval 3 ≠ 0)
       (c₀ c₁ c₂ : K)
       (h₀₁ : (C c₀ * ((X + C ((k : K) + 1)) * T) ^ t).eval 1 =
         (C c₁ * ((X + C 1) * T) ^ t).eval 1)
       (h₁₂ : (C c₁ * ((X + C 1) * T) ^ t).eval 3 =
         (C c₂ * ((X + C 1) * T) ^ t).eval 3)
       (h₂₀ : (C c₂ * ((X + C 1) * T) ^ t).eval 2 =
         (C c₀ * ((X + C ((k : K) + 1)) * T) ^ t).eval 2) :
       c₀ = 0 ∧ c₁ = 0 ∧ c₂ = 0 := by
   …

4. theorem OAI.Nagata.W04.ReducibleSquare.polynomial_shape_of_mark_divisibility line 100

   Source documentation

   Equality in the degree bound gives scalar-times-full-mark-product.

   theorem polynomial_shape_of_mark_divisibility {K : Type*} [Field K]
       (f P : K[X]) (k t : ℕ) (hP : P.Monic) (hdegree : P.natDegree = k)
       (hfdegree : f.natDegree ≤ k * t) (hdiv : P ^ t ∣ f) :
       f = C f.leadingCoeff * P ^ t := by
   …

5. theorem OAI.Nagata.W04.Dimension.polynomial_height_le_one line 123
6. theorem OAI.Nagata.W04.Dimension.prime_height_eq_one_of_le_one line 147
7. def OAI.Nagata.W04.Dimension.lastVariableEquiv line 167
8. theorem OAI.Nagata.W04.Dimension.lastVariableEquiv_symm_C line 172
9. theorem OAI.Nagata.W04.Dimension.height_le_one_of_independent_quotient line 183
10. theorem OAI.Nagata.W04.Dimension.height_eq_one_of_independent_quotient line 212
11. def OAI.Nagata.W04.ReducibleSquare.lineSubstitution line 234

    Source documentation

    Homogeneous coordinates on Y=i²-iU in the affine parameter U.

    def lineSubstitution (i : K) : Fin 3 → Polynomial K :=
    …

12. def OAI.Nagata.W04.ReducibleSquare.lineRestriction line 238

    Source documentation

    The actual polynomial restriction homomorphism from plane forms to component i.

    def lineRestriction (i : K) : MvPolynomial (Fin 3) K →+* Polynomial K :=
    …

13. theorem OAI.Nagata.W04.ReducibleSquare.lineRestriction_node_gluing line 242

    Source documentation

    Actual ambient forms automatically glue at each pairwise node.

    theorem lineRestriction_node_gluing (F : MvPolynomial (Fin 3) K) (i j : K) :
        (lineRestriction i F).eval (i + j) = (lineRestriction j F).eval (i + j) := by
    …

    Mentions: OAI.Nagata.W04.ReducibleSquare.lineRestriction

14. def OAI.Nagata.W04.ReducibleSquare.lineEquation line 255

    Source documentation

    The affine equation of component i.

    def lineEquation (i x y : K) : K := y + i * x - i ^ 2

15. theorem OAI.Nagata.W04.ReducibleSquare.lineEquation_on_component line 258

    Source documentation

    Restricting another line equation to component i gives the node factor.

    theorem lineEquation_on_component (i j x : K) :
        lineEquation j x (i ^ 2 - i * x) = (j - i) * (x - i - j) := by
    …

    Mentions: OAI.Nagata.W04.ReducibleSquare.lineEquation

16. theorem OAI.Nagata.W04.ReducibleSquare.marked_point_avoids_other_line line 264

    Source documentation

    Negative integer marked coordinates avoid every other component.

    theorem marked_point_avoids_other_line [CharZero K] (i j v : ℕ)
        (hij : i ≠ j) (hv : 0 < v) :
        lineEquation (j : K) (-(v : K)) ((i : K) ^ 2 - (i : K) * (-(v : K))) ≠ 0 := by
    …

    Mentions: OAI.Nagata.W04.ReducibleSquare.lineEquation

17. def OAI.Nagata.W04.ReducibleSquare.markTail line 288

    Source documentation

    The common marks with affine x-coordinates 2,...,k, in the parameter U=-x.

    def markTail {K : Type*} [CommSemiring K] (k : ℕ) : K[X] :=
    …

18. def OAI.Nagata.W04.ReducibleSquare.firstMark line 292

    Source documentation

    First marked x-coordinate: k+1 on component zero and 1 on all others.

    def firstMark (k i : ℕ) : ℕ := if i = 0 then k + 1 else 1

19. def OAI.Nagata.W04.ReducibleSquare.markPolynomial line 295

    Source documentation

    Actual polynomial vanishing at the k chosen marks on component i.

    def markPolynomial {K : Type*} [CommSemiring K] (k i : ℕ) : K[X] :=
    …

20. theorem OAI.Nagata.W04.ReducibleSquare.markTail_monic line 300
21. theorem OAI.Nagata.W04.ReducibleSquare.markTail_natDegree line 303
22. theorem OAI.Nagata.W04.ReducibleSquare.markPolynomial_monic line 309
23. theorem OAI.Nagata.W04.ReducibleSquare.markPolynomial_natDegree line 312
24. theorem OAI.Nagata.W04.ReducibleSquare.markTail_eval_nat_ne_zero line 321
25. theorem OAI.Nagata.W04.ReducibleSquare.firstMark_pos line 329
26. theorem OAI.Nagata.W04.ReducibleSquare.markPolynomial_eval_nat_ne_zero line 333
27. theorem OAI.Nagata.W04.ReducibleSquare.marked_linear_factors_coprime line 340
28. theorem OAI.Nagata.W04.ReducibleSquare.firstMark_ne_tail line 349
29. theorem OAI.Nagata.W04.ReducibleSquare.markPolynomial_pow_dvd line 354

    Source documentation

    Ordinary marked-point factor divisibility gives the full k-mark product power.

    theorem markPolynomial_pow_dvd (k i t : ℕ) (f : K[X])
        (hfirst : (X + C ((firstMark k i : ℕ) : K)) ^ t ∣ f)
        (htail : ∀ j < k - 1, (X + C ((j + 2 : ℕ) : K)) ^ t ∣ f) :
        (markPolynomial k i : K[X]) ^ t ∣ f := by
    …

    Mentions: OAI.Nagata.W04.ReducibleSquare.firstMark, OAI.Nagata.W04.ReducibleSquare.markPolynomial

30. theorem OAI.Nagata.W04.ReducibleSquare.marked_restriction_shape line 375

    Source documentation

    Equality-degree restrictions have the exact shape required by node gluing.

    theorem marked_restriction_shape (k i t : ℕ) (hk : 0 < k) (f : K[X])
        (hdeg : f.natDegree ≤ k * t)
        (hfirst : (X + C ((firstMark k i : ℕ) : K)) ^ t ∣ f)
        (htail : ∀ j < k - 1, (X + C ((j + 2 : ℕ) : K)) ^ t ∣ f) :
        f = C f.leadingCoeff * (markPolynomial k i : K[X]) ^ t := by
    …

    Mentions: OAI.Nagata.W04.ReducibleSquare.firstMark, OAI.Nagata.W04.ReducibleSquare.markPolynomial

31. theorem OAI.Nagata.W04.ReducibleSquare.line_family_zero line 396

    Source documentation

    No nonzero family of equality-degree marked restrictions can glue at all nodes.

    theorem line_family_zero {K : Type*} [Field K] [CharZero K]
        (k t : ℕ) (hk : 3 ≤ k) (ht : 0 < t) (f : ℕ → K[X])
        (hdeg : ∀ i < k, (f i).natDegree ≤ k * t)
        (hdiv : ∀ i < k, (markPolynomial k i : K[X]) ^ t ∣ f i)
        (hglue : ∀ i < k, ∀ j < k, (f i).eval ((i + j : ℕ) : K) =
          (f j).eval ((i + j : ℕ) : K)) :
        ∀ i < k, f i = 0 := by
    …

    Mentions: OAI.Nagata.W04.ReducibleSquare.markPolynomial

32. theorem OAI.Nagata.W04.ReducibleSquare.line_family_zero_of_marked_factors line 435

    Source documentation

    The same obstruction directly from multiplicity-factor conditions at each mark.

    theorem line_family_zero_of_marked_factors {K : Type*} [Field K] [CharZero K]
        (k t : ℕ) (hk : 3 ≤ k) (ht : 0 < t) (f : ℕ → K[X])
        (hdeg : ∀ i < k, (f i).natDegree ≤ k * t)
        (hfirst : ∀ i < k, (X + C ((firstMark k i : ℕ) : K)) ^ t ∣ f i)
        (htail : ∀ i < k, ∀ j < k - 1, (X + C ((j + 2 : ℕ) : K)) ^ t ∣ f i)
        (hglue : ∀ i < k, ∀ j < k, (f i).eval ((i + j : ℕ) : K) =
          (f j).eval ((i + j : ℕ) : K)) :
        ∀ i < k, f i = 0 := by
    …

    Mentions: OAI.Nagata.W04.ReducibleSquare.firstMark

33. theorem OAI.Nagata.W04.ReducibleSquare.ambient_restrictions_zero line 461

    Source documentation

    Every component restriction vanishes, with gluing discharged for ambient forms.

    theorem ambient_restrictions_zero {K : Type*} [Field K] [CharZero K]
        (k t : ℕ) (hk : 3 ≤ k) (ht : 0 < t) (F : MvPolynomial (Fin 3) K)
        (hdeg : ∀ i < k, (lineRestriction (i : K) F).natDegree ≤ k * t)
        (hfirst : ∀ i < k, (X + C ((firstMark k i : ℕ) : K)) ^ t ∣ lineRestriction (i : K) F)
        (htail : ∀ i < k, ∀ j < k - 1,
          (X + C ((j + 2 : ℕ) : K)) ^ t ∣ lineRestriction (i : K) F) :
        ∀ i < k, lineRestriction (i : K) F = 0 := by
    …

    Mentions: OAI.Nagata.W04.ReducibleSquare.lineRestriction, OAI.Nagata.W04.ReducibleSquare.firstMark

34. theorem OAI.Nagata.W04.ReducibleSquare.ambient_nonzero_restriction_obstruction line 474

    Source documentation

    An actual nonzero component restriction contradicts all the marked degree bounds.

    theorem ambient_nonzero_restriction_obstruction {K : Type*} [Field K] [CharZero K]
        (k t : ℕ) (hk : 3 ≤ k) (ht : 0 < t) (F : MvPolynomial (Fin 3) K)
        (hdeg : ∀ i < k, (lineRestriction (i : K) F).natDegree ≤ k * t)
        (hfirst : ∀ i < k, (X + C ((firstMark k i : ℕ) : K)) ^ t ∣ lineRestriction (i : K) F)
        (htail : ∀ i < k, ∀ j < k - 1,
          (X + C ((j + 2 : ℕ) : K)) ^ t ∣ lineRestriction (i : K) F)
        (hNonzero : ∃ i < k, lineRestriction (i : K) F ≠ 0) : False := by
    …

    Mentions: OAI.Nagata.W04.ReducibleSquare.lineRestriction, OAI.Nagata.W04.ReducibleSquare.firstMark