OAI/AlgebraicGeometry/PlaneCurves/NormalSpecialization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Homogeneous normal specialization for lines and smooth curves

  1. theorem OAI.Nagata.Workers.W28.polynomialGradient_ne_zero_of_partial line 16

    Source documentation

    A nonzero actual normal partial makes the actual polynomial differential nonzero.

    theorem polynomialGradient_ne_zero_of_partial
    (G : MvPolynomial (Fin 2) ℂ) (p : ComplexPlane)
    (hpartial : planePolynomialEval (MvPolynomial.pderiv 1 G) p ≠ 0) :
    polynomialGradient G p ≠ 0 := by
…

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

  2. theorem OAI.Nagata.Workers.W28.exists_normal_specialization_from_partial line 27

    Source documentation

    Local normal specialization with its analytic chart and actual derivative constructed from the polynomial and a nonzero actual normal partial.

    theorem exists_normal_specialization_from_partial
    (I : Finset ℕ) (j : ℕ → ℕ) (R : ℕ → MvPolynomial (Fin 2) ℂ)
    (u : ℕ) (hmin : ∀ α ∈ I, u ≤ α + j α)
    (G : MvPolynomial (Fin 2) ℂ) (p V : ComplexPlane)
    (hp : planePolynomialEval G p = 0)
    (hpartial : planePolynomialEval (MvPolynomial.pderiv 1 G) p ≠ 0)
    (exceptional : Finset ℂ) (m : ℕ)
    (horders : ∀ᶠ s : ℂ in 𝓝 0, s ∉ exceptional →
      Nagata.AffineMultiplicity.orderAtLeast
        (fun i : Fin 2 => if i = 0 then (p + s • V).1 else (p + s • V).2)
        m (factoredPlaneFamily I j R G s)) :
    ∃ e : OpenPartialHomeomorph ComplexPlane ComplexPlane,
…

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

  3. theorem OAI.Nagata.Workers.W28.line_normal_specialization line 68

    Source documentation

    Actual ordinary multiplicities of a finite plane polynomial family along an affine motion specialize to actual ideal-power multiplicity of the literal line-restricted initial normal polynomial. The chart and analytic limit are constructed in the proof from the nonzero actual normal partial.

    theorem line_normal_specialization
    (I : Finset ℕ) (j : ℕ → ℕ) (T : ℕ → MvPolynomial (Fin 3) ℂ)
    (u : ℕ) (hmin : ∀ α ∈ I, u ≤ α + j α)
    (G : MvPolynomial (Fin 3) ℂ) (i ξ : ℂ) (V : ComplexPlane)
    (hline : Nagata.W04.ReducibleSquare.lineRestriction i G = 0)
    (hpartial : planePolynomialEval
      (MvPolynomial.pderiv 1 (Nagata.W27.directChartHom (2 : Fin 3) G))
      (ξ, i ^ 2 - i * ξ) ≠ 0)
    (exceptional : Finset ℂ) (m : ℕ)
    (horders : ∀ᶠ s : ℂ in 𝓝 0, s ∉ exceptional →
      Nagata.AffineMultiplicity.orderAtLeast
        (fun a : Fin 2 => if a = 0 then ((ξ, i ^ 2 - i * ξ) + s • V).1
…

    Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.W04.ReducibleSquare.lineRestriction, OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.W27.directChartHom

  4. theorem OAI.Nagata.Workers.W28.homogeneous_normal_specialization line 121

    Source documentation

    Actual moving plane-curve multiplicities imply actual homogeneous normal polynomial order along an analytic parametrized homogeneous curve. Every local normal chart, derivative, zero-parameter limit, and variable frame factor is constructed by the checked bridge chain.

    theorem homogeneous_normal_specialization
    (I : Finset ℕ) (j : ℕ → ℕ) (T : ℕ → MvPolynomial (Fin 3) ℂ)
    (u : ℕ) (hmin : ∀ α ∈ I, u ≤ α + j α)
    (d k : ℕ) (hhom : ∀ α ∈ I, (T α).IsHomogeneous (d-k*j α))
    (hbound : ∀ α ∈ I, k*j α ≤ d)
    (G : MvPolynomial (Fin 3) ℂ) (hG : G.IsHomogeneous k)
    (X : Fin 3 → ℂ → ℂ) (c : Fin 3) (z₀ w₀ : ℂ)
    (hX : ∀ a, AnalyticAt ℂ (X a) z₀) (hc : X c z₀ ≠ 0)
    (hzero : ∀ᶠ z in 𝓝 z₀, MvPolynomial.eval (fun a => X a z) G = 0)
    (hpartial : planePolynomialEval (MvPolynomial.pderiv 1 (Nagata.W27.directChartHom c G))
      (normalizedCurvePoint X c z₀) ≠ 0)
    (V : ComplexPlane)
…

    Mentions: OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.W27.directChartHom, OAI.Nagata.Workers.W28.normalizedCurvePoint, OAI.Nagata.Workers.W28.ComplexPlane

  5. theorem OAI.Nagata.Workers.W28.homogeneous_normal_specialization_of_partialX line 184

    Source documentation

    The same actual homogeneous family and normal displacement specialize when only the first affine partial is known nonzero. The proof swaps actual polynomials, points and velocities, and restores the original frame expression.

    theorem homogeneous_normal_specialization_of_partialX
    (I : Finset ℕ) (j : ℕ → ℕ) (T : ℕ → MvPolynomial (Fin 3) ℂ)
    (u : ℕ) (hmin : ∀ α ∈ I, u ≤ α + j α)
    (d k : ℕ) (hhom : ∀ α ∈ I, (T α).IsHomogeneous (d-k*j α))
    (hbound : ∀ α ∈ I, k*j α ≤ d)
    (G : MvPolynomial (Fin 3) ℂ) (hG : G.IsHomogeneous k)
    (X : Fin 3 → ℂ → ℂ) (c : Fin 3) (z₀ w₀ : ℂ)
    (hX : ∀ a, AnalyticAt ℂ (X a) z₀) (hc : X c z₀ ≠ 0)
    (hzero : ∀ᶠ z in 𝓝 z₀, MvPolynomial.eval (fun a => X a z) G = 0)
    (hpartial : planePolynomialEval (MvPolynomial.pderiv 0 (Nagata.W27.directChartHom c G))
      (normalizedCurvePoint X c z₀) ≠ 0)
    (V : ComplexPlane)
…

    Mentions: OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.W27.directChartHom, OAI.Nagata.Workers.W28.normalizedCurvePoint, OAI.Nagata.Workers.W28.ComplexPlane

  6. theorem OAI.Nagata.Workers.W28.polynomialGradient_ne_zero_iff_partials line 266

    Source documentation

    The actual polynomial differential is nonzero exactly when at least one of its two actual coordinate partials is nonzero.

    theorem polynomialGradient_ne_zero_iff_partials
    (G : MvPolynomial (Fin 2) ℂ) (p : ComplexPlane) :
    polynomialGradient G p ≠ 0 ↔
      planePolynomialEval (MvPolynomial.pderiv 0 G) p ≠ 0 ∨
      planePolynomialEval (MvPolynomial.pderiv 1 G) p ≠ 0 := by
…

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

  7. theorem OAI.Nagata.Workers.W28.homogeneous_normal_specialization_of_gradient line 291

    Source documentation

    Both genuine smooth affine directions lead to the same actual normal polynomial, same original moving family and same homogeneous frame scaling.

    theorem homogeneous_normal_specialization_of_gradient
    (I : Finset ℕ) (j : ℕ → ℕ) (T : ℕ → MvPolynomial (Fin 3) ℂ)
    (u : ℕ) (hmin : ∀ α ∈ I, u ≤ α + j α)
    (d k : ℕ) (hhom : ∀ α ∈ I, (T α).IsHomogeneous (d-k*j α))
    (hbound : ∀ α ∈ I, k*j α ≤ d)
    (G : MvPolynomial (Fin 3) ℂ) (hG : G.IsHomogeneous k)
    (X : Fin 3 → ℂ → ℂ) (c : Fin 3) (z₀ w₀ : ℂ)
    (hX : ∀ a, AnalyticAt ℂ (X a) z₀) (hc : X c z₀ ≠ 0)
    (hzero : ∀ᶠ z in 𝓝 z₀, MvPolynomial.eval (fun a => X a z) G = 0)
    (hgradient : planePolynomialEval (MvPolynomial.pderiv 0 (Nagata.W27.directChartHom c G))
      (normalizedCurvePoint X c z₀) ≠ 0 ∨
      planePolynomialEval (MvPolynomial.pderiv 1 (Nagata.W27.directChartHom c G))
…

    Mentions: OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.W27.directChartHom, OAI.Nagata.Workers.W28.normalizedCurvePoint

  8. theorem OAI.Nagata.Workers.W28.homogeneous_normal_specialization_of_nonzero_differential line 325

    Source documentation

    The source smoothness input is the actual nonzero polynomial differential, with no fixed partial direction or analytic normal chart supplied as a hypothesis.

    theorem homogeneous_normal_specialization_of_nonzero_differential
    (I : Finset ℕ) (j : ℕ → ℕ) (T : ℕ → MvPolynomial (Fin 3) ℂ)
    (u : ℕ) (hmin : ∀ α ∈ I, u ≤ α + j α)
    (d k : ℕ) (hhom : ∀ α ∈ I, (T α).IsHomogeneous (d-k*j α))
    (hbound : ∀ α ∈ I, k*j α ≤ d)
    (G : MvPolynomial (Fin 3) ℂ) (hG : G.IsHomogeneous k)
    (X : Fin 3 → ℂ → ℂ) (c : Fin 3) (z₀ w₀ : ℂ)
    (hX : ∀ a, AnalyticAt ℂ (X a) z₀) (hc : X c z₀ ≠ 0)
    (hzero : ∀ᶠ z in 𝓝 z₀, MvPolynomial.eval (fun a => X a z) G = 0)
    (hdifferential : polynomialGradient (Nagata.W27.directChartHom c G)
      (normalizedCurvePoint X c z₀) ≠ 0)
    (V : ComplexPlane)
…

    Mentions: OAI.Nagata.Workers.W28.polynomialGradient, OAI.Nagata.W27.directChartHom, OAI.Nagata.Workers.W28.normalizedCurvePoint, OAI.Nagata.Workers.W28.ComplexPlane