OAI/AlgebraicGeometry/PlaneCurves/ChartGradients.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Nagata.Workers.W25.pderiv_directChartHom line 17

   Source documentation

   The affine partial derivative is the dehomogenized surviving ambient partial.

   theorem pderiv_directChartHom (c : Fin 3) (G : MvPolynomial (Fin 3) ℂ) (i : Fin 2) :
       MvPolynomial.pderiv i (Nagata.W27.directChartHom c G) =
         Nagata.W27.directChartHom c (MvPolynomial.pderiv (c.succAbove i) G) := by
   …

   Mentions: OAI.Nagata.W27.directChartHom

2. theorem OAI.Nagata.Workers.W25.eval_pderiv_directChartHom_scale line 36

   Source documentation

   Exact derivative scaling between a cone representative and its normalized chart.

   theorem eval_pderiv_directChartHom_scale {G : MvPolynomial (Fin 3) ℂ} {d : ℕ}
       (hG : G.IsHomogeneous d) (c : Fin 3) (x : Fin 3 → ℂ) (hc : x c ≠ 0) (i : Fin 2) :
       MvPolynomial.eval x (MvPolynomial.pderiv (c.succAbove i) G) =
         (x c) ^ (d - 1) * MvPolynomial.eval (fun j => x (c.succAbove j) / x c)
           (MvPolynomial.pderiv i (Nagata.W27.directChartHom c G)) := by
   …

   Mentions: OAI.Nagata.W27.directChartHom

3. theorem OAI.Nagata.Workers.W25.exists_nonzero_pderiv_directChartHom line 53

   Source documentation

   Every projective affine chart containing a nonsingular point has a nonzero ordinary two-coordinate affine gradient. Euler's identity rules out the omitted ambient partial being the only nonzero derivative.

   theorem exists_nonzero_pderiv_directChartHom {G : MvPolynomial (Fin 3) ℂ} {d : ℕ}
       (hG : G.IsHomogeneous d) (c : Fin 3) (x : Fin 3 → ℂ)
       (hc : x c ≠ 0) (hzero : MvPolynomial.eval x G = 0)
       (hgrad : ∃ j : Fin 3, MvPolynomial.eval x (MvPolynomial.pderiv j G) ≠ 0) :
       ∃ i : Fin 2, MvPolynomial.eval (fun j => x (c.succAbove j) / x c)
         (MvPolynomial.pderiv i (Nagata.W27.directChartHom c G)) ≠ 0 := by
   …

   Mentions: OAI.Nagata.W27.directChartHom

4. theorem OAI.Nagata.Workers.W25.planePolynomialEval_normalizedCurvePoint line 95
5. theorem OAI.Nagata.Workers.W25.normalizedCurvePoint_gradient_ne_zero line 105

   Source documentation

   Every containing direct chart satisfies the exact smoothness input to the coordinate-independent normal-polynomial construction.

   theorem normalizedCurvePoint_gradient_ne_zero
       {G : MvPolynomial (Fin 3) ℂ} {d : ℕ} (hG : G.IsHomogeneous d)
       (c : Fin 3) (X : Fin 3 → ℂ → ℂ) (z : ℂ) (hc : X c z ≠ 0)
       (hzero : MvPolynomial.eval (fun j => X j z) G = 0)
       (hgrad : ∃ j : Fin 3, MvPolynomial.eval (fun i => X i z) (MvPolynomial.pderiv j G) ≠ 0) :
       polynomialGradient (Nagata.W27.directChartHom c G) (normalizedCurvePoint X c z) ≠ 0 := by
   …

   Mentions: OAI.Nagata.W27.directChartHom