Formal branches of plane equations at nonsingular points, in either coordinate chart. The other coordinate is the parameter X plus its base value.

noncomputable def CCDN.formalPlanePolynomial {K : Type u_1} [CommRing K] (j : Fin 2) (a : K) : MvPolynomial (Fin 2) K →+* Polynomial (PowerSeries K)

Turn coordinate j into a polynomial variable and the other coordinate into the formal parameter X+a.

Equations

• CCDN.formalPlanePolynomial j a = MvPolynomial.eval₂Hom (Polynomial.C.comp PowerSeries.C) fun (k : Fin 2) => if k = j then Polynomial.X else Polynomial.C (PowerSeries.X + PowerSeries.C a)

@[simp]

theorem CCDN.formalPlanePolynomial_X {K : Type u_1} [CommRing K] (j k : Fin 2) (a : K) : (formalPlanePolynomial j a) (MvPolynomial.X k) = if k = j then Polynomial.X else Polynomial.C (PowerSeries.X + PowerSeries.C a)

formalPlanePolynomial j a sends variable j to the polynomial variable and the other variable to the constant polynomial with value the power series X + a.

theorem CCDN.plane_coordinate_cases {K : Type u_1} (z : Fin 2 → K) (j : Fin 2) : (fun (k : Fin 2) => if k = j then z j else z j.rev) = z

A point of the plane is recovered from its coordinate j and its other coordinate j.rev.

theorem CCDN.exists_unique_formal_plane_branch {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (z : Fin 2 → K) (j : Fin 2) (hz : (MvPolynomial.eval z) f = 0) (hj : (MvPolynomial.eval z) ((MvPolynomial.pderiv j) f) ≠ 0) : ∃! g : PowerSeries K, PowerSeries.constantCoeff g = z j ∧ MvPolynomial.eval₂ PowerSeries.C (fun (k : Fin 2) => if k = j then g else PowerSeries.X + PowerSeries.C (z j.rev)) f = 0

A nonzero chosen partial derivative supplies a unique formal branch through the given point. This works in arbitrary characteristic.