The chain rule for germs along an analytic map

Kollár computes the derivatives of the transform of an ideal "using the chain rule" [Kol07, 75]. On the stalks this is the following identity: for an analytic map f : M' → M, a chart φ of M at f b with coordinates x_k and any 𝕜-derivation δ of 𝒪_{M', b}, δ(s ∘ f) = ∑_k δ((x_k − x_k(f b)) ∘ f) · (∂_k s) ∘ f for every germ s at f b (derivation_germMap_eq_sum_coordDerivStalk; s ∘ f is the germ map germMap).

The proof is the Taylor-uniqueness argument of derivation_eq_sum_coordDerivStalk (Hironaka/Manifold/Germ/CoordDerivCoords.lean) rerun for the "derivation along f" F(s) := δ(s ∘ f) − ∑_k δ(x_k ∘ f) · (∂_k s) ∘ f: F is additive, satisfies the Leibniz rule F(st) = (s ∘ f) F(t) + (t ∘ f) F(s), kills the constants and the centred coordinates, hence every polynomial in the coordinates; and F lowers the order by one (F(𝔪_{f b}^{k+1}) ⊆ 𝔪_b^k, because the germ map is a local homomorphism and derivations lower the order). Every germ is a polynomial in the coordinates up to 𝔪^{k+1}, so F(s) ∈ ⋂_k 𝔪_b^k = 0. Not in the sources as a separate statement. It is used to transport derivations along germ maps (Hironaka/Resolution/Analytic/MaximalContact/StalkEquiv.lean) and to compute derivative ideals in the charts of a blow-up (Hironaka/Manifold/BlowUp/Transform/DerivChart.lean).

theorem Manifold.germMap_algebraMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] (f : M' → M) (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) (b : M') (a : 𝕜) : (germMap f hf b) ((algebraMap 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.stalk (f b))) a) = (algebraMap 𝕜 ↑((structureSheaf 𝕜 E M').presheaf.stalk b)) a

The germ map of an analytic map is a 𝕜-algebra map: constants pull back to constants.

theorem Manifold.germMap_mem_maximalIdeal_pow {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] (f : M' → M) (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) {b : M'} {s : ↑((structureSheaf 𝕜 E M).presheaf.stalk (f b))} {k : ℕ} (hs : s ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk (f b)) ^ k) : (germMap f hf b) s ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M').presheaf.stalk b) ^ k

The germ map is a local homomorphism, so it carries 𝔪_{f b}^k into 𝔪_b^k.

theorem Manifold.derivation_germMap_eq_sum_coordDerivStalk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] (f : M' → M) (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {b : M'} (hb : f b ∈ φ.source) (δ : Derivation 𝕜 ↑((structureSheaf 𝕜 E M').presheaf.stalk b) ↑((structureSheaf 𝕜 E M').presheaf.stalk b)) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk (f b))) : δ ((germMap f hf b) s) = ∑ k : Fin n, δ ((germMap f hf b) (centredCoord E ψ φ hφ hb k)) * (germMap f hf b) ((coordDerivStalk E ψ φ hφ hb k) s)

The chain rule for germs along an analytic map f : M' → M (the identity behind Kollár's computation "using the chain rule" [Kol07, 75]; the Taylor-uniqueness argument of derivation_eq_sum_coordDerivStalk for a derivation along the germ map). For a chart φ at f b with coordinates x_k, every 𝕜-derivation δ of 𝒪_{M', b} satisfies, on the germs s ∘ f, δ(s ∘ f) = ∑_k δ((x_k − x_k(f b)) ∘ f) · (∂_k s) ∘ f.