Descent of a centre along a surjective local analytic isomorphism

In the proof of [Kol07, Proposition 37], the blow-up sequences B(X') and B(X'') start with centres Z₀' ⊂ X' and Z₀'' ⊂ X''; since B commutes with the projections τᵢ, τ₁^*(Z₀') = Z₀'' = τ₂^*(Z₀') (37.1), and the subschemes Z₀ᵢ' ⊂ Uᵢ glue to a subscheme Z₀ ⊂ X (37.2). On manifolds: for a surjective local analytic isomorphism g : N → M with a fibre product (P, p₁, p₂) of g with itself, the equation p₁⁻¹(Z') = p₂⁻¹(Z') says that Z' is saturated, g⁻¹(g(Z')) = Z' (saturated_of_isFibreProduct); a saturated closed submanifold descends: g(Z') is closed (its complement is g(Z'ᶜ), open) and a closed submanifold of the same codimension, its adapted charts the adapted charts of Z' transported along local inverses of g (transportChart): IsClosedSubmanifold.image_of_saturated, the gluing of (37.2).

theorem Manifold.saturated_of_isFibreProduct {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N P : AnalyticManifold 𝕜 E} {g : AnalyticMap N M} {p₁ p₂ : AnalyticMap P N} (hp : IsFibreProduct g g p₁ p₂) {Z' : Set N.carrier} (hZ : ⇑p₁ ⁻¹' Z' = ⇑p₂ ⁻¹' Z') : ⇑g ⁻¹' ⇑g '' Z' = Z'

Kollár (37.1)–(37.2): if the two pull-backs of Z' to a fibre product of g with itself agree, Z' is saturated for g.

theorem Manifold.image_compl_of_saturated {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} {g : N.carrier → M.carrier} (hs : Function.Surjective g) {Z' : Set N.carrier} (hsat : g ⁻¹' g '' Z' = Z') : g '' Z'ᶜ = (g '' Z')ᶜ

A saturated set is the preimage of its image, so its complement's image is the complement of its image (for surjective g).

theorem Manifold.image_partialDiffeomorph_eq_of_saturated {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} {g : AnalyticMap N M} (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (hΦ : Set.EqOn (⇑g) (↑Φ.toPartialEquiv) Φ.source) {Z' : Set N.carrier} (hsat : ⇑g ⁻¹' ⇑g '' Z' = Z') : ↑Φ.toPartialEquiv '' (Z' ∩ Φ.source) = ⇑g '' Z' ∩ Φ.target

The image of a saturated set under a local inverse Φ of g is the image of the set.

theorem Manifold.IsClosedSubmanifold.image_of_saturated {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {g : AnalyticMap N M} (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hs : Function.Surjective ⇑g) {Z' : Set N.carrier} {c : ℕ} (hZ' : IsClosedSubmanifold ψ₀ Z' c) (hsat : ⇑g ⁻¹' ⇑g '' Z' = Z') : IsClosedSubmanifold ψ₀ (⇑g '' Z') c

Kollár (37.2), the subschemes Z₀ᵢ' ⊂ Uᵢ glue to a subscheme Z₀ ⊂ X: the image of a saturated closed submanifold under a surjective local analytic isomorphism is a closed submanifold of the same codimension — closed because its complement is the image of the open complement, with adapted charts transported along local inverses.