NormalPolynomials.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Normal frame identities, restricted polynomials, and automorphy

theorem OAI.Nagata.Workers.W17.differentiableAt_mvPolynomial_section_eval line 21

Source documentation

Evaluating an actual multivariate polynomial in holomorphic coordinate functions gives a holomorphic function on their common genuine domain.

theorem differentiableAt_mvPolynomial_section_eval
    {σ : Type*} {τ L : ℂ} {N : ℤ}
    (X : σ → Nagata.W08.automorphicSections τ N L)
    (T : MvPolynomial σ ℂ) (z : ℂ) (hz : z ≠ 0) :
    DifferentiableAt ℂ (fun w => MvPolynomial.eval (fun i => (X i).val w) T) z := by
…

Mentions: OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.Workers.W17.homogeneous_section_eval_automorphy line 36

Source documentation

Homogeneous evaluation has the exact multiplied degree and multiplier.

theorem homogeneous_section_eval_automorphy
    {σ : Type*} {τ L : ℂ} {N : ℤ}
    (X : σ → Nagata.W08.automorphicSections τ N L)
    (T : MvPolynomial σ ℂ) (n : ℕ) (hT : T.IsHomogeneous n)
    (z : ℂ) (hz : z ≠ 0) :
    MvPolynomial.eval (fun i => (X i).val (τ*z)) T =
      L^n * z^(-(N*(n:ℤ))) * MvPolynomial.eval (fun i => (X i).val z) T := by
…

Mentions: OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.Workers.W17.homogeneous_eval_mem_automorphicSections line 56

Source documentation

The forced-zero extension is an actual section with the precise degree. The punctured-domain convention is preserved even for constant polynomials.

theorem homogeneous_eval_mem_automorphicSections
    {σ : Type*} {τ L : ℂ} {N : ℤ} (hτ : τ ≠ 0)
    (X : σ → Nagata.W08.automorphicSections τ N L)
    (T : MvPolynomial σ ℂ) (n : ℕ) (hT : T.IsHomogeneous n) :
    Nagata.W08.normalizeAtZero (fun z => MvPolynomial.eval (fun i => (X i).val z) T) ∈
      Nagata.W08.automorphicSections τ (N*(n:ℤ)) (L^n) := by
…

Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.W08.normalizeAtZero

def OAI.Nagata.Workers.W17.restrictedCoefficient line 83
theorem OAI.Nagata.Workers.W17.restrictedCoefficient_zero line 86
def OAI.Nagata.Workers.W17.restrictedNormalPolynomial line 91
theorem OAI.Nagata.Workers.W17.restrictedNormalPolynomial_coeff line 96

theorem OAI.Nagata.Workers.W17.restrictedNormalPolynomial_bound line 101

Source documentation

The finite degree bound survives restriction, including at the forced-zero origin.

theorem restrictedNormalPolynomial_bound
    (X : σ → ℂ → ℂ) (F : Polynomial (MvPolynomial σ ℂ)) (N : ℕ)
    (hF : ∀ j, N < j → F.coeff j = 0) :
    ∀ j, N < j → (restrictedNormalPolynomial X F).coeff j = 0 := by
…

Mentions: OAI.Nagata.Workers.W17.restrictedNormalPolynomial

theorem OAI.Nagata.Workers.W17.restrictedNormalPolynomial_ne_zero line 109

Source documentation

A genuine coefficient evaluation witness proves the restricted polynomial nonzero.

theorem restrictedNormalPolynomial_ne_zero
    (X : σ → ℂ → ℂ) (F : Polynomial (MvPolynomial σ ℂ))
    (hw : ∃ j z, z ≠ 0 ∧ MvPolynomial.eval (fun i => X i z) (F.coeff j) ≠ 0) :
    restrictedNormalPolynomial X F ≠ 0 := by
…

Mentions: OAI.Nagata.Workers.W17.restrictedNormalPolynomial

def OAI.Nagata.Workers.W17.functionEvaluation line 121
Source documentation
Evaluation at a genuine punctured-plane point is a unital ring map.
```
def functionEvaluation (z : ℂ) : (ℂ → ℂ) →+* ℂ where
…
```

theorem OAI.Nagata.Workers.W17.restrictedNormalPolynomial_map_evaluation line 129

Source documentation

Coefficient restriction commutes with every genuine point evaluation.

theorem restrictedNormalPolynomial_map_evaluation
    (X : σ → ℂ → ℂ) (F : Polynomial (MvPolynomial σ ℂ)) (z : ℂ) (hz : z ≠ 0) :
    (restrictedNormalPolynomial X F).map (functionEvaluation z) =
      F.map (MvPolynomial.eval (fun i => X i z)) := by
…

Mentions: OAI.Nagata.Workers.W17.restrictedNormalPolynomial, OAI.Nagata.Workers.W17.functionEvaluation

theorem OAI.Nagata.Workers.W17.restrictedNormalPolynomial_scalarExpression line 139

Source documentation

Exact scalar expression in the covering frame, needed for the local normal jets.

theorem restrictedNormalPolynomial_scalarExpression
    (X : σ → ℂ → ℂ) (F : Polynomial (MvPolynomial σ ℂ))
    (z w : ℂ) (hz : z ≠ 0) :
    Nagata.CoefficientSpaces.scalarExpression (restrictedNormalPolynomial X F) z w =
      (F.map (MvPolynomial.eval (fun i => X i z))).eval w := by
…

Mentions: OAI.Nagata.CoefficientSpaces.scalarExpression, OAI.Nagata.Workers.W17.restrictedNormalPolynomial

theorem OAI.Nagata.Workers.W17.restrictedNormalPolynomial_source_sections line 150

theorem OAI.Nagata.Workers.W17.eval_directChartHom line 181

Source documentation

Evaluation commutes with the actual two-variable projective chart map.

theorem eval_directChartHom (c : Fin 3) (T : MvPolynomial (Fin 3) ℂ)
    (v : Fin 2 → ℂ) :
    MvPolynomial.eval v (Nagata.W27.directChartHom c T) =
      MvPolynomial.eval (Fin.insertNth (α := fun _ : Fin 3 => ℂ) c 1 v) T := by
…

Mentions: OAI.Nagata.W27.directChartHom

theorem OAI.Nagata.Workers.W17.scaled_chart_vector line 199

Source documentation

Normalizing a nonzero chart coordinate reconstructs the genuine cone vector.

theorem scaled_chart_vector (c : Fin 3) (x : Fin 3 → ℂ) (hx : x c ≠ 0) :
    (x c) • Fin.insertNth (α := fun _ : Fin 3 => ℂ) c 1 (fun b => x (c.succAbove b) / x c) = x := by
…

theorem OAI.Nagata.Workers.W17.normal_polynomial_frame_identity line 210

Source documentation

The homogeneous normal polynomial transforms by weight d, and its fiber coordinate by weight k. This supplies the exact covering-frame scalar identity.

theorem normal_polynomial_frame_identity
    (I : Finset ℕ) (j : ℕ → ℕ) (T : ℕ → MvPolynomial (Fin 3) ℂ)
    (d k : ℕ) (hhom : ∀ α ∈ I, (T α).IsHomogeneous (d-k*j α))
    (hbound : ∀ α ∈ I, k*j α ≤ d)
    (c : Fin 3) (x : Fin 3 → ℂ) (hx : x c ≠ 0) (w : ℂ) :
    (∑ α ∈ I, w^j α * MvPolynomial.eval x (T α)) =
      (x c)^d * ∑ α ∈ I, (w/(x c)^k)^j α *
        MvPolynomial.eval (fun b => x (c.succAbove b)/x c)
          (Nagata.W27.directChartHom c (T α)) := by
…

Mentions: OAI.Nagata.W27.directChartHom

theorem OAI.Nagata.Workers.W17.restrictedNormalPolynomial_ne_zero_of_principal_relations line 236

Source documentation

The actual restriction of a polynomial with nonzero residue remains nonzero once the actual ideal of coordinate relations is identified with the equation.

theorem restrictedNormalPolynomial_ne_zero_of_principal_relations
    (X : Fin 3 → ℂ → ℂ) (G : MvPolynomial (Fin 3) ℂ)
    (hrelations : Nagata.Workers.W25.polynomialRelationIdeal X = Ideal.span ({G} : Set _))
    (F : Polynomial (MvPolynomial (Fin 3) ℂ))
    (hF : F.map (Ideal.Quotient.mk (Ideal.span ({G} : Set (MvPolynomial (Fin 3) ℂ)))) ≠ 0) :
    restrictedNormalPolynomial X F ≠ 0 := by
…

Mentions: OAI.Nagata.Workers.W25.polynomialRelationIdeal, OAI.Nagata.Workers.W17.restrictedNormalPolynomial

def OAI.Nagata.Workers.W17.affineSwap line 267
Source documentation
The genuine polynomial-ring equivalence exchanging the two affine variables.
```
def affineSwap : MvPolynomial (Fin 2) ℂ ≃+* MvPolynomial (Fin 2) ℂ :=
…
```
theorem OAI.Nagata.Workers.W17.eval_affineSwap line 270

theorem OAI.Nagata.Workers.W17.order_affineSwap_iff line 280

Source documentation

Every actual ordinary multiplicity condition survives the coordinate swap.

theorem order_affineSwap_iff (P : MvPolynomial (Fin 2) ℂ) (p : ComplexPlane) (m : ℕ) :
    Nagata.AffineMultiplicity.orderAtLeast
      (fun i : Fin 2 => if i = 0 then p.2 else p.1) m (affineSwap P) ↔
    Nagata.AffineMultiplicity.orderAtLeast
      (fun i : Fin 2 => if i = 0 then p.1 else p.2) m P := by
…

Mentions: OAI.Nagata.Workers.W17.affineSwap

theorem OAI.Nagata.Workers.W17.affineSwap_factoredPlaneFamily line 290

Source documentation

Swapping the actual variables commutes with the finite G-adic family.

theorem affineSwap_factoredPlaneFamily
    (I : Finset ℕ) (j : ℕ → ℕ) (R : ℕ → MvPolynomial (Fin 2) ℂ)
    (G : MvPolynomial (Fin 2) ℂ) (s : ℂ) :
    affineSwap (factoredPlaneFamily I j R G s) =
      factoredPlaneFamily I j (fun α => affineSwap (R α)) (affineSwap G) s := by
…

Mentions: OAI.Nagata.Workers.W17.affineSwap

theorem OAI.Nagata.Workers.W17.partialY_affineSwap line 298

Source documentation

The alternative normal partial becomes the standard one after swapping.

theorem partialY_affineSwap (G : MvPolynomial (Fin 2) ℂ) (p : ComplexPlane) :
    planePolynomialEval (MvPolynomial.pderiv 1 (affineSwap G)) p.swap =
      planePolynomialEval (MvPolynomial.pderiv 0 G) p := by
…

Mentions: OAI.Nagata.Workers.W17.affineSwap

theorem OAI.Nagata.Workers.W17.partialX_affineSwap line 308

Source documentation

The other derivative coordinate is exchanged at the same actual point.

theorem partialX_affineSwap (G : MvPolynomial (Fin 2) ℂ) (p : ComplexPlane) :
    planePolynomialEval (MvPolynomial.pderiv 0 (affineSwap G)) p.swap =
      planePolynomialEval (MvPolynomial.pderiv 1 G) p := by
…

Mentions: OAI.Nagata.Workers.W17.affineSwap

theorem OAI.Nagata.Workers.W17.polynomialGradient_affineSwap line 319
Source documentation
The actual normal displacement is unchanged when both variables and velocity coordinates are swapped.
```
theorem polynomialGradient_affineSwap (G : MvPolynomial (Fin 2) ℂ) (p V : ComplexPlane) :
    polynomialGradient (affineSwap G) p.swap V.swap = polynomialGradient G p V := by
…
```
Mentions: OAI.Nagata.Workers.W17.affineSwap
theorem OAI.Nagata.Workers.W17.swap_affine_motion line 328
Source documentation
Swapping commutes with the actual affine-linear moving point.
```
theorem swap_affine_motion (p V : ComplexPlane) (s : ℂ) :
    (p+s • V).swap = p.swap+s • V.swap := rfl
…
```