The coordinate swap realises the formal equivalence

The formal half of Kollár's uniqueness of maximal contact [Kol07, 95], on the analytic stalk. At p with ord_p I = m ≥ 1, take the charts e = (x₁, y), e' = (x₁', y) of exists_commonCharts (Hironaka/Resolution/Analytic/MaximalContact/CommonCharts.lean: H = {x₁ = 0}, H' = {x₁' = 0}, the components of E through p among the shared coordinates y), the coordinate swap Φ = e'⁻¹ ∘ e (Hironaka/Manifold/Chart/Swap.lean) and its pullback of germs r = Φ^*, with T_e ∘ r = T_{e'} (IsPullbackStalk.taylorHom_eq'). Then:

• r x₁' = x₁ and r y_j = y_j (the Taylor identity and the injectivity of T_e), so r carries the vanishing ideal of H' onto that of H and fixes those of the components of E;
• Kollár's formal automorphism G = T_e ∘ T_{e'}⁻¹ of 𝕜⟦X⟧ (taylorAut) is X_{i₀} ↦ X_{i₀} + T_e(x₁' − x₁), X_j ↦ X_j — of the form 1 + T_e(MC(I)_p) since x₁, x₁' ∈ MC(I)_p (IsOnePlus, through eq_substAlgHom_of_forall_X_mem); by Kollár's Proposition 94 (isInvariantOnePlus_map_taylorHom, Hironaka/Resolution/Analytic/MaximalContact/TaylorTransport.lean) G maps Î = T_e(I_p)𝕜⟦X⟧ into itself, hence onto itself (Ideal.map_eq_of_map_le, Noetherian), and reading T_{e'} = G⁻¹ ∘ T_e gives T_e(r(I_p)) 𝕜⟦X⟧ = T_e(I_p) 𝕜⟦X⟧; through the completion isomorphism 𝒪̂_p ≅ 𝕜⟦X⟧ and Krull's intersection theorem (Ideal.eq_of_map_adicCompletion_eq) this is r(I_p) = I_p;
• s − r s ∈ MC(I)_p for every germ s: on the coordinates of e' the defect is 0 or x₁' − x₁ ∈ MC(I)_p, and the coordinate criterion sub_mem_of_forall_coord_sub_mem extends it.

The result (exists_realizing_swap; coordinateSwapAutomorphism_realizes_formal is the same statement without the last clause) is propagated to a neighbourhood in Hironaka/Resolution/Analytic/MaximalContact/Propagation.lean. The Hironaka library has the same argument for the completed local ring of a scheme (Hironaka/Resolution/Algebraic/MaximalContact/FormalEquivExists.lean).

theorem Hironaka.Manifold.mem_of_idealSheaf_le_iteratedDeriv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) {m : ℕ} (hm : 1 ≤ m) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ H 1) (hHmc : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv I (m - 1)) {p : M.carrier} (hp : Manifold.IdealSheaf.ord I p = ↑m) : p ∈ H

A point of order exactly m ≥ 1 lies on every hypersurface of maximal contact (its ideal sheaf is contained in MC(I), whose stalk at p is proper).

noncomputable def Hironaka.Manifold.taylorAut {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (e e' : OpenPartialHomeomorph M.carrier E) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) {p : M.carrier} (hpe : p ∈ e.source) (hpe' : p ∈ e'.source) : MvPowerSeries (Fin n) 𝕜 ≃+* MvPowerSeries (Fin n) 𝕜

Kollár's formal automorphism φ^* = T_e ∘ T_{e'}⁻¹ of 𝒪̂_p ≅ 𝕜⟦X⟧ [Kol07, 95], explicitly: the composite of the two completion isomorphisms (exists_taylor_automorphism' of Hironaka/Manifold/Chart/Swap.lean, made a definition so that its action on the whole completion is available).

Equations

• Hironaka.Manifold.taylorAut ψ e e' he he' hpe hpe' = (Manifold.taylorCompletionEquiv E ψ e' hpe' he').symm.trans (Manifold.taylorCompletionEquiv E ψ e hpe he)

theorem Hironaka.Manifold.taylorAut_apply_taylorHom {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {e e' : OpenPartialHomeomorph M.carrier E} {he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier} {he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier} {p : M.carrier} {hpe : p ∈ e.source} {hpe' : p ∈ e'.source} (s : ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.stalk p)) : (taylorAut ψ e e' he he' hpe hpe') ((Manifold.taylorHom E ψ e' hpe' he') s) = (Manifold.taylorHom E ψ e hpe he) s

The formal automorphism carries the e'-expansion of every germ to its e-expansion.

theorem Hironaka.Manifold.taylorAut_apply_taylorCompletionEquiv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {e e' : OpenPartialHomeomorph M.carrier E} {he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier} {he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier} {p : M.carrier} {hpe : p ∈ e.source} {hpe' : p ∈ e'.source} (h : AdicCompletion (IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.stalk p)) ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.stalk p)) : (taylorAut ψ e e' he he' hpe hpe') ((Manifold.taylorCompletionEquiv E ψ e' hpe' he') h) = (Manifold.taylorCompletionEquiv E ψ e hpe he) h

The formal automorphism on the whole completion: φ^* ∘ T̂_{e'} = T̂_e.

theorem Hironaka.Manifold.exists_realizing_swap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) {m : ℕ} (hm : 1 ≤ m) (hI : Manifold.IdealSheaf.iteratedDeriv I (m - 1) * Manifold.IdealSheaf.deriv I ≤ I) {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) {H H' : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ H 1) (hH' : Manifold.IsClosedSubmanifold ψ H' 1) (hHmc : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv I (m - 1)) (hH'mc : hH'.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv I (m - 1)) (hHF : Manifold.HypersurfaceFamily.IsSnc ψ (F.append H)) (hH'F : Manifold.HypersurfaceFamily.IsSnc ψ (F.append H')) (p : M.carrier) (hp : Manifold.IdealSheaf.ord I p = ↑m) : ∃ (e : OpenPartialHomeomorph M.carrier E) (e' : OpenPartialHomeomorph M.carrier E) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) (hpe : p ∈ e.source) (hpe' : p ∈ e'.source) (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M.carrier M.carrier ⊤) (r : AnalyticManifold.IdealSheaf.stalkRing M p →+* AnalyticManifold.IdealSheaf.stalkRing M p), ↑e p = 0 ∧ ↑e' p = 0 ∧ Manifold.IsCoordinateSwap E M.carrier e e' p Φ ∧ Manifold.IsPullbackStalk E M.carrier (↑Φ.toPartialEquiv) r ∧ (∀ (s : AnalyticManifold.IdealSheaf.stalkRing M p), (Manifold.taylorHom E ψ e hpe he) (r s) = (Manifold.taylorHom E ψ e' hpe' he') s) ∧ Ideal.map r (Manifold.vanishingStalk H' p) = Manifold.vanishingStalk H p ∧ Ideal.map r (Manifold.IdealSheaf.stalkIdeal I p) = Manifold.IdealSheaf.stalkIdeal I p ∧ (∀ (j : F.ι), Ideal.map r (Manifold.vanishingStalk (F.hyp j) p) = Manifold.vanishingStalk (F.hyp j) p) ∧ (∀ (s : AnalyticManifold.IdealSheaf.stalkRing M p), s - r s ∈ (Manifold.IdealSheaf.iteratedDeriv I (m - 1)).stalkIdeal p) ∧ ∀ (G : MvPowerSeries (Fin n) 𝕜), (taylorAut ψ e e' he he' hpe hpe') G - G ∈ Ideal.map (Manifold.taylorHom E ψ e hpe he) ((Manifold.IdealSheaf.iteratedDeriv I (m - 1)).stalkIdeal p)

The coordinate swap realises the formal equivalence [Kol07, 95], the working form, with Kollár's formal automorphism T_e ∘ T_{e'}⁻¹ written as 1 + T_e(MC(I)_p) on the whole of 𝕜⟦X⟧. For I MC-invariant, p of order exactly m ≥ 1, and hypersurfaces of maximal contact H, H' with E + H, E + H' snc, there are centred charts e, e' at p, the coordinate swap Φ = e'⁻¹ ∘ e and its pullback of germs r with T_e ∘ r = T_{e'}, such that r carries the vanishing ideal of H' onto that of H, fixes I_p and the vanishing ideals of the components of E, and moves every germ by an element of MC(I)_p.

theorem Hironaka.Manifold.coordinateSwapAutomorphism_realizes_formal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) {m : ℕ} (hm : 1 ≤ m) (hI : Manifold.IdealSheaf.iteratedDeriv I (m - 1) * Manifold.IdealSheaf.deriv I ≤ I) {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) {H H' : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ H 1) (hH' : Manifold.IsClosedSubmanifold ψ H' 1) (hHmc : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv I (m - 1)) (hH'mc : hH'.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv I (m - 1)) (hHF : Manifold.HypersurfaceFamily.IsSnc ψ (F.append H)) (hH'F : Manifold.HypersurfaceFamily.IsSnc ψ (F.append H')) (p : M.carrier) (hp : Manifold.IdealSheaf.ord I p = ↑m) : ∃ (e : OpenPartialHomeomorph M.carrier E) (e' : OpenPartialHomeomorph M.carrier E) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) (hpe : p ∈ e.source) (hpe' : p ∈ e'.source) (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M.carrier M.carrier ⊤) (r : AnalyticManifold.IdealSheaf.stalkRing M p →+* AnalyticManifold.IdealSheaf.stalkRing M p), ↑e p = 0 ∧ ↑e' p = 0 ∧ Manifold.IsCoordinateSwap E M.carrier e e' p Φ ∧ Manifold.IsPullbackStalk E M.carrier (↑Φ.toPartialEquiv) r ∧ (∀ (s : AnalyticManifold.IdealSheaf.stalkRing M p), (Manifold.taylorHom E ψ e hpe he) (r s) = (Manifold.taylorHom E ψ e' hpe' he') s) ∧ Ideal.map r (Manifold.vanishingStalk H' p) = Manifold.vanishingStalk H p ∧ Ideal.map r (Manifold.IdealSheaf.stalkIdeal I p) = Manifold.IdealSheaf.stalkIdeal I p ∧ (∀ (j : F.ι), Ideal.map r (Manifold.vanishingStalk (F.hyp j) p) = Manifold.vanishingStalk (F.hyp j) p) ∧ ∀ (s : AnalyticManifold.IdealSheaf.stalkRing M p), s - r s ∈ (Manifold.IdealSheaf.iteratedDeriv I (m - 1)).stalkIdeal p

The coordinate swap realises the formal equivalence [Kol07, 95]: exists_realizing_swap without its last clause.