EffectiveCurves.lean`

42 declarations, 0 contain sorry, 0 declared as axioms

Effective cycles, their equations, and equation-independent degrees

theorem OAI.Nagata.Workers.W10.ternary_unit_eq_C line 19
Source documentation
Every polynomial unit over C is exactly a nonzero constant scalar.
```
theorem ternary_unit_eq_C (u : TernaryPolynomialˣ) :
    ∃ a : ℂˣ, (u : TernaryPolynomial) = MvPolynomial.C (a : ℂ) := by
…
```
theorem OAI.Nagata.Workers.W10.associated_iff_complex_unit line 30
Source documentation
Association is precisely equality up to nonzero complex scalar, including for reducible and nonreduced polynomials.
```
theorem associated_iff_complex_unit (F G : TernaryPolynomial) :
    Associated F G ↔ ∃ a : ℂˣ, MvPolynomial.C (a : ℂ) * G = F := by
…
```
theorem OAI.Nagata.Workers.W10.associated_totalDegree_eq line 41
Source documentation
Associated nonzero equations have equal actual total degrees.
```
theorem associated_totalDegree_eq {F G : TernaryPolynomial} (hF : F ≠ 0)
    (h : Associated F G) : F.totalDegree = G.totalDegree := by
…
```
theorem OAI.Nagata.Workers.W10.classOfForm_eq_iff_idealCycle line 48
Source documentation
The full ideal cycle identifies exactly the projective equation class at a fixed degree, not merely the underlying set of zeros.
```
theorem classOfForm_eq_iff_idealCycle {d : ℕ} (F G : NonzeroHomogeneousForm d) :
    classOfForm F = classOfForm G ↔ equationIdealCycle F.polynomial = equationIdealCycle G.polynomial := by
…
```
def OAI.Nagata.Workers.W10.EffectivePlaneCurve line 67
Source documentation
A nonzero finite effective cycle of genuine homogeneous prime principal ideals in C[X0,X1,X2]. The weights retain repeated components.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:283 (same statement text; different proof or body). Qualify references as OAI.Nagata.Workers.W10.EffectivePlaneCurve@path.
```
def EffectivePlaneCurve := {D : Ideal TernaryPolynomial →₀ ℕ //
…
```
def OAI.Nagata.Workers.W10.curveEquation line 72
Source documentation
Reconstruct an actual homogeneous equation from the ideal cycle.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:289 (different declaration text). Qualify references as OAI.Nagata.Workers.W10.curveEquation@path.
```
def curveEquation (C : EffectivePlaneCurve) : TernaryPolynomial :=
…
```
theorem OAI.Nagata.Workers.W10.curveEquation_spec line 75
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:293 (different declaration text). Qualify references as OAI.Nagata.Workers.W10.curveEquation_spec@path.
theorem OAI.Nagata.Workers.W10.curveEquation_nonzero line 80
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:300 (different declaration text). Qualify references as OAI.Nagata.Workers.W10.curveEquation_nonzero@path.
def OAI.Nagata.Workers.W10.curveDegree line 83
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:303 (different declaration text). Qualify references as OAI.Nagata.Workers.W10.curveDegree@path.
theorem OAI.Nagata.Workers.W10.curveDegree_pos line 85
theorem OAI.Nagata.Workers.W10.curveEquation_homogeneous line 88
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:305 (different declaration text). Qualify references as OAI.Nagata.Workers.W10.curveEquation_homogeneous@path.
theorem OAI.Nagata.Workers.W10.curveEquation_idealCycle line 91
def OAI.Nagata.Workers.W10.curveForm line 95
Source documentation
The chosen reconstruction is packaged as a genuine nonzero homogeneous form.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:309 (different declaration text). Qualify references as OAI.Nagata.Workers.W10.curveForm@path.
```
def curveForm (C : EffectivePlaneCurve) : NonzeroHomogeneousForm (curveDegree C) :=
…
```
def OAI.Nagata.Workers.W10.curveEquationClass line 98
theorem OAI.Nagata.Workers.W10.equationIdealCycle_classRepresentative line 103
Source documentation
Replacing a form by the chosen representative of its projective class preserves the entire ideal cycle, including every repeated-factor weight.
```
theorem equationIdealCycle_classRepresentative {d : ℕ} (F : NonzeroHomogeneousForm d) :
    equationIdealCycle (classRepresentative (classOfForm F)).polynomial = equationIdealCycle F.polynomial :=
…
```
def OAI.Nagata.Workers.W10.curveOfEquation line 108
Source documentation
An actual positive-degree projective equation class gives its zero-divisor cycle.
```
def curveOfEquation (E : PositivePlaneEquation) : EffectivePlaneCurve :=
…
```
theorem OAI.Nagata.Workers.W10.curveOfEquation_curveEquationClass line 123
theorem OAI.Nagata.Workers.W10.curveOfEquation_injective line 132
Source documentation
Even across degrees, equal ideal cycles identify precisely the same positive projective equation class.
```
theorem curveOfEquation_injective : Function.Injective curveOfEquation := by
…
```
Mentions: OAI.Nagata.Workers.W10.curveOfEquation
theorem OAI.Nagata.Workers.W10.curveEquationClass_curveOfEquation line 150
def OAI.Nagata.Workers.W10.planeCurveEquationEquiv line 157
Source documentation
Full equivalence between genuine positive effective ideal cycles and all positive-degree projective equation classes. Repeated components are preserved.
```
def planeCurveEquationEquiv : EffectivePlaneCurve ≃ PositivePlaneEquation where
…
```
theorem OAI.Nagata.Workers.W10.curveEquation_associated line 176
Source documentation
Any nonzero equation with this full ideal cycle differs from the chosen equation by an actual nonzero complex scalar.
```
theorem curveEquation_associated (C : EffectivePlaneCurve) {F : TernaryPolynomial}
    (hF : F ≠ 0) (hcycle : equationIdealCycle F = C.val) :
    Associated (curveEquation C) F :=
…
```
theorem OAI.Nagata.Workers.W10.curveDegree_eq_totalDegree line 184
Source documentation
Degree is independent of the equation, without a homogeneity assumption on the alternate representative (homogeneity follows from its cycle).
```
theorem curveDegree_eq_totalDegree (C : EffectivePlaneCurve) {F : TernaryPolynomial}
    (hF : F ≠ 0) (hcycle : equationIdealCycle F = C.val) :
    curveDegree C = F.totalDegree :=
…
```

theorem OAI.Nagata.Workers.W10.curveDegree_eq_formDegree line 190

Source documentation

Every alternative homogeneous representative has exactly this degree.

theorem curveDegree_eq_formDegree (C : EffectivePlaneCurve) {d : ℕ}
    (F : NonzeroHomogeneousForm d) (hcycle : equationIdealCycle F.polynomial = C.val) :
    curveDegree C = d :=
…

def OAI.Nagata.Workers.W10.curveMultiplicityAtLeast line 197
Source documentation
Local multiplicity uses the actual affine chart maximal-ideal powers, equivalently the actual regular local-ring order used by the manuscript.
```
def curveMultiplicityAtLeast (C : EffectivePlaneCurve) (p : PlanePoint) (m : ℕ) : Prop :=
…
```
theorem OAI.Nagata.Workers.W10.curveMultiplicityAtLeast_iff_equation line 200
theorem OAI.Nagata.Workers.W10.curveMultiplicityAtLeast_iff_localOrder line 208
def OAI.Nagata.Workers.W10.curveChartIdeal line 216
Source documentation
The genuine principal ideal on every affine plane chart; no radical is taken.
```
def curveChartIdeal (C : EffectivePlaneCurve) (c : Fin 3) :
    Ideal (MvPolynomial (ChartVariables c) ℂ) :=
…
```
theorem OAI.Nagata.Workers.W10.curveChartIdeal_eq_equation line 220
theorem OAI.Nagata.Workers.W10.curveEquationClass_multiplicity line 229
Source documentation
The reconstructed projective equation class has precisely the cycle's local order.
```
theorem curveEquationClass_multiplicity (C : EffectivePlaneCurve) (p : PlanePoint) (m : ℕ) :
    classMultiplicityAtLeast (curveEquationClass C).equationClass p m ↔
      curveMultiplicityAtLeast C p m :=
…
```
Mentions: OAI.Nagata.Workers.W10.curveEquationClass, OAI.Nagata.Workers.W10.curveMultiplicityAtLeast
theorem OAI.Nagata.Workers.W10.curveEquationClass_chartIdeal line 234
theorem OAI.Nagata.Workers.W10.curveOfEquation_degree line 238
theorem OAI.Nagata.Workers.W10.curveOfEquation_multiplicity line 245
Source documentation
Passing from a positive projective equation class to its cycle preserves ordinary local multiplicity exactly.
```
theorem curveOfEquation_multiplicity (E : PositivePlaneEquation) (p : PlanePoint) (m : ℕ) :
    curveMultiplicityAtLeast (curveOfEquation E) p m ↔
      classMultiplicityAtLeast E.equationClass p m := by
…
```
Mentions: OAI.Nagata.Workers.W10.curveMultiplicityAtLeast, OAI.Nagata.Workers.W10.curveOfEquation
def OAI.Nagata.Workers.W10.curveOfForm line 262
theorem OAI.Nagata.Workers.W10.curveOfForm_cycle line 265
theorem OAI.Nagata.Workers.W10.curveOfForm_degree line 269

theorem OAI.Nagata.Workers.W10.curveOfForm_mul_cycle line 274

Source documentation

The product equation represents exactly the sum of effective cycles.

theorem curveOfForm_mul_cycle {d e : ℕ} (F : NonzeroHomogeneousForm d)
    (G : NonzeroHomogeneousForm e) (hd : 0 < d) (he : 0 < e) :
    (curveOfForm (F.mul G) (Nat.add_pos_left hd e)).val =
      (curveOfForm F hd).val + (curveOfForm G he).val := by
…

Mentions: OAI.Nagata.Workers.W10.curveOfForm

theorem OAI.Nagata.Workers.W10.curveOfForm_pow_cycle line 283
Source documentation
Repeated components retain every multiplicity: a positive power scales the whole natural-valued cycle, rather than passing to its reduced support.
```
theorem curveOfForm_pow_cycle {d : ℕ} (F : NonzeroHomogeneousForm d)
    (hd : 0 < d) (N : ℕ) (hN : 0 < N) :
    (curveOfForm (F.pow N) (Nat.mul_pos hd hN)).val = N • (curveOfForm F hd).val := by
…
```
Mentions: OAI.Nagata.Workers.W10.curveOfForm
def OAI.Nagata.Workers.W10.coordinateLineForm line 301
def OAI.Nagata.Workers.W10.coordinateLineCurve line 304
instance OAI.Nagata.Workers.W10.effectivePlaneCurveNonempty line 306
theorem OAI.Nagata.Workers.W10.coordinateLineCurve_degree line 308
theorem OAI.Nagata.Workers.W10.coordinateLineCurve_cycle line 311