Order one at a point

A germ s ∈ 𝒪_{M,a} has order one (ordElem, the order read on the Taylor series) iff its value s(a) vanishes and some first partial derivative ∂_i s (a) does not (ord_eq_one_iff_exists_coordDerivStalk_ne_zero'): the degree-0 coefficient of the Taylor series is the value (IsTaylorHom.constantCoeff'), the degree-1 coefficients are the partial derivatives (IsTaylorHom.pderiv: T (∂_i s) = ∂_{X_i} (T s)), and a power series has order one iff its constant term vanishes and some linear term does not (MvPowerSeries.order_eq_one_iff', from MvPowerSeries.order_eq_nat). This is the criterion behind Kollár's "local section of MC(I) that has order 1 at x" [Kol07, Theorem 80, proof], made chart-free in Hironaka/Manifold/Chart/Adapted.lean.

theorem Manifold.constantCoeff_pderiv {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (i : Fin n) (F : MvPowerSeries (Fin n) 𝕜) : MvPowerSeries.constantCoeff ((MvPowerSeries.pderiv i) F) = (MvPowerSeries.coeff (Finsupp.single i 1)) F

The constant coefficient of ∂_{X_i} F is the coefficient of X_i in F.

theorem Manifold.eval_coordDerivStalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (i : Fin n) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : (eval 𝕜 E M a) ((coordDerivStalk E ψ φ hφ ha i) s) = (MvPowerSeries.coeff (Finsupp.single i 1)) ((taylorHom E ψ φ ha hφ) s)

The value at a of ∂_i s is the coefficient of X_i in the Taylor series of s.

theorem Finsupp.degree_eq_one_iff {σ : Type u_2} (d : σ →₀ ℕ) : degree d = 1 ↔ ∃ (i : σ), d = single i 1

A multi-index of degree one is a single index.

theorem MvPowerSeries.order_eq_one_iff' {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (F : MvPowerSeries (Fin n) 𝕜) : F.order = 1 ↔ constantCoeff F = 0 ∧ ∃ (i : Fin n), (coeff (Finsupp.single i 1)) F ≠ 0

A power series has order one iff its constant term vanishes and some coefficient of degree one does not.

theorem Manifold.ord_eq_one_iff_exists_coordDerivStalk_ne_zero' {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : IsLocalRing.ordElem s = 1 ↔ (eval 𝕜 E M a) s = 0 ∧ ∃ (i : Fin n), (eval 𝕜 E M a) ((coordDerivStalk E ψ φ hφ ha i) s) ≠ 0

In a chart φ at a with coordinates ψ, a germ has order one iff it vanishes at a and some partial derivative ∂_i does not (the order-one sections of [Kol07, Theorem 80, proof]).