Tangent differentiation on formal plane branches. Vanishing of successive tangent derivatives implies local multiplicity below the characteristic.

noncomputable def CCDN.planeTangent {K : Type u_1} [CommRing K] (f : MvPolynomial (Fin 2) K) (j : Fin 2) : Derivation K (MvPolynomial (Fin 2) K) (MvPolynomial (Fin 2) K)

The polynomial tangent vector field, with coordinate j as local parameter.

Equations

• CCDN.planeTangent f j = (MvPolynomial.pderiv j.rev) f • MvPolynomial.pderiv j - (MvPolynomial.pderiv j) f • MvPolynomial.pderiv j.rev

theorem CCDN.planeTangent_apply {K : Type u_1} [CommRing K] (f h : MvPolynomial (Fin 2) K) (j : Fin 2) : (planeTangent f j) h = (MvPolynomial.pderiv j.rev) f * (MvPolynomial.pderiv j) h - (MvPolynomial.pderiv j) f * (MvPolynomial.pderiv j.rev) h

The tangent vector field of f with local parameter coordinate j applied to h is ∂_{j.rev} f * ∂_j h - ∂_j f * ∂_{j.rev} h.

theorem CCDN.formal_plane_multiplicity_of_tangent {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (ψ : MvPolynomial (Fin 2) K →ₐ[K] PowerSeries K) (hψ : ψ f = 0) (z : Fin 2 → K) (hconst : ∀ (h : MvPolynomial (Fin 2) K), PowerSeries.constantCoeff (ψ h) = (MvPolynomial.eval z) h) (j : Fin 2) (hparam : ψ (MvPolynomial.X j - MvPolynomial.C (z j)) = PowerSeries.X) (hsmooth : (MvPolynomial.eval z) ((MvPolynomial.pderiv j.rev) f) ≠ 0) (g : MvPolynomial (Fin 2) K) (N : ℕ) (hchar : ∀ (n : ℕ), 0 < n → n < N → ↑n ≠ 0) (hzero : ∀ r < N, (MvPolynomial.eval z) ((⇑(planeTangent f j))^[r] g) = 0) : PowerSeries.X ^ N ∣ ψ g

Polynomial tangent derivatives give local divisibility.