ChartMultiplicityBridge.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Equivalence of projective and affine ideal-power multiplicity

abbrev OAI.Nagata.ProjectiveGeometry.ChartLocalRing line 19
def OAI.Nagata.ProjectiveGeometry.localHomogeneousCoordinates line 24
Source documentation
The homogeneous coordinate functions in the genuine local ring of chart b; the distinguished coordinate is one.
```
def localHomogeneousCoordinates (b : Fin 3) (p : PlanePoint) :
    Fin 3 → ChartLocalRing b p :=
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint, OAI.Nagata.ProjectiveGeometry.ChartLocalRing
theorem OAI.Nagata.ProjectiveGeometry.localHomogeneousCoordinates_isUnit line 32
Source documentation
A homogeneous coordinate which is nonzero at the point is a unit in the local ring. This is the actual denominator used on projective chart overlaps.
```
theorem localHomogeneousCoordinates_isUnit (b c : Fin 3) (p : PlanePoint)
    (hb : p.rep b ≠ 0) (hc : p.rep c ≠ 0) :
    IsUnit (localHomogeneousCoordinates b p c) := by
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint, OAI.Nagata.ProjectiveGeometry.localHomogeneousCoordinates
def OAI.Nagata.ProjectiveGeometry.localChartDenominatorUnit line 43
Source documentation
The invertible denominator for the substitution from chart c into the local ring of chart b. Its invertibility has just been proved.
```
def localChartDenominatorUnit (b c : Fin 3) (p : PlanePoint)
    (hb : p.rep b ≠ 0) (hc : p.rep c ≠ 0) : (ChartLocalRing b p)ˣ :=
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint, OAI.Nagata.ProjectiveGeometry.ChartLocalRing
theorem OAI.Nagata.ProjectiveGeometry.localChartDenominatorUnit_val line 47
def OAI.Nagata.ProjectiveGeometry.chartTransitionToLocalRing line 55
Source documentation
The concrete rational substitution on an overlap of affine projective charts, with values in the actual local ring at the target point.
```
def chartTransitionToLocalRing (b c : Fin 3) (p : PlanePoint)
    (hb : p.rep b ≠ 0) (hc : p.rep c ≠ 0) :
    MvPolynomial (ChartVariables c) ℂ →+* ChartLocalRing b p :=
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint, OAI.Nagata.ProjectiveGeometry.ChartLocalRing
theorem OAI.Nagata.ProjectiveGeometry.eval₂_dehomogenize line 64
theorem OAI.Nagata.ProjectiveGeometry.eval₂_localHomogeneousCoordinates line 77

theorem OAI.Nagata.ProjectiveGeometry.chartTransition_dehomogenize line 94

Source documentation

The source chart equation becomes the target chart equation multiplied by the actual invertible denominator to degree d.

theorem chartTransition_dehomogenize {F : MvPolynomial (Fin 3) ℂ} {d : ℕ}
    (hF : F.IsHomogeneous d) (b c : Fin 3) (p : PlanePoint)
    (hb : p.rep b ≠ 0) (hc : p.rep c ≠ 0) :
    chartTransitionToLocalRing b c p hb hc (dehomogenize c F) =
      (↑((localChartDenominatorUnit b c p hb hc)⁻¹) : ChartLocalRing b p) ^ d *
        algebraMap (MvPolynomial (ChartVariables b) ℂ) (ChartLocalRing b p)
          (dehomogenize b F) := by
…

Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint, OAI.Nagata.ProjectiveGeometry.chartTransitionToLocalRing, OAI.Nagata.ProjectiveGeometry.localChartDenominatorUnit, OAI.Nagata.ProjectiveGeometry.ChartLocalRing

theorem OAI.Nagata.ProjectiveGeometry.residueEval_localHomogeneousCoordinates line 113
theorem OAI.Nagata.ProjectiveGeometry.chartTransition_residueEval line 124
Source documentation
The actual rational substitution sends the target residue point to the source chart coordinates. This discharges evaluation compatibility.
```
theorem chartTransition_residueEval (b c : Fin 3) (p : PlanePoint)
    (hb : p.rep b ≠ 0) (hc : p.rep c ≠ 0)
    (f : MvPolynomial (ChartVariables c) ℂ) :
    AffineMultiplicity.residueEval (chartCoordinates b p)
      (chartTransitionToLocalRing b c p hb hc f) =
        MvPolynomial.eval (chartCoordinates c p) f := by
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint, OAI.Nagata.AffineMultiplicity.residueEval, OAI.Nagata.ProjectiveGeometry.chartTransitionToLocalRing

theorem OAI.Nagata.ProjectiveGeometry.orderAtLeast_map_into_kernel line 153

Source documentation

A coordinate substitution respecting evaluation transports all ideal-power orders into the kernel of the target evaluation homomorphism. This applies to rational chart substitutions after mapping into an actual local ring.

theorem orderAtLeast_map_into_kernel {σ K R : Type*} [CommRing K] [CommRing R]
    (p : σ → K) (e : MvPolynomial σ K →+* R) (ρ : R →+* K)
    (he : ∀ f, ρ (e f) = MvPolynomial.eval p f)
    (m : ℕ) (f : MvPolynomial σ K)
    (hf : AffineMultiplicity.orderAtLeast p m f) :
    e f ∈ (RingHom.ker ρ) ^ m := by
…

theorem OAI.Nagata.ProjectiveGeometry.chart_order_transport_via_residue line 168

theorem OAI.Nagata.ProjectiveGeometry.chart_order_transport line 190

Source documentation

Ordinary affine ideal-power orders agree on every projective chart overlap for a homogeneous form, at every nonnegative order.

theorem chart_order_transport {F : MvPolynomial (Fin 3) ℂ} {d : ℕ}
    (hF : F.IsHomogeneous d) (b c : Fin 3) (p : PlanePoint)
    (hb : p.rep b ≠ 0) (hc : p.rep c ≠ 0) (m : ℕ)
    (hf : AffineMultiplicity.orderAtLeast (chartCoordinates c p) m (dehomogenize c F)) :
    AffineMultiplicity.orderAtLeast (chartCoordinates b p) m (dehomogenize b F) :=
…

Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint

theorem OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast_iff_some_chart line 202

Source documentation

One containing chart suffices for every multiplicity order. All residue, localization, and homogeneous-scaling requirements have concrete witnesses.

theorem multiplicityAtLeast_iff_some_chart {F : MvPolynomial (Fin 3) ℂ} {d : ℕ}
    (hF : F.IsHomogeneous d) (p : PlanePoint) (m : ℕ) :
    multiplicityAtLeast F p m ↔
      ∃ c : Fin 3, p.rep c ≠ 0 ∧
        AffineMultiplicity.orderAtLeast (chartCoordinates c p) m (dehomogenize c F) := by
…

Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint

theorem OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast_iff_chart line 214
theorem OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast_C_mul_iff line 226
Source documentation
Nonzero scalar multiples define the same local multiplicity conditions, including every nonreduced order. This is the equation-class descent bridge.
```
theorem multiplicityAtLeast_C_mul_iff (a : ℂ) (ha : a ≠ 0)
    (F : MvPolynomial (Fin 3) ℂ) (p : PlanePoint) (m : ℕ) :
    multiplicityAtLeast (MvPolynomial.C a * F) p m ↔ multiplicityAtLeast F p m := by
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint
theorem OAI.Nagata.ProjectiveGeometry.eval_dehomogenize line 242
theorem OAI.Nagata.ProjectiveGeometry.eval_dehomogenize_homogeneous line 249

theorem OAI.Nagata.ProjectiveGeometry.chart_order_one_iff line 259

Source documentation

First-order vanishing in any containing chart agrees with vanishing of the original homogeneous form at the point's representative.

theorem chart_order_one_iff {F : MvPolynomial (Fin 3) ℂ} {d : ℕ}
    (hF : F.IsHomogeneous d) (p : PlanePoint) (c : Fin 3) (hc : p.rep c ≠ 0) :
    AffineMultiplicity.orderAtLeast (chartCoordinates c p) 1 (dehomogenize c F) ↔
      MvPolynomial.eval p.rep F = 0 := by
…

Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint

theorem OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast_one_iff line 267

theorem OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast_one_iff_some_chart line 279

Source documentation

At order one, one containing chart suffices; this is proved from the homogeneous scaling identity rather than assumed coordinate invariance.

theorem multiplicityAtLeast_one_iff_some_chart {F : MvPolynomial (Fin 3) ℂ} {d : ℕ}
    (hF : F.IsHomogeneous d) (p : PlanePoint) :
    multiplicityAtLeast F p 1 ↔
      ∃ c : Fin 3, p.rep c ≠ 0 ∧
        AffineMultiplicity.orderAtLeast (chartCoordinates c p) 1 (dehomogenize c F) := by
…

Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint

theorem OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast_iff_localOrder line 291