Basic properties of the strict transform: off the centre, restriction to opens

The field-independent properties of the strict transform of a closed subspace (saturationStalk, strictTransformSubspace).

• Off the exceptional divisor F the strict transform is the total transform (immediate from the definition; cf. [BM97, Remark 3.15]). The saturation at a' ∉ F is the total transform's stalk (I_{F,a'} = 𝒪, saturationStalk_of_notMem_cosupport), which is the image of I_{π(a')} under the stalk map of π (IdealSheaf.stalkIdeal_pullback); on points, |X'| ∖ |F| = π⁻¹(|X|) ∖ |F| (cosupport_pullback), and since |X'| is closed it contains closure(π⁻¹(|X| ∖ Y)); the points of the exceptional divisor are π⁻¹(Y) (IsBlowUp.cosupport_exceptionalIdealSheaf). The statements about strictTransformSubspace take the finite type of the saturation as the explicit hypothesis hex (saturationStalk_hasLocalGenerators supplies it).
• The saturation stalks commute with restriction to an open U ⊆ M (saturationStalk_restrict; the case of an open inclusion of [Wlo09, Proposition 3.4.1, (2)]): the total transform and the exceptional ideal of the restricted blowing-up are the pullbacks of those of π along the inclusion π⁻¹(U) ⊆ M', the two pullbacks composing as in birationalTransform_restrict; the colon by a power transports along the stalk isomorphism of the inclusion (Ideal.map_colon_pow_of_bijective, germMap_val_bijective), and Ideal.map commutes with the union over k (Ideal.map_iSup).

theorem Manifold.IsBlowUp.cosupport_exceptionalIdealSheaf {𝕜 : 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} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) : (IdealSheaf.pullback π ⋯ hY.idealSheaf).support = π ⁻¹' Y

The points of the exceptional divisor are the preimages of the points of the centre, |F| = π⁻¹(Y) (cosupport_pullback and |I_Y| = Y).

theorem Manifold.stalkIdeal_strictTransformSubspace_of_notMem_cosupport_of_hasLocalGenerators {𝕜 : 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} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (I : IdealSheaf (structureSheaf 𝕜 E M)) (hex : IdealSheaf.HasLocalGenerators (saturationStalk hY h I)) {a' : M'} (ha' : a' ∉ (IdealSheaf.pullback π ⋯ hY.idealSheaf).support) : (strictTransformSubspace hY h I).stalkIdeal a' = Ideal.map (germMap π ⋯ a') (I.stalkIdeal (π a'))

Given the finite type of the saturation: off the exceptional divisor the stalk of the strict transform is the image of the stalk of X under the stalk map of π.

theorem Manifold.cosupport_strictTransformSubspace_diff_of_hasLocalGenerators {𝕜 : 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} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (I : IdealSheaf (structureSheaf 𝕜 E M)) (hex : IdealSheaf.HasLocalGenerators (saturationStalk hY h I)) : (strictTransformSubspace hY h I).support \ (IdealSheaf.pullback π ⋯ hY.idealSheaf).support = π ⁻¹' I.support \ (IdealSheaf.pullback π ⋯ hY.idealSheaf).support

Given the finite type of the saturation: on points, off the exceptional divisor the strict transform is the preimage of X.

theorem Manifold.closure_subset_cosupport_strictTransformSubspace_of_hasLocalGenerators {𝕜 : 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} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (I : IdealSheaf (structureSheaf 𝕜 E M)) (hex : IdealSheaf.HasLocalGenerators (saturationStalk hY h I)) : closure (π ⁻¹' (I.support \ Y)) ⊆ (strictTransformSubspace hY h I).support

Given the finite type of the saturation: |X'| contains the closure of π⁻¹(|X| ∖ Y).

theorem Manifold.saturationStalk_restrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {U : TopologicalSpace.Opens M} {U' : TopologicalSpace.Opens M'} (hU' : ↑U' = π ⁻¹' ↑U) {π' : ↥U' → ↥U} (hπ' : ∀ (p : ↥U'), ↑(π' p) = π ↑p) (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (I : IdealSheaf (structureSheaf 𝕜 E M)) (q : ↥U') : saturationStalk ⋯ ⋯ (IdealSheaf.pullback Subtype.val ⋯ I) q = Ideal.map (germMap Subtype.val ⋯ q) (saturationStalk hY h I ↑q)

The saturation commutes with restriction to an open subset — on the restricted blowing-up π' : π⁻¹(U) → U, the saturation stalk of I|_U at q is the saturation stalk of I at q transported along the stalk isomorphism of the inclusion π⁻¹(U) ⊆ M' (birationalTransform_restrict).