Kollár's Proposition 94 for the analytic stalk, through the Taylor homomorphism

Kollár applies his Proposition 94 to the completed ideal Î ⊆ 𝒪̂_p ≅ 𝕜⟦X⟧ of an MC-invariant I [Kol07, 95]. The analytic bridge is the Taylor homomorphism T_e : 𝒪_{M,p} → 𝕜⟦X⟧ of a chart e at p (Hironaka/Manifold/Germ/TaylorHom.lean), which is injective and carries the coordinate derivations to the formal partial derivatives (IsTaylorHom.pderiv):

• D_map_taylorHom, Dpow_map_taylorHom, MC_map_taylorHom: the derivative ideals of the Hironaka library's regular coordinates (IsLocalRing.RegularCoords) transport along T_e, T_e(D(J)) 𝕜⟦X⟧ = D(T_e(J) 𝕜⟦X⟧) (RegularCoords.D_map for the regular coordinates of the stalk and of 𝕜⟦X⟧);
• isMCInvariant_map_taylorHom: MC-invariance of I (the sheaf inequality MC(I) · D(I) ≤ I) gives MC-invariance of Î := T_e(I_p) 𝕜⟦X⟧ in the standard coordinates;
• map_taylorHom_MC_le_maximalIdeal: at a point of order exactly m ≥ 1, T_e(MC(I)_p) ⊆ (X);
• isInvariantOnePlus_map_taylorHom: hence, by Proposition 94 (isMCInvariant_iff_isInvariantOnePlus of Hironaka/Algebra/Local/Prop94.lean), Î is invariant under every automorphism of 𝕜⟦X⟧ of the form 1 + T_e(MC(I)_p) [Kol07, Proposition 94].

This is the input of the coordinate swap's action on I_p (Hironaka/Resolution/Analytic/MaximalContact/SwapRealizes.lean).

Transport of the derivative ideals along the Taylor homomorphism

theorem Hironaka.Manifold.dim_stalk_eq {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] {a : M} : ↑n = ringKrullDim ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)

The dimension of the stalk is n.

theorem Hironaka.Manifold.D_map_taylorHom {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (c : IsLocalRing.RegularCoords (↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)) n) (hcp : ∀ (i : Fin n), c.pderiv i = Derivation.restrictScalars ℚ (Manifold.coordDerivStalk E ψ φ hφ ha i)) (J : Ideal ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)) : (IsLocalRing.RegularCoords.stdMvPowerSeries 𝕜 n).D (Ideal.map (Manifold.taylorHom E ψ φ ha hφ) J) = Ideal.map (Manifold.taylorHom E ψ φ ha hφ) (c.D J)

The transport of the derivative ideal along the Taylor homomorphism (RegularCoords.D_map; T_e carries the coordinate derivations of the stalk to the formal partial derivatives): D(T_e(J)) = T_e(D(J)) for the regular coordinates c of the stalk in the chart e and the standard coordinates of 𝕜⟦X⟧.

theorem Hironaka.Manifold.Dpow_map_taylorHom {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (c : IsLocalRing.RegularCoords (↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)) n) (hcp : ∀ (i : Fin n), c.pderiv i = Derivation.restrictScalars ℚ (Manifold.coordDerivStalk E ψ φ hφ ha i)) (r : ℕ) (J : Ideal ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)) : (IsLocalRing.RegularCoords.stdMvPowerSeries 𝕜 n).Dpow r (Ideal.map (Manifold.taylorHom E ψ φ ha hφ) J) = Ideal.map (Manifold.taylorHom E ψ φ ha hφ) (c.Dpow r J)

The iterated derivative ideals transport along the Taylor homomorphism.

theorem Hironaka.Manifold.MC_map_taylorHom {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (c : IsLocalRing.RegularCoords (↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)) n) (hcp : ∀ (i : Fin n), c.pderiv i = Derivation.restrictScalars ℚ (Manifold.coordDerivStalk E ψ φ hφ ha i)) (m : ℕ) (J : Ideal ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)) : (IsLocalRing.RegularCoords.stdMvPowerSeries 𝕜 n).MC (Ideal.map (Manifold.taylorHom E ψ φ ha hφ) J) m = Ideal.map (Manifold.taylorHom E ψ φ ha hφ) (c.MC J m)

The maximal contact ideal transports along the Taylor homomorphism.

MC-invariance of the Taylor image and Proposition 94

theorem Hironaka.Manifold.isMCInvariant_map_taylorHom {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] (I : M.IdealSheaf) {m : ℕ} (e : OpenPartialHomeomorph M.carrier E) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) {p : M.carrier} (hpe : p ∈ e.source) (hI : Manifold.IdealSheaf.iteratedDeriv I (m - 1) * Manifold.IdealSheaf.deriv I ≤ I) : (IsLocalRing.RegularCoords.stdMvPowerSeries 𝕜 n).IsMCInvariant (Ideal.map (Manifold.taylorHom E ψ e hpe he) (Manifold.IdealSheaf.stalkIdeal I p)) m

The MC-invariance MC(I) · D(I) ≤ I of the ideal sheaf gives, at p, the MC-invariance of Î = T_e(I_p) 𝕜⟦X⟧ in the standard coordinates (Kollár's MC(I) and MC(Î), [Kol07, 95]).

theorem Hironaka.Manifold.map_taylorHom_MC_le_maximalIdeal {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] (I : M.IdealSheaf) {m : ℕ} (e : OpenPartialHomeomorph M.carrier E) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) {p : M.carrier} (hpe : p ∈ e.source) (hm : 1 ≤ m) (hp : Manifold.IdealSheaf.ord I p = ↑m) : Ideal.map (Manifold.taylorHom E ψ e hpe he) ((Manifold.IdealSheaf.iteratedDeriv I (m - 1)).stalkIdeal p) ≤ IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) 𝕜)

At a point of order exactly m ≥ 1, the Taylor image of MC(I)_p lies in the maximal ideal (X) of 𝕜⟦X⟧ (MC(I) has order 1 there, ord_iteratedDeriv_eq_one).

theorem Hironaka.Manifold.isInvariantOnePlus_map_taylorHom {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] (I : M.IdealSheaf) {m : ℕ} (e : OpenPartialHomeomorph M.carrier E) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) {p : M.carrier} (hpe : p ∈ e.source) (hm : 1 ≤ m) (hI : Manifold.IdealSheaf.iteratedDeriv I (m - 1) * Manifold.IdealSheaf.deriv I ≤ I) (hp : Manifold.IdealSheaf.ord I p = ↑m) : IsLocalRing.IsInvariantOnePlus (Ideal.map (Manifold.taylorHom E ψ e hpe he) (Manifold.IdealSheaf.stalkIdeal I p)) (Ideal.map (Manifold.taylorHom E ψ e hpe he) ((Manifold.IdealSheaf.iteratedDeriv I (m - 1)).stalkIdeal p))

Kollár's Proposition 94 applied ([Kol07, Proposition 94]; [Kol07, 95]): for I MC-invariant and p of order exactly m ≥ 1, the ideal Î = T_e(I_p) 𝕜⟦X⟧ is invariant under every automorphism of 𝕜⟦X⟧ of the form 1 + T_e(MC(I)_p).