OAI/AlgebraicGeometry/PlaneCurves/CycleMultiplicity.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Nagata.AffineMultiplicity.root_power_dvd_of_orderAtLeast line 21

   Source documentation

   A concrete polynomial substitution preserving evaluation at a marked point pulls its mth ideal power into the mth root-factor power.

   theorem root_power_dvd_of_orderAtLeast
       (p : σ → R) (a : R) (φ : MvPolynomial σ R →+* Polynomial R)
       (hφ : ∀ g, (φ g).eval a = MvPolynomial.eval p g)
       (m : ℕ) (f : MvPolynomial σ R) (hf : orderAtLeast p m f) :
       (Polynomial.X - Polynomial.C a) ^ m ∣ φ f := by
   …

2. theorem OAI.Nagata.W04.ReducibleSquare.lineRestriction_eval line 48
3. theorem OAI.Nagata.W04.ReducibleSquare.lineRestriction_marked_root_power line 62

   Source documentation

   Ambient affine multiplicity at the actual marked point yields root-factor divisibility of the actual line restriction. For projective multiplicity the input must first be expressed in a chart; no such bridge is assumed here.

   theorem lineRestriction_marked_root_power (i v : K) (m : ℕ)
       (F : MvPolynomial (Fin 3) K)
       (hF : AffineMultiplicity.orderAtLeast ![-v, i ^ 2 + i * v, 1] m F) :
       (Polynomial.X + Polynomial.C v) ^ m ∣ lineRestriction i F := by
   …

   Mentions: OAI.Nagata.W04.ReducibleSquare.lineRestriction

4. theorem OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity_eq_powerSeriesOrder line 93

   Source documentation

   The explicit finite minimum equals the order of the actual polynomial's coefficientwise embedding in multivariate formal power series.

   theorem ordinaryMultiplicity_eq_powerSeriesOrder
       (p : σ → R) (f : MvPolynomial σ R) (hf : f ≠ 0) :
       (ordinaryMultiplicity p f hf : ℕ∞) =
         (translateHom p f : MvPowerSeries σ R).order := by
   …

5. theorem OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity_mul line 109

   Source documentation

   Over a coefficient ring without zero divisors, actual ordinary orders add exactly under multiplication, including products defining reducible curves.

   theorem ordinaryMultiplicity_mul [NoZeroDivisors R]
       (p : σ → R) (f g : MvPolynomial σ R)
       (hf : f ≠ 0) (hg : g ≠ 0) :
       ordinaryMultiplicity p (f * g) (mul_ne_zero hf hg) =
         ordinaryMultiplicity p f hf + ordinaryMultiplicity p g hg := by
   …

6. theorem OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity_one line 120
7. theorem OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity_pow line 131

   Source documentation

   Powers scale numerical multiplicity exactly, including exponent zero and nonreduced curve equations. Nonvanishing of every power is derived.

   theorem ordinaryMultiplicity_pow [NoZeroDivisors R] [Nontrivial R]
       (p : σ → R) (f : MvPolynomial σ R) (hf : f ≠ 0) (N : ℕ) :
       ordinaryMultiplicity p (f ^ N) (pow_ne_zero N hf) = ordinaryMultiplicity p f hf * N := by
   …

8. theorem OAI.Nagata.ProjectiveGeometry.formOrdinaryMultiplicity_mul line 152

   Source documentation

   Products of actual nonzero homogeneous equations add their numerical ordinary multiplicities at every projective point.

   theorem formOrdinaryMultiplicity_mul {d e : ℕ}
       (F : W16.NonzeroHomogeneousForm d) (G : W16.NonzeroHomogeneousForm e)
       (p : PlanePoint) :
       formOrdinaryMultiplicity (F.mul G) p =
         formOrdinaryMultiplicity F p + formOrdinaryMultiplicity G p := by
   …

   Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint

9. theorem OAI.Nagata.ProjectiveGeometry.formOrdinaryMultiplicity_pow line 169

   Source documentation

   Repeated factors retain their full numerical multiplicity, including the zeroth power as the constant equation.

   theorem formOrdinaryMultiplicity_pow {d : ℕ}
       (F : W16.NonzeroHomogeneousForm d) (N : ℕ) (p : PlanePoint) :
       formOrdinaryMultiplicity (F.pow N) p = formOrdinaryMultiplicity F p * N := by
   …

   Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint

10. theorem OAI.Nagata.ProjectiveGeometry.classOrdinaryMultiplicity_classOfForm_mul line 181

    Source documentation

    The exact product formula also holds after passing to equation classes.

    theorem classOrdinaryMultiplicity_classOfForm_mul {d e : ℕ}
        (F : W16.NonzeroHomogeneousForm d) (G : W16.NonzeroHomogeneousForm e)
        (p : PlanePoint) :
        classOrdinaryMultiplicity (W16.classOfForm (F.mul G)) p =
          classOrdinaryMultiplicity (W16.classOfForm F) p +
            classOrdinaryMultiplicity (W16.classOfForm G) p := by
    …

    Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint, OAI.Nagata.ProjectiveGeometry.classOrdinaryMultiplicity, OAI.Nagata.W16.classOfForm

11. theorem OAI.Nagata.ProjectiveGeometry.classOrdinaryMultiplicity_classOfForm_pow line 189
12. theorem OAI.Nagata.ProjectiveGeometry.classOrdinaryMultiplicity_representative_product line 197

    Source documentation

    Arbitrary genuine equation classes may be represented and multiplied, with exact numerical order independent of the chosen equation representatives.

    theorem classOrdinaryMultiplicity_representative_product {d e : ℕ}
        (C : W16.PlaneEquationClass d) (D : W16.PlaneEquationClass e) (p : PlanePoint) :
        classOrdinaryMultiplicity
          (W16.classOfForm ((W16.classRepresentative C).mul (W16.classRepresentative D))) p =
          classOrdinaryMultiplicity C p + classOrdinaryMultiplicity D p := by
    …

    Mentions: OAI.Nagata.W16.PlaneEquationClass, OAI.Nagata.ProjectiveGeometry.PlanePoint, OAI.Nagata.ProjectiveGeometry.classOrdinaryMultiplicity, OAI.Nagata.W16.classOfForm, OAI.Nagata.W16.classRepresentative

13. theorem OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity_finset_prod line 215
14. theorem OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity_finset_prod_pow line 229
15. def OAI.Nagata.W15.weightedProductForm line 244

    Source documentation

    The actual weighted product equation, including zero coefficients and empty products. Its degree is proved by homogeneity and nonzeroness.

    def weightedProductForm {ι : Type*} (s : Finset ι) (d : ι → ℕ)
        (F : ∀ i, W16.NonzeroHomogeneousForm (d i)) (n : ι → ℕ) :
        W16.NonzeroHomogeneousForm (∑ i ∈ s, d i * n i) where
    …

16. theorem OAI.Nagata.W15.weightedProductForm_totalDegree line 251
17. theorem OAI.Nagata.W15.weightedProductForm_ordinaryMultiplicity line 256
18. theorem OAI.Nagata.W15.weightedProductForm_classMultiplicity line 272
19. theorem OAI.Nagata.W15.weightedProductForm_class_independent line 280

    Source documentation

    Replacing each component equation by another representative of the same equation class does not change the weighted product's equation class.

    theorem weightedProductForm_class_independent {ι : Type*} (s : Finset ι) (d : ι → ℕ)
        (F G : ∀ i, W16.NonzeroHomogeneousForm (d i)) (n : ι → ℕ)
        (h : ∀ i, W16.classOfForm (F i) = W16.classOfForm (G i)) :
        W16.classOfForm (weightedProductForm s d F n) =
          W16.classOfForm (weightedProductForm s d G n) := by
    …

    Mentions: OAI.Nagata.W16.classOfForm, OAI.Nagata.W15.weightedProductForm

20. def OAI.Nagata.W15.PlanePrimeComponent line 313

    Source documentation

    An actual homogeneous nonzero prime principal ideal of the ternary coordinate ring. No equation or multiplicity is assumed in this type.

    def PlanePrimeComponent := {I : Ideal TernaryPolynomial //
    …

21. def OAI.Nagata.W15.componentCurve line 317
22. def OAI.Nagata.W15.componentDegree line 328
23. def OAI.Nagata.W15.componentForm line 329
24. def OAI.Nagata.W15.componentMultiplicity line 331
25. theorem OAI.Nagata.W15.componentForm_idealCycle line 334
26. theorem OAI.Nagata.W15.equationIdealCycle_finset_prod line 338
27. def OAI.Nagata.W15.curveComponent line 348
28. def OAI.Nagata.W15.cycleProductForm line 351
29. theorem OAI.Nagata.W15.cycleProductForm_idealCycle line 357
30. theorem OAI.Nagata.W15.cycleProductForm_degree line 374
31. theorem OAI.Nagata.W15.cycleProductForm_multiplicity line 379
32. def OAI.Nagata.W15.curveOrdinaryMultiplicity line 397

    Source documentation

    Actual ordinary multiplicity of the reconstructed curve equation.

    Distinct definitions of this name: ComparatorChallenges/Nagata.lean:329 (different declaration text). Qualify references as OAI.Nagata.W15.curveOrdinaryMultiplicity@path.

    def curveOrdinaryMultiplicity (C : EffectivePlaneCurve) (p : PlanePoint) : ℕ :=
    …

33. theorem OAI.Nagata.W15.curveMultiplicityAtLeast_iff_le_ordinaryMultiplicity line 400
34. theorem OAI.Nagata.W15.curveOrdinaryMultiplicity_eq_form line 407

    Source documentation

    The number agrees with every homogeneous equation realizing the same full cycle, not merely the same underlying zero set.

    theorem curveOrdinaryMultiplicity_eq_form (C : EffectivePlaneCurve) {d : ℕ}
        (F : W16.NonzeroHomogeneousForm d) (hcycle : equationIdealCycle F.polynomial = C.val)
        (p : PlanePoint) : curveOrdinaryMultiplicity C p = formOrdinaryMultiplicity F p := by
    …

35. theorem OAI.Nagata.W15.curveDegree_eq_component_sum line 418
36. theorem OAI.Nagata.W15.curveOrdinaryMultiplicity_eq_component_sum line 424
37. theorem OAI.Nagata.W15.componentDegree_eq_formDegree line 430
38. theorem OAI.Nagata.W15.componentMultiplicity_eq_form line 436
39. theorem OAI.Nagata.W15.curveOrdinaryMultiplicity_eq_class line 442
40. theorem OAI.Nagata.W15.curveMultiplicityAtLeast_iff_component_sum line 447