OAI/AlgebraicGeometry/PlaneCurves/ProjectiveMultiplicity.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Nagata.W16.HomogeneousFormSpace line 27
2. abbrev OAI.Nagata.W16.PlaneEquationClass line 31

   Source documentation

   Nonzero homogeneous equations modulo nonzero complex scalar.

   abbrev PlaneEquationClass (d : ℕ) := Projectivization ℂ (HomogeneousFormSpace d)

   Mentions: OAI.Nagata.W16.HomogeneousFormSpace

3. structure OAI.Nagata.W16.PositivePlaneEquation line 35

   Source documentation

   A positive-degree equation class. The Cartier-divisor correspondence is not included as a structure field or an assumption.

   structure PositivePlaneEquation where
   …

4. def OAI.Nagata.W16.formVector line 40
5. theorem OAI.Nagata.W16.formVector_ne_zero line 43
6. def OAI.Nagata.W16.classOfForm line 47
7. def OAI.Nagata.W16.classRepresentative line 50
8. theorem OAI.Nagata.W16.classOfForm_representative line 58
9. theorem OAI.Nagata.W16.classOfForm_surjective line 62
10. theorem OAI.Nagata.W16.classOfForm_eq_iff line 68

    Source documentation

    This equality criterion identifies equations only by units of ℂ.

    theorem classOfForm_eq_iff {d : ℕ} (F G : NonzeroHomogeneousForm d) :
        classOfForm F = classOfForm G ↔
          ∃ a : ℂˣ, MvPolynomial.C (a : ℂ) * G.polynomial = F.polynomial := by
    …

    Mentions: OAI.Nagata.W16.classOfForm

11. theorem OAI.Nagata.W16.representative_classOfForm line 83
12. theorem OAI.Nagata.W16.representative_totalDegree line 93
13. def OAI.Nagata.W16.classMultiplicityAtLeast line 99

    Source documentation

    The local-order lower bound of an equation class, using the actual chart coordinate rings and their point maximal ideals.

    def classMultiplicityAtLeast {d : ℕ} (C : PlaneEquationClass d)
        (p : PlanePoint) (m : ℕ) : Prop :=
    …

    Mentions: OAI.Nagata.W16.PlaneEquationClass

14. theorem OAI.Nagata.W16.classMultiplicityAtLeast_classOfForm line 103
15. theorem OAI.Nagata.W16.classMultiplicityAtLeast_iff_localOrder line 111
16. def OAI.Nagata.W16.classZeroLocus line 120

    Source documentation

    The underlying projective zero locus is kept separately from the equation class: it is not the equivalence relation defining the class.

    def classZeroLocus {d : ℕ} (C : PlaneEquationClass d) : Set PlanePoint :=
    …

    Mentions: OAI.Nagata.W16.PlaneEquationClass

17. theorem OAI.Nagata.W16.classZeroLocus_classOfForm line 123
18. theorem OAI.Nagata.W16.mem_classZeroLocus_iff_order_one line 130
19. def OAI.Nagata.W16.classChartIdeal line 136

    Source documentation

    The full principal ideal of the local equation, without radicalization. In particular, powers of equations retain their nonreduced structure.

    def classChartIdeal {d : ℕ} (C : PlaneEquationClass d) (c : Fin 3) :
        Ideal (MvPolynomial (ChartVariables c) ℂ) :=
    …

    Mentions: OAI.Nagata.W16.PlaneEquationClass

20. theorem OAI.Nagata.W16.classChartIdeal_classOfForm line 140
21. theorem OAI.Nagata.W16.classChartEquation_ne_zero line 149

    Source documentation

    The chart equation is nonzero, so its ideal defines a genuine principal hypersurface equation, including its multiplicity structure.

    theorem classChartEquation_ne_zero {d : ℕ} (C : PlaneEquationClass d) (c : Fin 3) :
        dehomogenize c (classRepresentative C).polynomial ≠ 0 :=
    …

    Mentions: OAI.Nagata.W16.PlaneEquationClass, OAI.Nagata.W16.classRepresentative

22. theorem OAI.Nagata.W16.classChartIdeal_mul line 154

    Source documentation

    The full chart ideal of a product is the product of its chart ideals.

    theorem classChartIdeal_mul {d e : ℕ} (F : NonzeroHomogeneousForm d)
        (G : NonzeroHomogeneousForm e) (c : Fin 3) :
        classChartIdeal (classOfForm (F.mul G)) c =
          classChartIdeal (classOfForm F) c * classChartIdeal (classOfForm G) c := by
    …

    Mentions: OAI.Nagata.W16.classChartIdeal, OAI.Nagata.W16.classOfForm

23. theorem OAI.Nagata.W16.classChartIdeal_pow line 164

    Source documentation

    Raising an equation to the Nth power raises its actual principal chart ideal to the Nth power. This explicitly preserves nonreduced structure.

    theorem classChartIdeal_pow {d : ℕ} (F : NonzeroHomogeneousForm d)
        (c : Fin 3) (N : ℕ) :
        classChartIdeal (classOfForm (F.pow N)) c = classChartIdeal (classOfForm F) c ^ N := by
    …

    Mentions: OAI.Nagata.W16.classChartIdeal, OAI.Nagata.W16.classOfForm

24. theorem OAI.Nagata.W16.classChartIdeal_local_compatibility line 173

    Source documentation

    The full principal chart ideals agree after transport into the actual local ring at a point of an overlap. The transition factor is a proved unit.

    theorem classChartIdeal_local_compatibility {d : ℕ} (C : PlaneEquationClass d)
        (b c : Fin 3) (p : PlanePoint) (hb : p.rep b ≠ 0) (hc : p.rep c ≠ 0) :
        Ideal.map (chartTransitionToLocalRing b c p hb hc) (classChartIdeal C c) =
          Ideal.map
            (algebraMap (MvPolynomial (ChartVariables b) ℂ) (ChartLocalRing b p))
            (classChartIdeal C b) := by
    …

    Mentions: OAI.Nagata.W16.PlaneEquationClass, OAI.Nagata.W16.classChartIdeal

25. def OAI.Nagata.ProjectiveGeometry.formOrdinaryMultiplicity line 202

    Distinct definitions of this name: ComparatorChallenges/Nagata.lean:316 (different declaration text). Qualify references as OAI.Nagata.ProjectiveGeometry.formOrdinaryMultiplicity@path.

26. theorem OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast_iff_le_formOrdinaryMultiplicity line 209
27. theorem OAI.Nagata.ProjectiveGeometry.formOrdinaryMultiplicity_eq_chart line 219
28. theorem OAI.Nagata.ProjectiveGeometry.formOrdinaryMultiplicity_attained line 238
29. def OAI.Nagata.ProjectiveGeometry.classOrdinaryMultiplicity line 250
30. theorem OAI.Nagata.ProjectiveGeometry.classMultiplicityAtLeast_iff_le_classOrdinaryMultiplicity line 253
31. theorem OAI.Nagata.ProjectiveGeometry.classOrdinaryMultiplicity_classOfForm line 258