Closed submanifolds of a coproduct manifold

Given closed submanifolds S i ⊆ N i of codimension s of countably many analytic manifolds modelled on E, the union of their images under the summand inclusions sigmaMk N i is a closed submanifold S* ⊆ sigmaManifold N of codimension s, and the coproduct of the bundled submanifolds is the bundled submanifold S*. Not in the sources: bookkeeping for the comparison of resolutions along a closed embedding of a coproduct (cf. [Kol07, 34.4]).

• preimage_sigmaMk_iUnion_image: sigmaMk N i ⁻¹' (⋃ j, sigmaMk N j '' Y j) = Y i — the summand images are disjoint and sigmaMk N i is injective (the identity behind every clause below);
• isClosedSubmanifold_sigmaUnion: S* is a closed submanifold, the instance of IsClosedSubmanifold.iUnion_image at the summand inclusions;
• sigmaSubmanifoldIncl (the summand inclusion of the bundled S i into the bundled S*, IsClosedSubmanifold.restrictMap along sigmaMk N i), a local diffeomorphism; sigmaSubmanifoldDesc (their descent, sigmaDescMap), bijective; sigmaSubmanifoldDiffeomorph (IsLocalDiffeomorph.toDiffeomorphOfBijective), with the two compatibilities inclusionMap_sigmaSubmanifoldDiffeomorph_mk (with the inclusion maps) and sigmaSubmanifoldDiffeomorph_comp_sigmaMk (with the summand inclusions);
• idealSheaf_sigmaUnion: the ideal sheaf of S* is the coproduct ideal sheaf IdealSheaf.sigmaOf N (fun i => (hS i).idealSheaf);
• preimage_sigmaSubmanifoldDiffeomorph_preimageOpens: the preimage under the diffeomorphism of preimageOpens U on S* is the union of the summand images of the pieces' preimageOpens of the preimages of U along sigmaMk N i; and preimageOpens_sigmaMk_sigmaCoordImage: sigmaMk i ⁻¹' sigmaCoordImage G W = W i as Opens;
• sigmaMapDiffeomorph: the coproduct of a family of diffeomorphisms e i : M i ≅ N i (one pair of models E, E') is a diffeomorphism sigmaManifold M ≅ sigmaManifold N with sigmaMapDiffeomorph e (sigmaMk M i x) = sigmaMk N i (e i x).

Everything here is at the level of manifolds; no blow-up sequence enters. It is used to compare the resolution of a disjoint union of pieces with the disjoint union of their resolutions (Hironaka/Resolution/Analytic/Kol07Thm45/CoproductPadIdentity.lean).

Preimages along the summand inclusions

theorem Hironaka.Manifold.preimage_sigmaMk_iUnion_image {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (Y : (i : σ) → Set (N i).carrier) (i : σ) : ⇑(Manifold.sigmaMk N i) ⁻¹' ⋃ (j : σ), ⇑(Manifold.sigmaMk N j) '' Y j = Y i

The preimage under the summand inclusion sigmaMk N i of a union of summand images is the i-th set: the summand images are pairwise disjoint (pairwise_disjoint_range_sigmaMk) and sigmaMk N i is injective.

theorem Hironaka.Manifold.sigmaMk_mem_iUnion_image {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (Y : (i : σ) → Set (N i).carrier) (i : σ) (x : (N i).carrier) : x ∈ Y i → (Manifold.sigmaMk N i) x ∈ ⋃ (j : σ), ⇑(Manifold.sigmaMk N j) '' Y j

The summand inclusion maps Y i into the union of the summand images.

The restricted map along a local diffeomorphism, for an equal preimage

theorem Manifold.IsClosedSubmanifold.isLocalDiffeomorph_restrictMap_of_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {A B : AnalyticManifold 𝕜 E} (h : AnalyticMap B A) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {S : Set A.carrier} {S' : Set B.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (hS' : IsClosedSubmanifold ψ S' s) (heq : S' = ⇑h ⁻¹' S) (hmaps : ∀ x ∈ S', h x ∈ S) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ ⇑(hS'.restrictMap hS ⇑h ⋯ hmaps)

IsClosedSubmanifold.isLocalDiffeomorph_restrictMap for a closed submanifold S' equal to the preimage h ⁻¹' S (not syntactically the preimage): the restriction of the local analytic isomorphism h to S' → S is a local analytic isomorphism of the bundled submanifolds.

The coproduct slice

theorem Hironaka.Manifold.isClosedSubmanifold_sigmaUnion {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) : Manifold.IsClosedSubmanifold ψ (⋃ (i : σ), ⇑(Manifold.sigmaMk N i) '' S i) s

The union of the summand images of closed submanifolds of codimension s is a closed submanifold of the coproduct of codimension s: IsClosedSubmanifold.iUnion_image at the summand inclusions.

noncomputable def Hironaka.Manifold.sigmaSubmanifoldIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) (i : σ) : AnalyticMap ⋯.toAnalyticManifold ⋯.toAnalyticManifold

The summand inclusion of the coproduct slice: the restriction of sigmaMk N i to the bundled submanifolds (IsClosedSubmanifold.restrictMap).

Equations

• Hironaka.Manifold.sigmaSubmanifoldIncl hS i = ⋯.restrictMap ⋯ ⇑(Manifold.sigmaMk N i) ⋯ ⋯

theorem Hironaka.Manifold.inclusionMap_sigmaSubmanifoldIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) (i : σ) (p : ⋯.toAnalyticManifold.carrier) : ⋯.inclusionMap ((sigmaSubmanifoldIncl hS i) p) = (Manifold.sigmaMk N i) (⋯.inclusionMap p)

The summand inclusion of the slice commutes with the inclusion maps.

theorem Hironaka.Manifold.isLocalDiffeomorph_sigmaSubmanifoldIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) (i : σ) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ ⇑(sigmaSubmanifoldIncl hS i)

The summand inclusion of the slice is a local analytic isomorphism (isLocalDiffeomorph_restrictMap_of_eq at sigmaMk N i, whose preimage of the slice is S i).

noncomputable def Hironaka.Manifold.sigmaSubmanifoldDesc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) : AnalyticMap (Manifold.sigmaManifold fun (i : σ) => ⋯.toAnalyticManifold) ⋯.toAnalyticManifold

The descent of the summand inclusions, ∐ᵢ Sᵢ → S*.

Equations

• Hironaka.Manifold.sigmaSubmanifoldDesc hS = Manifold.sigmaDescMap fun (i : σ) => Hironaka.Manifold.sigmaSubmanifoldIncl hS i

theorem Hironaka.Manifold.sigmaSubmanifoldDesc_mk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) (i : σ) (p : ⋯.toAnalyticManifold.carrier) : (sigmaSubmanifoldDesc hS) ((Manifold.sigmaMk (fun (i : σ) => ⋯.toAnalyticManifold) i) p) = (sigmaSubmanifoldIncl hS i) p

The descent on the i-th summand is the i-th inclusion.

theorem Hironaka.Manifold.isLocalDiffeomorph_sigmaSubmanifoldDesc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ ⇑(sigmaSubmanifoldDesc hS)

The descent of the summand inclusions is a local diffeomorphism (each inclusion is one).

theorem Hironaka.Manifold.bijective_sigmaSubmanifoldDesc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) : Function.Bijective ⇑(sigmaSubmanifoldDesc hS)

The descent is bijective: injective since the summand images are disjoint and each summand inclusion is injective, surjective since every point of the slice lies in some summand image.

noncomputable def Hironaka.Manifold.sigmaSubmanifoldDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (Manifold.sigmaManifold fun (i : σ) => ⋯.toAnalyticManifold).carrier ⋯.toAnalyticManifold.carrier ⊤

The coproduct of the bundled submanifolds is analytically isomorphic to the bundled slice (IsLocalDiffeomorph.toDiffeomorphOfBijective).

Equations

• Hironaka.Manifold.sigmaSubmanifoldDiffeomorph hS = ⋯.toDiffeomorphOfBijective ⋯

theorem Hironaka.Manifold.coe_sigmaSubmanifoldDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) : ⇑(sigmaSubmanifoldDiffeomorph hS) = ⇑(sigmaSubmanifoldDesc hS)

The diffeomorphism's underlying map is the descent sigmaSubmanifoldDesc.

theorem Hironaka.Manifold.sigmaSubmanifoldDiffeomorph_mk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) (i : σ) (p : ⋯.toAnalyticManifold.carrier) : (sigmaSubmanifoldDiffeomorph hS) ((Manifold.sigmaMk (fun (i : σ) => ⋯.toAnalyticManifold) i) p) = (sigmaSubmanifoldIncl hS i) p

theorem Hironaka.Manifold.inclusionMap_sigmaSubmanifoldDiffeomorph_mk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) (i : σ) (p : ⋯.toAnalyticManifold.carrier) : ⋯.inclusionMap ((sigmaSubmanifoldDiffeomorph hS) ((Manifold.sigmaMk (fun (i : σ) => ⋯.toAnalyticManifold) i) p)) = (Manifold.sigmaMk N i) (⋯.inclusionMap p)

The isomorphism commutes with the inclusion maps: hS*.inclusionMap (Φ ⟨i, p⟩) = sigmaMk N i ((hS i).inclusionMap p).

theorem Hironaka.Manifold.sigmaSubmanifoldDiffeomorph_comp_sigmaMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) (i : σ) : ⇑(sigmaSubmanifoldDiffeomorph hS) ∘ ⇑(Manifold.sigmaMk (fun (i : σ) => ⋯.toAnalyticManifold) i) = ⇑(sigmaSubmanifoldIncl hS i)

The isomorphism composed with the i-th summand inclusion of the coproduct is the i-th summand inclusion of the slice.

theorem Hironaka.Manifold.idealSheaf_sigmaUnion {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) : ⋯.idealSheaf = Manifold.IdealSheaf.sigmaOf N fun (i : σ) => ⋯.idealSheaf

The ideal sheaf of the slice is the coproduct ideal sheaf of the pieces' (IdealSheaf.ext_of_comap_sigmaMk; per summand comap_sigmaMk_sigmaOf, idealSheaf_preimage_of_isLocalDiffeomorph at sigmaMk N i and idealSheaf_congr on preimage_sigmaMk_iUnion_image).

theorem Hironaka.Manifold.preimage_sigmaSubmanifoldDiffeomorph_preimageOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} {S : (i : σ) → Set (N i).carrier} {s : ℕ} (hS : ∀ (i : σ), Manifold.IsClosedSubmanifold ψ (S i) s) (U : TopologicalSpace.Opens (Manifold.sigmaManifold N).carrier) : ⇑(sigmaSubmanifoldDiffeomorph hS) ⁻¹' ↑(⋯.preimageOpens U) = ⋃ (i : σ), ⇑(Manifold.sigmaMk (fun (i : σ) => ⋯.toAnalyticManifold) i) '' ↑(⋯.preimageOpens (Manifold.preimageOpens ⇑(Manifold.sigmaMk N i) ⋯ U))

The preimage under the isomorphism of the slice's reading of an open U of the coproduct is the union of the summand images of the pieces' readings of the preimages of U along the summand inclusions.

The coordinate image read on a summand

theorem Hironaka.Manifold.preimageOpens_sigmaMk_sigmaCoordImage {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Finite ι] (G : ι → TopologicalSpace.Opens (Fin n → 𝕜)) (W : (i : ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (G i)).carrier) (i : ι) : Manifold.preimageOpens ⇑(Manifold.sigmaMk (fun (i : ι) => pieceAmbient 𝕜 (G i)) i) ⋯ (sigmaCoordImage G W) = W i

The preimage along the i-th summand inclusion of sigmaCoordImage G W = ⋃ⱼ sigmaMk j '' W j is W i, as Opens (coe_sigmaCoordImage, preimage_sigmaMk_iUnion_image).

The coproduct of a family of diffeomorphisms

theorem Hironaka.Manifold.isLocalDiffeomorph_sigmaMapFun {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : σ → AnalyticManifold 𝕜 E} {N : σ → AnalyticManifold 𝕜 E'} (e : (i : σ) → Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (M i).carrier (N i).carrier ⊤) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') ⊤ fun (p : (Manifold.sigmaManifold M).carrier) => (Manifold.sigmaMk N p.fst) ((e p.fst) p.snd)

The summand-wise map of a family of diffeomorphisms is a local analytic isomorphism of the coproducts (IsLocalDiffeomorph.sigmaDesc of the compositions sigmaMk N i ∘ e i).

theorem Hironaka.Manifold.bijective_sigmaMapFun {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : σ → AnalyticManifold 𝕜 E} {N : σ → AnalyticManifold 𝕜 E'} (e : (i : σ) → Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (M i).carrier (N i).carrier ⊤) : Function.Bijective fun (p : (Manifold.sigmaManifold M).carrier) => (Manifold.sigmaMk N p.fst) ((e p.fst) p.snd)

The summand-wise map of a family of diffeomorphisms is bijective.

noncomputable def Hironaka.Manifold.sigmaMapDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : σ → AnalyticManifold 𝕜 E} {N : σ → AnalyticManifold 𝕜 E'} (e : (i : σ) → Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (M i).carrier (N i).carrier ⊤) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (Manifold.sigmaManifold M).carrier (Manifold.sigmaManifold N).carrier ⊤

The coproduct of a family of diffeomorphisms e i : M i ≅ N i (one pair of models E, E') as a diffeomorphism of the coproducts, with sigmaMapDiffeomorph e (sigmaMk M i x) = sigmaMk N i (e i x) by rfl.

Equations

• Hironaka.Manifold.sigmaMapDiffeomorph e = ⋯.toDiffeomorphOfBijective ⋯

theorem Hironaka.Manifold.sigmaMapDiffeomorph_mk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : σ → AnalyticManifold 𝕜 E} {N : σ → AnalyticManifold 𝕜 E'} (e : (i : σ) → Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (M i).carrier (N i).carrier ⊤) (i : σ) (x : (M i).carrier) : (sigmaMapDiffeomorph e) ((Manifold.sigmaMk M i) x) = (Manifold.sigmaMk N i) ((e i) x)