The stalk map of a local analytic isomorphism; derivatives commute with local isomorphisms

For an analytic map h : N → M that is a local analytic isomorphism at b, the stalk map h^* = germMap h b : 𝒪_{M, h b} →+* 𝒪_{N, b} has the stalk map of a local inverse as a two-sided inverse (the argument of IdealSheaf.ord_pullback_of_isLocalDiffeomorphAt) and fixes the constants, so it is a 𝕜-algebra isomorphism germAlgEquiv. Consequently the derivative ideal sheaves commute with the pull-back along a local analytic isomorphism: h^*(D^r J) = D^r(h^*J) (comap_iteratedDeriv) — Kollár's "if f : Y → X is smooth, then D(f^*I) = f^*(D(I))" [Kol07, Lemma 74 (4)], for local analytic isomorphisms; in particular MC(h^*I) = h^*MC(I) for MC = D^{m−1} (comap_iteratedDeriv_pred), the identity behind condition (4′) of [Kol07, Definition 91] and condition (2) of [Kol07, Definition 96], where MC(ψ^*I) appears.

noncomputable def Hironaka.Manifold.germMapInv {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) {b : N.carrier} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑h) b) : ↑((Manifold.structureSheaf 𝕜 E N.carrier).presheaf.stalk b) →+* ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.stalk (h b))

The stalk map of a local inverse of h at b: 𝒪_{N, b} →+* 𝒪_{M, h b}.

Equations

• Hironaka.Manifold.germMapInv h hb = Manifold.germMapOn ⋯.choose.invFun ⋯ ⋯ ⋯

theorem Hironaka.Manifold.germMapInv_comp_germMap {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) {b : N.carrier} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑h) b) : (germMapInv h hb).comp (Manifold.germMap ⇑h ⋯ b) = RingHom.id ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.stalk (h b))

theorem Hironaka.Manifold.germMap_comp_germMapInv {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) {b : N.carrier} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑h) b) : (Manifold.germMap ⇑h ⋯ b).comp (germMapInv h hb) = RingHom.id ↑((Manifold.structureSheaf 𝕜 E N.carrier).presheaf.stalk b)

noncomputable def Hironaka.Manifold.germRingEquiv {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) {b : N.carrier} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑h) b) : ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.stalk (h b)) ≃+* ↑((Manifold.structureSheaf 𝕜 E N.carrier).presheaf.stalk b)

The stalk map of a local analytic isomorphism at b as a ring isomorphism (the inverse is the stalk map of a local inverse of h).

Equations

• Hironaka.Manifold.germRingEquiv h hb = { toFun := ⇑(Manifold.germMap ⇑h ⋯ b), invFun := ⇑(Hironaka.Manifold.germMapInv h hb), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

noncomputable def Hironaka.Manifold.germAlgEquiv {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) {b : N.carrier} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑h) b) : ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.stalk (h b)) ≃ₐ[𝕜] ↑((Manifold.structureSheaf 𝕜 E N.carrier).presheaf.stalk b)

The stalk map of a local analytic isomorphism at b, as a 𝕜-algebra isomorphism 𝒪_{M, h b} ≃ₐ[𝕜] 𝒪_{N, b} (the inverse is the stalk map of a local inverse of h).

Equations

• Hironaka.Manifold.germAlgEquiv h hb = AlgEquiv.ofRingEquiv ⋯

theorem Hironaka.Manifold.germAlgEquiv_apply {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) {b : N.carrier} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑h) b) (s : ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.stalk (h b))) : (germAlgEquiv h hb) s = (Manifold.germMap ⇑h ⋯ b) s

theorem Hironaka.Manifold.stalkIdeal_comap_eq_map_germAlgEquiv {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (J : M.IdealSheaf) (b : N.carrier) : (Manifold.IdealSheaf.pullback ⇑h ⋯ J).stalkIdeal b = Ideal.map (germAlgEquiv h ⋯) (Manifold.IdealSheaf.stalkIdeal J (h b))

The stalk of the pull-back along a local analytic isomorphism, through the algebra isomorphism.

theorem Hironaka.Manifold.comap_iteratedDeriv {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (J : M.IdealSheaf) (r : ℕ) : Manifold.IdealSheaf.pullback ⇑h ⋯ (Manifold.IdealSheaf.iteratedDeriv J r) = (Manifold.IdealSheaf.pullback ⇑h ⋯ J).iteratedDeriv r

Kollár's "if f : Y → X is smooth, then D(f^*I) = f^*(D(I))" [Kol07, Lemma 74 (4)] for local analytic isomorphisms: h^*(D^r J) = D^r(h^*J).

theorem Hironaka.Manifold.comap_iteratedDeriv_pred {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (I : M.IdealSheaf) (m : ℕ) : (Manifold.IdealSheaf.pullback ⇑h ⋯ I).iteratedDeriv (m - 1) = Manifold.IdealSheaf.pullback ⇑h ⋯ (Manifold.IdealSheaf.iteratedDeriv I (m - 1))

MC(h^*I) = h^*MC(I) for a local analytic isomorphism h.