The pull-back of the ideal sheaf of a closed submanifold along a local analytic isomorphism

For a local analytic isomorphism h : N → M and a closed submanifold Y ⊆ M, the pull-back h^*I_Y of the ideal sheaf of Y is the ideal sheaf of the preimage submanifold h⁻¹(Y) (IsClosedSubmanifold.preimage_of_isLocalDiffeomorph): comap h hY.idealSheaf = (hY.preimage_of_isLocalDiffeomorph hh).idealSheaf (comap_idealSheaf_of_isLocalDiffeomorph). This is Kollár's pull-back of a blow-up centre along a smooth morphism [Kol07, 30.1] and the reducedness of the pulled-back centre used in the chart computation of his proof of the uniqueness of blow-up sequences [Kol07, Theorem 97, proof]; it is the centre clause of the one-step descent lemma (agreeOnSubspace_blowUpLift) for the lifts of local isomorphisms along a blow-up sequence.

Proof: both sides have cosupport h⁻¹(Y); at a ∈ h⁻¹(Y) the stalk of the pull-back is the image of the stalk I_{Y, h a} = (x_{σ i}) under h^* (isIdealSheafOf_idealSheaf), and the germs x_{σ i} ∘ h are the adapted coordinates of the transported chart φ ∘ h of h⁻¹(Y) at a (transportChart along a local inverse Φ of h, isAdaptedChart_transportChart), which generate I_{h⁻¹Y, a} by the same specification; off h⁻¹(Y) both stalks are the unit ideal. Also stalkIdeal_comap_eq_map_germMap: the stalk of a pull-back is the image of the stalk under the stalk map.

theorem Manifold.stalkIdeal_comap_eq_map_germMap {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (J : M.IdealSheaf) (a : N.carrier) : (IdealSheaf.pullback ⇑h ⋯ J).stalkIdeal a = Ideal.map (germMap ⇑h ⋯ a) (IdealSheaf.stalkIdeal J (h a))

The stalk of the pull-back at a is the image of the stalk at h a.

theorem Manifold.germMap_coord_eq_coord_transportChart {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (hΦ : Set.EqOn (⇑h) (↑Φ.toPartialEquiv) Φ.source) {a : N.carrier} (ha : a ∈ Φ.source) (φ : OpenPartialHomeomorph M.carrier E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) (hφa : h a ∈ φ.source) (hφ' : transportChart Φ.symm φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N.carrier) (ha' : a ∈ (transportChart Φ.symm φ).source) (i : Fin n) : (germMap ⇑h ⋯ a) (coord E ψ φ hφ hφa i) = coord E ψ (transportChart Φ.symm φ) hφ' ha' i

The coordinate germ of the transported chart φ ∘ Φ at a is the pull-back along h of the coordinate germ of φ at h a, when h = Φ near a.

theorem Manifold.comap_idealSheaf_of_isLocalDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : IdealSheaf.pullback ⇑h ⋯ hY.idealSheaf = ⋯.idealSheaf

The pull-back of the ideal sheaf of a closed submanifold along a local analytic isomorphism is the ideal sheaf of the preimage submanifold ([Kol07, 30.1]; the centre clause of agreeOnSubspace_blowUpLift for the lifts of local isomorphisms — Kollár's ψ_i^* I_{Z_i} = I_{Z_i^U} for étale ψ_i).