A closed submanifold of the bundled S is a closed submanifold of M

The push-forward of a blow-up sequence of a closed subscheme S ⊆ X regards its centres Z_i^S ⊆ S_i ⊆ X_i as closed subschemes Z_i^X := (j_i)_* Z_i^S of X_i [Kol07, Definition 30.3]. This module proves the manifold statement, the converse of IsClosedSubmanifold.preimage_val_of_subset (Nested.lean): a closed submanifold Y' of the bundled S (with its induced charts on 𝕜^{n-s}) of codimension c' is, read in M, a closed submanifold of codimension c' + s (IsClosedSubmanifold.imageVal_isClosedSubmanifold); a smooth subspace of a manifold is locally a coordinate subspace [BM97, (3.8)(2)].

The adapted chart at a point of Y' is built from an adapted chart φ of S in M (S = {z_{σ₁} = 0}) and an adapted chart χ of Y' in S: the chart change θ = χ ∘ χ₀⁻¹ of 𝕜^{n-s} between the induced chart χ₀ of φ and χ is analytic (both lie in the maximal atlas of S), and it is extended to 𝕜^n by the identity on the σ₁-coordinates (extendComplFun, extendCompl, extendComplE) — a chart change of E in the analytic groupoid. The chart φ ∘ Θ of M then reads S on the σ₁-coordinates and χ on the complementary ones, so Y' is the zero set of the s + c' coordinates σ₁ ⊔ σ' (imageValEmb). Not in the sources; a chart computation.

The model: a chart change of 𝕜^{n-s} extended by the identity on s coordinates

noncomputable def Manifold.extendComplFun {𝕜 : Type} {n s : ℕ} (σ : Fin s ↪ Fin n) (f : (Fin (n - s) → 𝕜) → Fin (n - s) → 𝕜) (z : Fin n → 𝕜) : Fin n → 𝕜

The map of 𝕜^n that is the identity on the coordinates σ and f on the complementary coordinates (read through projCompl and complEquiv).

Equations

• Manifold.extendComplFun σ f z j = if h : j ∈ Set.range ⇑σ then z j else f (Manifold.projCompl σ z) ((Manifold.complEquiv σ) ⟨j, h⟩)

theorem Manifold.extendComplFun_apply_range {𝕜 : Type} {n s : ℕ} (σ : Fin s ↪ Fin n) (f : (Fin (n - s) → 𝕜) → Fin (n - s) → 𝕜) (z : Fin n → 𝕜) (i : Fin s) : extendComplFun σ f z (σ i) = z (σ i)

theorem Manifold.extendComplFun_apply_compl {𝕜 : Type} {n s : ℕ} (σ : Fin s ↪ Fin n) (f : (Fin (n - s) → 𝕜) → Fin (n - s) → 𝕜) (z : Fin n → 𝕜) (k : Fin (n - s)) : extendComplFun σ f z ↑((complEquiv σ).symm k) = f (projCompl σ z) k

theorem Manifold.projCompl_extendComplFun {𝕜 : Type} {n s : ℕ} (σ : Fin s ↪ Fin n) (f : (Fin (n - s) → 𝕜) → Fin (n - s) → 𝕜) (z : Fin n → 𝕜) : projCompl σ (extendComplFun σ f z) = f (projCompl σ z)

theorem Manifold.extendComplFun_extendComplFun {𝕜 : Type} {n s : ℕ} (σ : Fin s ↪ Fin n) {f g : (Fin (n - s) → 𝕜) → Fin (n - s) → 𝕜} {z : Fin n → 𝕜} (hgf : g (f (projCompl σ z)) = projCompl σ z) : extendComplFun σ g (extendComplFun σ f z) = z

theorem Manifold.continuousOn_extendComplFun {𝕜 : Type} {n s : ℕ} [RCLike 𝕜] (σ : Fin s ↪ Fin n) {f : (Fin (n - s) → 𝕜) → Fin (n - s) → 𝕜} {U : Set (Fin (n - s) → 𝕜)} (hf : ContinuousOn f U) : ContinuousOn (extendComplFun σ f) {z : Fin n → 𝕜 | projCompl σ z ∈ U}

theorem Manifold.contDiffOn_extendComplFun {𝕜 : Type} {n s : ℕ} [RCLike 𝕜] (σ : Fin s ↪ Fin n) {f : (Fin (n - s) → 𝕜) → Fin (n - s) → 𝕜} {U : Set (Fin (n - s) → 𝕜)} (hf : ContDiffOn 𝕜 ⊤ f U) : ContDiffOn 𝕜 ⊤ (extendComplFun σ f) {z : Fin n → 𝕜 | projCompl σ z ∈ U}

noncomputable def Manifold.extendCompl {𝕜 : Type} {n s : ℕ} [RCLike 𝕜] (σ : Fin s ↪ Fin n) (θ : OpenPartialHomeomorph (Fin (n - s) → 𝕜) (Fin (n - s) → 𝕜)) : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)

A partial homeomorphism θ of 𝕜^{n-s} extended to 𝕜^n by the identity on the coordinates σ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Manifold.extendComplE {𝕜 : Type} {n s : ℕ} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (ψ : E ≃L[𝕜] Fin n → 𝕜) (σ : Fin s ↪ Fin n) (θ : OpenPartialHomeomorph (Fin (n - s) → 𝕜) (Fin (n - s) → 𝕜)) : OpenPartialHomeomorph E E

The chart change of E corresponding to extendCompl σ θ through ψ.

Equations

• Manifold.extendComplE ψ σ θ = ψ.toHomeomorph.toOpenPartialHomeomorph.trans ((Manifold.extendCompl σ θ).trans ψ.symm.toHomeomorph.toOpenPartialHomeomorph)

theorem Manifold.extendComplE_apply {𝕜 : Type} {n s : ℕ} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (ψ : E ≃L[𝕜] Fin n → 𝕜) (σ : Fin s ↪ Fin n) (θ : OpenPartialHomeomorph (Fin (n - s) → 𝕜) (Fin (n - s) → 𝕜)) (v : E) : ↑(extendComplE ψ σ θ) v = ψ.symm (extendComplFun σ (↑θ) (ψ v))

theorem Manifold.mem_extendComplE_source {𝕜 : Type} {n s : ℕ} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (ψ : E ≃L[𝕜] Fin n → 𝕜) (σ : Fin s ↪ Fin n) (θ : OpenPartialHomeomorph (Fin (n - s) → 𝕜) (Fin (n - s) → 𝕜)) {v : E} : v ∈ (extendComplE ψ σ θ).source ↔ projCompl σ (ψ v) ∈ θ.source

theorem Manifold.mem_extendComplE_target {𝕜 : Type} {n s : ℕ} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (ψ : E ≃L[𝕜] Fin n → 𝕜) (σ : Fin s ↪ Fin n) (θ : OpenPartialHomeomorph (Fin (n - s) → 𝕜) (Fin (n - s) → 𝕜)) {v : E} : v ∈ (extendComplE ψ σ θ).target ↔ projCompl σ (ψ v) ∈ θ.target

theorem Manifold.extendComplE_mem_contDiffGroupoid {𝕜 : Type} {n s : ℕ} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (ψ : E ≃L[𝕜] Fin n → 𝕜) (σ : Fin s ↪ Fin n) (θ : OpenPartialHomeomorph (Fin (n - s) → 𝕜) (Fin (n - s) → 𝕜)) (hθ : ContDiffOn 𝕜 ⊤ (↑θ) θ.source) (hθ' : ContDiffOn 𝕜 ⊤ (↑θ.symm) θ.target) : extendComplE ψ σ θ ∈ contDiffGroupoid ⊤ (modelWithCornersSelf 𝕜 E)

The extended chart change lies in the analytic groupoid of E when θ is analytic both ways.

noncomputable def Manifold.imageValEmb {n s c' : ℕ} (σ₁ : Fin s ↪ Fin n) (σ' : Fin c' ↪ Fin (n - s)) : Fin (c' + s) ↪ Fin n

The block embedding of Y' ⊆ S ⊆ M: the s coordinates of S and the c' coordinates of Y' inside S, the latter read among the complementary coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.imageValEmb_inl {n s c' : ℕ} (σ₁ : Fin s ↪ Fin n) (σ' : Fin c' ↪ Fin (n - s)) (k' : Fin c') : (imageValEmb σ₁ σ') (finSumFinEquiv (Sum.inl k')) = ↑((complEquiv σ₁).symm (σ' k'))

theorem Manifold.imageValEmb_inr {n s c' : ℕ} (σ₁ : Fin s ↪ Fin n) (σ' : Fin c' ↪ Fin (n - s)) (j : Fin s) : (imageValEmb σ₁ σ') (finSumFinEquiv (Sum.inr j)) = σ₁ j

The image of a closed submanifold of the bundled S

def Manifold.IsClosedSubmanifold.imageVal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (Y' : Set hS.toAnalyticManifold.carrier) : Set M

A subset of the bundled S read in M through the inclusion (the centres Z_i^X := (j_i)_* Z_i^S of the push-forward of a blow-up sequence, [Kol07, Definition 30.3]).

Equations

• hS.imageVal Y' = Subtype.val '' Y'

theorem Manifold.IsClosedSubmanifold.mem_imageVal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (Y' : Set hS.toAnalyticManifold.carrier) (x : M) : x ∈ hS.imageVal Y' ↔ ∃ p ∈ Y', ↑p = x

theorem Manifold.IsClosedSubmanifold.preimageVal_imageVal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (Y' : Set hS.toAnalyticManifold.carrier) : hS.preimageVal (hS.imageVal Y') = Y'

Reading a subset of the bundled S in M and back gives it back.

theorem Manifold.IsClosedSubmanifold.imageVal_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (Y' : Set hS.toAnalyticManifold.carrier) : hS.imageVal Y' ⊆ S

theorem Manifold.IsClosedSubmanifold.isClosed_imageVal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) {Y' : Set hS.toAnalyticManifold.carrier} (hY' : IsClosed Y') : IsClosed (hS.imageVal Y')

theorem Manifold.IsClosedSubmanifold.isAdaptedChart_extendComplE {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) {Y' : Set hS.toAnalyticManifold.carrier} {c' : ℕ} {a' : hS.toAnalyticManifold.carrier} {χ : OpenPartialHomeomorph hS.toAnalyticManifold.carrier (Fin (n - s) → 𝕜)} {σ' : Fin c' ↪ Fin (n - s)} (ha'χ : a' ∈ χ.source) (hχ : IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Y' χ σ') {φ : OpenPartialHomeomorph M E} {σ₁ : Fin s ↪ Fin n} (haφ : ↑a' ∈ φ.source) (hφ : IsAdaptedChart ψ S φ σ₁) : ↑a' ∈ (φ.trans (extendComplE ψ σ₁ ((hS.inducedChart hφ ⋯).symm.trans χ))).source ∧ IsAdaptedChart ψ (hS.imageVal Y') (φ.trans (extendComplE ψ σ₁ ((hS.inducedChart hφ ⋯).symm.trans χ))) (imageValEmb σ₁ σ')

The chart of M extending a chart of the bundled S by the equations of S (the chart of imageVal_isClosedSubmanifold, stated separately because the chart itself is used when simple normal crossings are lifted along a restricted succession): for φ adapted to S and containing (a' : M) in its source, χ₀ the induced chart of φ on S, and χ a chart of S adapted to Y' containing a' in its source, the chart φ ≫ₕ extendComplE ψ σ₁ (χ₀⁻¹ ≫ₕ χ) of M contains (a' : M) in its source and is adapted to imageVal Y' with the indices imageValEmb σ₁ σ' — the s coordinates of S from φ, the c' coordinates of Y' from χ through the chart change χ ∘ χ₀⁻¹ of 𝕜^{n−s}.

theorem Manifold.IsClosedSubmanifold.imageVal_isClosedSubmanifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) {Y' : Set hS.toAnalyticManifold.carrier} {c' : ℕ} (hY' : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Y' c') : IsClosedSubmanifold ψ (hS.imageVal Y') (c' + s)

A closed submanifold of a closed submanifold is a closed submanifold, the converse of preimage_val_of_subset: a closed submanifold Y' of the bundled S of codimension c' is, read in M, a closed submanifold of codimension c' + s.