Tools for the propagation step

Kollár's propagation step ("(91.1′–4′) also hold in an open neighbourhood U(p) of p", [Kol07, 95]) moves stalk-level facts at one point to a neighbourhood (Hironaka/Resolution/Analytic/MaximalContact/Propagation.lean). This module holds the general tools it uses:

• IdealSheaf.eventually_germ_mem_stalkIdeal: a section whose germ at a lies in the stalk ideal J_a has its germs in J at every point near a — the witness g' ∈ J(V) with g'_a = g_a agrees with g on a neighbourhood, on which J is a sheaf of ideals;
• germMap_germ_eq_germMap_germ_of_eventuallyEq: the pull-backs along two maps f, g of the germs of two sections agree when the composites s₁ ∘ f, s₂ ∘ g agree near the point;
• map_stalkCast_stalkIdeal: transport of a stalk ideal along an equality of points;
• contMDiffOn_subtypeVal_comp_iff: analyticity of a map into an open subset is analyticity of its composite with the inclusion (Mathlib's ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff, at C^ω);
• PartialDiffeomorph.isLocalDiffeomorph_comp_subtype_val: a partial analytic isomorphism Φ composed with the inclusion of an open U ⊆ Φ.source, as a map out of the open submanifold U, is a local analytic isomorphism — Kollár's Φ : U(p) → M.

theorem Manifold.IdealSheaf.eventually_germ_mem_stalkIdeal {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) {W : TopologicalSpace.Opens ↑X} {a : ↑X} (ha : a ∈ W) (g : ↑(𝒪.presheaf.obj (Opposite.op W))) (h : (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ W a ha)) g ∈ J.stalkIdeal a) : ∀ᶠ (b : ↑X) in nhds a, ∀ (hb : b ∈ W), (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ W b hb)) g ∈ J.stalkIdeal b

A germ in the stalk ideal at a stays in the stalk ideals nearby: if the germ at a of a section g lies in J_a, the germs of g at all points near a lie in J (the witness g' ∈ J(V) with g'_a = g_a agrees with g on a neighbourhood).

theorem Hironaka.Manifold.germMap_germ_eq_germMap_germ_of_eventuallyEq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U M : AnalyticManifold 𝕜 E} (f g : AnalyticMap U M) (u : U.carrier) {W₁ W₂ : TopologicalSpace.Opens M.carrier} (h₁ : f u ∈ W₁) (h₂ : g u ∈ W₂) (s₁ : ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.obj (Opposite.op W₁))) (s₂ : ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.obj (Opposite.op W₂))) (hev : ∀ᶠ (x : U.carrier) in nhds u, Manifold.extendSection 𝕜 E s₁ (f x) = Manifold.extendSection 𝕜 E s₂ (g x)) : (Manifold.germMap ⇑f ⋯ u) ((CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.germ W₁ (f u) h₁)) s₁) = (Manifold.germMap ⇑g ⋯ u) ((CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.germ W₂ (g u) h₂)) s₂)

Two pull-backs of germs of sections agree when the composites agree near the point.

theorem Hironaka.Manifold.map_stalkCast_stalkIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) {x y : M.carrier} (h : x = y) : Ideal.map (stalkCast h) (Manifold.IdealSheaf.stalkIdeal J x) = Manifold.IdealSheaf.stalkIdeal J y

Transport of a stalk ideal along an equality of points.

theorem Hironaka.Manifold.contMDiffOn_subtypeVal_comp_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] {U : TopologicalSpace.Opens N} (f : M → ↥U) (s : Set M) : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (Subtype.val ∘ f) s ↔ ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f s

Analyticity of a map into an open subset U is analyticity of its composite with the inclusion (Mathlib's ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff at C^ω).

theorem Hironaka.Manifold.PartialDiffeomorph.isLocalDiffeomorph_comp_subtype_val {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M N ⊤) (U : TopologicalSpace.Opens M) (hU : ↑U ⊆ Φ.source) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ fun (x : ↥U) => ↑Φ.toPartialEquiv ↑x

Kollár's Φ : U(p) → M [Kol07, 95]: a partial analytic isomorphism Φ composed with the inclusion of an open U ⊆ Φ.source, as a map out of the open submanifold U, is a local analytic isomorphism — its inverse Φ⁻¹ : Φ(U) → U is analytic into the open subset.