Germ-locality of the ideal sheaf of a closed submanifold, and total transforms of products

Four general facts about ideal sheaves on an analytic manifold, used to compute the total transform of the monomial part under a blow-up (BMO/Step1ExistsComap.lean):

• the ideal sheaf of a closed submanifold is germ-local: its stalk at x depends only on the submanifold near x, so two closed submanifolds that agree on an open neighbourhood of x have the same ideal stalk there (IsClosedSubmanifold.stalkIdeal_idealSheaf_eq_of_inter_eq; the variant …_left for a submanifold cut out of another by an open set);
• the total transform of an ideal sheaf has unit stalk at every point whose image lies off a set outside which the ideal sheaf has unit stalks (totalTransform_stalkIdeal_eq_top_of_notMem_preimage);
• the stalk of the total transform of a locally finite product of ideal sheaves (BMO/LocallyFiniteProduct.lean) is the finite product of the stalks of the total transforms of the factors active at the image point (stalkIdeal_totalTransform_locallyFiniteProduct);
• the total transform is multiplicative, π^*(A · B) = π^*(A) · π^*(B) (IdealSheaf.pullback_mul).

Not in the sources; auxiliary lemmas for Step 1 of the proof of [Kol07, Theorem 107].

theorem Manifold.IsClosedSubmanifold.stalkIdeal_idealSheaf_eq_of_inter_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ ψ' : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S T : Set M} {c c' : ℕ} (hS : IsClosedSubmanifold ψ S c) (hT : IsClosedSubmanifold ψ' T c') {W : Set M} (hW : IsOpen W) {x : M} (hxW : x ∈ W) (hST : S ∩ W = T ∩ W) : hS.idealSheaf.stalkIdeal x = hT.idealSheaf.stalkIdeal x

Germ-locality of the ideal sheaf of a closed submanifold: if two closed submanifolds S, T agree on an open set W containing x, their ideal stalks at x coincide. At a point of S (hence of T) a germ lies in either stalk ideal exactly when its section vanishes on the submanifold near x, and 𝓝[S] x = 𝓝[T] x; off S (hence off T) both stalks are the unit ideal.

theorem Manifold.IsClosedSubmanifold.stalkIdeal_idealSheaf_eq_of_inter_eq_left {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ ψ' : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S C : Set M} {c c' : ℕ} (hS : IsClosedSubmanifold ψ S c) (hC : IsClosedSubmanifold ψ' C c') {W : Set M} (hW : IsOpen W) (hSW : S ∩ W = C) {x : M} (hxC : x ∈ C) : hS.idealSheaf.stalkIdeal x = hC.idealSheaf.stalkIdeal x

If a closed submanifold C is cut out of a closed submanifold S by an open set, S ∩ W = C, then at a point of C the two ideal sheaves have the same stalk: S and C agree on W. The case of a connected component of a member of a boundary family.

theorem Hironaka.Manifold.totalTransform_stalkIdeal_eq_top_of_notMem_preimage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (h : Manifold.IsBlowUp ψ Y c π) (B : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {S₀ : Set M} (hB : ∀ y ∉ S₀, B.stalkIdeal y = ⊤) {x : M'} (hx : x ∉ π ⁻¹' S₀) : (Manifold.IdealSheaf.pullback π ⋯ B).stalkIdeal x = ⊤

The total transform of an ideal sheaf B has unit stalk at every point whose image lies off a set S₀ outside which B has unit stalks.

theorem Hironaka.Manifold.stalkIdeal_totalTransform_locallyFiniteProduct {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {κ : Type u} (h : Manifold.IsBlowUp ψ Y c π) (A : κ → Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (S : κ → Set M) (hLF : LocallyFinite S) (hunit : ∀ (i : κ), ∀ x ∉ S i, (A i).stalkIdeal x = ⊤) (x : M') : (Manifold.IdealSheaf.pullback π ⋯ (Manifold.IdealSheaf.locallyFiniteProduct (Manifold.structureSheaf 𝕜 E M) A S hLF hunit)).stalkIdeal x = ∏ i ∈ Manifold.IdealSheaf.activeFinset S hLF (π x), (Manifold.IdealSheaf.pullback π ⋯ (A i)).stalkIdeal x

The total transform of a locally finite product, stalkwise: at a point x of the blow-up, the stalk of π^*(∏ᵢ Aᵢ) is the finite product, over the indices i active at π x, of the stalks of π^*(Aᵢ). The stalk of a total transform is the image of the stalk below under the germ map, and Ideal.map distributes over the finite product.