Stalk isomorphisms along an open inclusion and along a local isomorphism

The birational transform of a marked ideal commutes with restriction to open subsets and with local isomorphisms [Kol07, Definition 30, 30.1]. The content of that statement, on the analytic side, is the pair of stalk isomorphisms provided here, together with the transport of colon ideals along them:

• the stalk map germMap Subtype.val of the inclusion of an open subset U ⊆ M is bijective: injective because the inclusion maps the neighbourhood filter of a point of U onto its neighbourhood filter in M (map_nhds_subtype_val, IsOpen.nhdsWithin_eq), surjective because a germ on U has an analytic representative near the point which, extended by 0, is analytic on M (analyticity on U is analyticity on M at points of U: Mathlib's liftPropAt_iff_comp_subtype_val);
• the stalk map germMapOn g of a partial analytic diffeomorphism g at a point of its source is bijective: injective because g maps neighbourhood filters onto neighbourhood filters (OpenPartialHomeomorph.map_nhds_eq), surjective because a representative composed with g⁻¹ is a representative at g x (eventually_left_inverse);
• under a ring isomorphism the colon (I : J^m) goes to (e(I) : e(J)^m);
• stalk maps compose and depend only on the map near the point; pullbacks of ideal sheaves compose.

Everything is read through the characterization stalkToGerm_germMapOn of the stalk map as composition of germs of functions. The transport of the birational transform along an open inclusion is Hironaka.Manifold.BlowUp.Transform.OpenSubset. The arguments are routine and not in the sources.

theorem Ideal.map_colon_pow_equiv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (e : R ≃+* S) (I J : Ideal R) (m : ℕ) : map (↑e) (Submodule.colon I ↑(J ^ m)) = Submodule.colon (map (↑e) I) ↑(map (↑e) J ^ m)

Under a ring isomorphism e, the image of the colon (I : J^m) is the colon (e(I) : e(J)^m) — the algebraic step by which the colon stalks are transported along the stalk isomorphisms of an open inclusion or a local isomorphism.

theorem Ideal.map_colon_pow_of_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (e : R →+* S) (he : Function.Bijective ⇑e) (I J : Ideal R) (m : ℕ) : map e (Submodule.colon I ↑(J ^ m)) = Submodule.colon (map e I) ↑(map e J ^ m)

The colon by a power transports along a bijective ring homomorphism (the ring-isomorphism form applied to RingEquiv.ofBijective).

theorem Manifold.germMapOn_germMapOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E₁ : Type u_2} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] {E₂ : Type u_3} [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E₁ M₁] {M₂ : Type u} [TopologicalSpace M₂] [ChartedSpace E₂ M₂] {φ₁ : M₂ → M₁} {V₁ : TopologicalSpace.Opens M₂} (hφ₁ : ContMDiffOn (modelWithCornersSelf 𝕜 E₂) (modelWithCornersSelf 𝕜 E₁) ⊤ φ₁ ↑V₁) {φ₂ : N → M₂} {V₂ : TopologicalSpace.Opens N} (hφ₂ : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E₂) ⊤ φ₂ ↑V₂) {b : N} (hb : b ∈ V₂) {c₂ : M₂} (hc₂ : φ₂ b = c₂) (hc₂V : c₂ ∈ V₁) {c₁ : M₁} (hc₁ : φ₁ c₂ = c₁) {V₃ : TopologicalSpace.Opens N} (hφ₃ : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E₁) ⊤ (φ₁ ∘ φ₂) ↑V₃) (hb₃ : b ∈ V₃) (hc₃ : (φ₁ ∘ φ₂) b = c₁) (s : ↑((structureSheaf 𝕜 E₁ M₁).presheaf.stalk c₁)) : (germMapOn φ₂ hφ₂ hb hc₂) ((germMapOn φ₁ hφ₁ hc₂V hc₁) s) = (germMapOn (φ₁ ∘ φ₂) hφ₃ hb₃ hc₃) s

Composition of stalk maps — (s ∘ φ₁) ∘ φ₂ = s ∘ (φ₁ ∘ φ₂), for any open domain of analyticity of the composite (the stalk map depends on it only through proofs).

theorem Manifold.germMapOn_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E₁ : Type u_2} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E₁ M₁] {φ φ' : N → M₁} {V : TopologicalSpace.Opens N} (hφ : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E₁) ⊤ φ ↑V) (hφ' : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E₁) ⊤ φ' ↑V) {b : N} (hb : b ∈ V) {c : M₁} (hc : φ b = c) (hc' : φ' b = c) (heq : ∀ x ∈ V, φ x = φ' x) (s : ↑((structureSheaf 𝕜 E₁ M₁).presheaf.stalk c)) : (germMapOn φ hφ hb hc) s = (germMapOn φ' hφ' hb hc') s

The stalk map depends only on the map on the open set.

theorem Manifold.germMapOn_map_stalkIdeal_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E₁ : Type u_2} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E₁ M₁] {φ : N → M₁} {V : TopologicalSpace.Opens N} (hφ : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E₁) ⊤ φ ↑V) {b : N} (hb : b ∈ V) {c c' : M₁} (hcc' : c = c') (hc : φ b = c) (hc' : φ b = c') (J : IdealSheaf (structureSheaf 𝕜 E₁ M₁)) : Ideal.map (germMapOn φ hφ hb hc) (J.stalkIdeal c) = Ideal.map (germMapOn φ hφ hb hc') (J.stalkIdeal c')

Transport of the image of a stalk ideal along an equality of base points.

@[simp]

theorem Manifold.IdealSheaf.pullback_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E₁ : Type u_2} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] {E₂ : Type u_3} [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E₁ M₁] {M₂ : Type u} [TopologicalSpace M₂] [ChartedSpace E₂ M₂] (J : IdealSheaf (structureSheaf 𝕜 E₁ M₁)) (φ₁ : M₂ → M₁) (hφ₁ : ContMDiff (modelWithCornersSelf 𝕜 E₂) (modelWithCornersSelf 𝕜 E₁) ⊤ φ₁) (φ₂ : N → M₂) (hφ₂ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E₂) ⊤ φ₂) : pullback φ₂ hφ₂ (pullback φ₁ hφ₁ J) = pullback (φ₁ ∘ φ₂) ⋯ J

Pulling back twice is pulling back along the composite.

theorem Manifold.IdealSheaf.pullback_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E₁ : Type u_2} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E₁ M₁] (J : IdealSheaf (structureSheaf 𝕜 E₁ M₁)) {φ φ' : N → M₁} (hφ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E₁) ⊤ φ) (hφ' : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E₁) ⊤ φ') (h : φ = φ') : pullback φ hφ J = pullback φ' hφ' J

The pullback depends only on the map.

theorem Manifold.contMDiffAt_iff_comp_subtype_val {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {U : TopologicalSpace.Opens M} (f : M → 𝕜) (x : ↥U) : ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 𝕜) ⊤ f ↑x ↔ ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 𝕜) ⊤ (f ∘ Subtype.val) x

Analyticity of a function on M at a point of an open subset U is analyticity of its restriction to the manifold U (Mathlib's liftPropAt_iff_comp_subtype_val).

theorem Manifold.germMap_val_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (U : TopologicalSpace.Opens M) (p : ↥U) : Function.Injective ⇑(germMap Subtype.val ⋯ p)

The stalk map along the inclusion of an open subset is injective (the inclusion maps neighbourhood filters onto neighbourhood filters).

theorem Manifold.germMap_val_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (U : TopologicalSpace.Opens M) (p : ↥U) : Function.Surjective ⇑(germMap Subtype.val ⋯ p)

The stalk map along the inclusion of an open subset is surjective — a germ on U, represented near the point, extends by 0 to an analytic representative on M.

theorem Manifold.germMap_val_bijective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (U : TopologicalSpace.Opens M) (p : ↥U) : Function.Bijective ⇑(germMap Subtype.val ⋯ p)

The stalk isomorphism along an open inclusion — the stalk map 𝒪_{M,p} → 𝒪_{U,p} of Subtype.val : U → M is bijective.

theorem Manifold.germMapOn_partialDiffeomorph_injective {𝕜 : 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₂'] (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁' M₂' ⊤) {x : M₁'} (hx : x ∈ g.source) : Function.Injective ⇑(germMapOn ↑g.toPartialEquiv ⋯ hx ⋯)

The stalk map along a partial diffeomorphism, at a point of its source, is injective (g maps the neighbourhood filter onto that of g x).

theorem Manifold.germMapOn_partialDiffeomorph_surjective {𝕜 : 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₂'] (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁' M₂' ⊤) {x : M₁'} (hx : x ∈ g.source) : Function.Surjective ⇑(germMapOn ↑g.toPartialEquiv ⋯ hx ⋯)

The stalk map along a partial diffeomorphism, at a point of its source, is surjective — a representative near x composed with g⁻¹ represents a germ at g x.

theorem Manifold.germMapOn_partialDiffeomorph_bijective {𝕜 : 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₂'] (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁' M₂' ⊤) {x : M₁'} (hx : x ∈ g.source) : Function.Bijective ⇑(germMapOn ↑g.toPartialEquiv ⋯ hx ⋯)

The stalk isomorphism along a local analytic isomorphism — the stalk map 𝒪_{M₂, g x} → 𝒪_{M₁, x} of a partial diffeomorphism g at a point x of its source is bijective.