NormalCharts.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Analytic normal charts and their invertible Jacobians; Multiplicity in analytic normal charts; Equations for the inverse analytic normal chart

abbrev OAI.Nagata.Workers.W28.ComplexPlane line 26
def OAI.Nagata.Workers.W28.planePolynomialEval line 29
Source documentation
Evaluate an actual two-variable polynomial on the complex affine plane.
```
def planePolynomialEval (G : MvPolynomial (Fin 2) ℂ) (z : ComplexPlane) : ℂ :=
…
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane
def OAI.Nagata.Workers.W28.polynomialNormalCoordinates line 33
Source documentation
Tangential coordinate and actual polynomial defining equation.
```
def polynomialNormalCoordinates (G : MvPolynomial (Fin 2) ℂ)
    (z : ComplexPlane) : ComplexPlane := (z.1, planePolynomialEval G z)
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.planePolynomialEval
theorem OAI.Nagata.Workers.W28.planePolynomialEval_analyticAt line 36
theorem OAI.Nagata.Workers.W28.polynomialNormalCoordinates_analyticAt line 42

theorem OAI.Nagata.Workers.W28.exists_analytic_normal_chart line 50

Source documentation

If the actual Jacobian of (ζ,G) is nonsingular, it provides an open local chart whose inverse is analytic at the image of the marked point. No abstract geometric object or prescribed chart-existence field is assumed.

theorem exists_analytic_normal_chart
    (G : MvPolynomial (Fin 2) ℂ) (p : ComplexPlane)
    (hdet : (fderiv ℂ (polynomialNormalCoordinates G) p).det ≠ 0) :
    ∃ e : OpenPartialHomeomorph ComplexPlane ComplexPlane,
      (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G ∧
      p ∈ e.source ∧
      AnalyticAt ℂ e.symm (polynomialNormalCoordinates G p) := by
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.polynomialNormalCoordinates

theorem OAI.Nagata.Workers.W28.polynomial_order_in_inverse_chart line 88

Source documentation

Actual polynomial ideal-power multiplicity is preserved by the inverse of a genuine analytic local chart at its marked image.

theorem polynomial_order_in_inverse_chart
    (P : MvPolynomial (Fin 2) ℂ)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (p : ComplexPlane) (hp : p ∈ e.source)
    (he : AnalyticAt ℂ e.symm (e p)) (m : ℕ)
    (hP : Nagata.AffineMultiplicity.orderAtLeast
      (fun i : Fin 2 => if i = 0 then p.1 else p.2) m P) :
    HasAnalyticOrderAtLeast (𝕜 := ℂ) (planePolynomialEval P ∘ e.symm) (e p) m := by
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast, OAI.Nagata.Workers.W28.planePolynomialEval

theorem OAI.Nagata.Workers.W28.polynomial_order_in_rescaled_inverse_chart line 106

Source documentation

At any actual point of the inverse chart, normal rescaling transports polynomial ordinary multiplicity to the rescaled local analytic function. The polynomial point in the hypothesis is the actual inverse image of (u,s*w).

theorem polynomial_order_in_rescaled_inverse_chart
    (P : MvPolynomial (Fin 2) ℂ)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (s : ℂ) (q : ComplexPlane) (m : ℕ)
    (he : AnalyticAt ℂ e.symm (analyticNormalScale s q))
    (hP : Nagata.AffineMultiplicity.orderAtLeast
      (fun i : Fin 2 => if i = 0 then (e.symm (analyticNormalScale s q)).1
        else (e.symm (analyticNormalScale s q)).2) m P) :
    HasAnalyticOrderAtLeast (𝕜 := ℂ)
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.analyticNormalScale, OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast

theorem OAI.Nagata.Workers.W28.exists_normal_chart_with_locally_analytic_inverse line 121

Source documentation

The analytic inverse obtained from a nonsingular polynomial chart remains analytic throughout some genuine neighborhood of the marked chart image.

theorem exists_normal_chart_with_locally_analytic_inverse
    (G : MvPolynomial (Fin 2) ℂ) (p : ComplexPlane)
    (hdet : (fderiv ℂ (polynomialNormalCoordinates G) p).det ≠ 0) :
    ∃ e : OpenPartialHomeomorph ComplexPlane ComplexPlane,
      (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G ∧
      p ∈ e.source ∧ ∀ᶠ y in 𝓝 (e p), AnalyticAt ℂ e.symm y := by
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.polynomialNormalCoordinates

def OAI.Nagata.Workers.W28.polynomialGradient line 143
Source documentation
The continuous linear map given by the two actual polynomial partials.
```
def polynomialGradient (G : MvPolynomial (Fin 2) ℂ) (p : ComplexPlane) :
    ComplexPlane →L[ℂ] ℂ :=
…
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane
theorem OAI.Nagata.Workers.W28.planePolynomialEval_hasFDerivAt line 149
Source documentation
Algebraic partial derivatives agree with the complex Fréchet derivative.
```
theorem planePolynomialEval_hasFDerivAt (G : MvPolynomial (Fin 2) ℂ)
    (p : ComplexPlane) :
    HasFDerivAt (planePolynomialEval G) (polynomialGradient G p) p := by
…
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.Workers.W28.polynomialGradient
theorem OAI.Nagata.Workers.W28.polynomialNormalCoordinates_hasFDerivAt line 203
theorem OAI.Nagata.Workers.W28.polynomialNormalCoordinates_det line 211
Source documentation
Exact Jacobian identity: det D(X,G) = ∂G/∂Y.
```
theorem polynomialNormalCoordinates_det
    (G : MvPolynomial (Fin 2) ℂ) (p : ComplexPlane) :
    (fderiv ℂ (polynomialNormalCoordinates G) p).det =
      planePolynomialEval (MvPolynomial.pderiv 1 G) p := by
…
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.polynomialNormalCoordinates, OAI.Nagata.Workers.W28.planePolynomialEval

theorem OAI.Nagata.Workers.W28.exists_analytic_normal_chart_of_partial_ne_zero line 224

Source documentation

A nonzero actual normal partial derivative supplies the local analytic chart.

theorem exists_analytic_normal_chart_of_partial_ne_zero
    (G : MvPolynomial (Fin 2) ℂ) (p : ComplexPlane)
    (hpartial : planePolynomialEval (MvPolynomial.pderiv 1 G) p ≠ 0) :
    ∃ e : OpenPartialHomeomorph ComplexPlane ComplexPlane,
      (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G ∧
      p ∈ e.source ∧
      AnalyticAt ℂ e.symm (polynomialNormalCoordinates G p) := by
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.Workers.W28.polynomialNormalCoordinates

def OAI.Nagata.Workers.W28.polynomialOtherCoordinates line 235
Source documentation
The alternative tangential coordinate, used when the other partial is nonzero.
```
def polynomialOtherCoordinates (G : MvPolynomial (Fin 2) ℂ)
    (z : ComplexPlane) : ComplexPlane := (z.2, planePolynomialEval G z)
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.planePolynomialEval
theorem OAI.Nagata.Workers.W28.polynomialOtherCoordinates_det line 238
theorem OAI.Nagata.Workers.W28.exists_analytic_other_chart_of_partial_ne_zero line 254

theorem OAI.Nagata.Workers.W28.exists_analytic_chart_of_nonzero_gradient line 282

Source documentation

A nonzero polynomial gradient supplies one of the two genuine normal charts.

theorem exists_analytic_chart_of_nonzero_gradient
    (G : MvPolynomial (Fin 2) ℂ) (p : ComplexPlane)
    (hgradient : planePolynomialEval (MvPolynomial.pderiv 0 G) p ≠ 0 ∨
      planePolynomialEval (MvPolynomial.pderiv 1 G) p ≠ 0) :
    ∃ e : OpenPartialHomeomorph ComplexPlane ComplexPlane,
      ((e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G ∨
       (e : ComplexPlane → ComplexPlane) = polynomialOtherCoordinates G) ∧
      p ∈ e.source ∧ AnalyticAt ℂ e.symm (e p) := by
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.Workers.W28.polynomialNormalCoordinates, OAI.Nagata.Workers.W28.polynomialOtherCoordinates

theorem OAI.Nagata.Workers.W28.inverse_normal_chart_first line 307

Source documentation

The inverse chart's tangential coordinate is the actual first coordinate.

theorem inverse_normal_chart_first
    (G : MvPolynomial (Fin 2) ℂ)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G)
    (q : ComplexPlane) (hq : q ∈ e.target) : (e.symm q).1 = q.1 := by
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.polynomialNormalCoordinates

theorem OAI.Nagata.Workers.W28.inverse_normal_chart_equation line 317
Source documentation
The defining polynomial evaluated in genuine normal coordinates is exactly that normal coordinate, as an identity throughout the chart target.
```
theorem inverse_normal_chart_equation
    (G : MvPolynomial (Fin 2) ℂ)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G)
    (q : ComplexPlane) (hq : q ∈ e.target) : planePolynomialEval G (e.symm q) = q.2 := by
…
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.polynomialNormalCoordinates, OAI.Nagata.Workers.W28.planePolynomialEval

theorem OAI.Nagata.Workers.W28.rescaled_inverse_normal_chart_equation line 326

Source documentation

Exact defining-equation identity after the normal degeneration substitution.

theorem rescaled_inverse_normal_chart_equation
    (G : MvPolynomial (Fin 2) ℂ)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G)
    (s : ℂ) (q : ComplexPlane) (hq : analyticNormalScale s q ∈ e.target) :
    planePolynomialEval G (e.symm (analyticNormalScale s q)) = s * q.2 :=
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.polynomialNormalCoordinates, OAI.Nagata.Workers.W28.analyticNormalScale, OAI.Nagata.Workers.W28.planePolynomialEval