Finite shrunk covers of a relatively compact open by open embeddings

The per-open identities of the family functors are read on a relatively compact open U of a manifold M, so a local question on M reduces to finitely many pieces covering the compact closure U. Two such reductions share their cover: Step 3 of the proof of [Kol07, Theorem 103] (the neighbourhoods with maximal contact, ShrunkMCCover) and the chaining of the commutation with closed embeddings [Kol07, 108] (the sources of adapted charts, FlagCover). This module holds the data and the lemmas common to both:

• ShrunkEmbeddingCover M U: finitely many analytic open embeddings ιᵢ : Nᵢ → M with opens Vᵢ ⋐ range ιᵢ (compact closures inside the ranges) covering closure U;
• the coproduct sigma = ⨆ᵢ Nᵢ with the coproduct map desc = ⨆ᵢ ιᵢ (Kollár's g : X^* → X), a local analytic isomorphism and a coproduct of open embeddings;
• the open opens = ⨆ᵢ ιᵢ⁻¹(Vᵢ ∩ U) of the coproduct, with compact closure (isCompact_closure_opens, through the closed compact closedHull = ⨆ᵢ ιᵢ⁻¹(closure Vᵢ)) and image U (image_opens_eq);
• the restricted cover map coverMap : sigma.restrict opens → M.restrict U, a surjective local analytic isomorphism and a coproduct of open embeddings.

structure Hironaka.Manifold.ShrunkEmbeddingCover {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) (U : TopologicalSpace.Opens M.carrier) : Type (max (u + 1) u_1)

A shrunk embedding cover of the relatively compact open U of M — finitely many analytic open embeddings ιᵢ : Nᵢ → M with opens Vᵢ of M with compact closures inside the ranges of the ιᵢ, covering closure U.

• ι : Type u

  The (finite) index type of the pieces.

• finite : Finite self.ι
• N : self.ι → AnalyticManifold 𝕜 E

  The manifolds of the pieces.

• incl (i : self.ι) : AnalyticMap (self.N i) M

  The open embeddings of the pieces.

• isAnalyticOpenEmbedding_incl (i : self.ι) : Manifold.IsAnalyticOpenEmbedding (self.incl i)

  The maps ιᵢ are analytic open embeddings.

• V : self.ι → TopologicalSpace.Opens M.carrier

  The shrunk opens.

• hVc (i : self.ι) : IsCompact (closure ↑(self.V i))

  The shrunk opens have compact closures.

• hVr (i : self.ι) : closure ↑(self.V i) ⊆ Set.range ⇑(self.incl i)

  The closures of the shrunk opens lie in the ranges of the embeddings.

• hcov : closure ↑U ⊆ ⋃ (i : self.ι), ↑(self.V i)

  The shrunk opens cover closure U.

The coproduct of the pieces and its cover map

noncomputable def Hironaka.Manifold.ShrunkEmbeddingCover.sigma {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : AnalyticManifold 𝕜 E

The coproduct ⨆ᵢ Nᵢ of the pieces (Kollár's X^*).

Equations

• C.sigma = Manifold.sigmaManifold C.N

@[reducible, inline]

abbrev Hironaka.Manifold.ShrunkEmbeddingCover.desc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : AnalyticMap C.sigma M

The coproduct map ⨆ᵢ ιᵢ : ⨆ᵢ Nᵢ → M (Kollár's g : X^* → X).

Equations

• C.desc = Manifold.sigmaDescMap C.incl

theorem Hironaka.Manifold.ShrunkEmbeddingCover.desc_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) (p : C.sigma.carrier) : C.desc p = (C.incl p.fst) p.snd

theorem Hironaka.Manifold.ShrunkEmbeddingCover.isLocalDiffeomorph_desc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑C.desc

The coproduct map is a local analytic isomorphism.

theorem Hironaka.Manifold.ShrunkEmbeddingCover.isCoprodOfOpenEmbeddings_desc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : Manifold.IsCoprodOfOpenEmbeddings C.desc

The coproduct map is a coproduct of open embeddings.

def Hironaka.Manifold.ShrunkEmbeddingCover.opens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : TopologicalSpace.Opens C.sigma.carrier

The open ⨆ᵢ ιᵢ⁻¹(Vᵢ ∩ U) of the coproduct.

Equations

• C.opens = { carrier := {p : (i : C.ι) × (C.N i).carrier | (C.incl p.fst) p.snd ∈ ↑(C.V p.fst) ∩ ↑U}, is_open' := ⋯ }

theorem Hironaka.Manifold.ShrunkEmbeddingCover.mem_opens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) (p : C.sigma.carrier) : p ∈ ↑C.opens ↔ (C.incl p.fst) p.snd ∈ ↑(C.V p.fst) ∩ ↑U

def Hironaka.Manifold.ShrunkEmbeddingCover.closedHull {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : Set C.sigma.carrier

The closed set ⨆ᵢ ιᵢ⁻¹(closure Vᵢ) of the coproduct, which contains the closure of opens.

Equations

• C.closedHull = {p : (i : C.ι) × (C.N i).carrier | (C.incl p.fst) p.snd ∈ closure ↑(C.V p.fst)}

theorem Hironaka.Manifold.ShrunkEmbeddingCover.isClosed_closedHull {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : IsClosed C.closedHull

theorem Hironaka.Manifold.ShrunkEmbeddingCover.closedHull_eq_iUnion {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : C.closedHull = ⋃ (i : C.ι), ⇑(Manifold.sigmaMk C.N i) '' ⇑(C.incl i) ⁻¹' closure ↑(C.V i)

theorem Hironaka.Manifold.ShrunkEmbeddingCover.isCompact_closedHull {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : IsCompact C.closedHull

⨆ᵢ ιᵢ⁻¹(closure Vᵢ) is compact: finitely many pieces, each the preimage under an open embedding of a compact set inside its range.

theorem Hironaka.Manifold.ShrunkEmbeddingCover.closure_opens_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : closure ↑C.opens ⊆ C.closedHull

theorem Hironaka.Manifold.ShrunkEmbeddingCover.isCompact_closure_opens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : IsCompact (closure ↑C.opens)

The open ⨆ᵢ ιᵢ⁻¹(Vᵢ ∩ U) has compact closure (closure (Vᵢ ⊓ U) ⊆ closure Vᵢ, finitely many compact pieces).

theorem Hironaka.Manifold.ShrunkEmbeddingCover.image_opens_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : ⇑C.desc '' ↑C.opens ⊆ ↑U

The coproduct map sends ⨆ᵢ ιᵢ⁻¹(Vᵢ ∩ U) into U.

theorem Hironaka.Manifold.ShrunkEmbeddingCover.image_opens_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : ⇑C.desc '' ↑C.opens = ↑U

The coproduct map sends ⨆ᵢ ιᵢ⁻¹(Vᵢ ∩ U) onto U: the Vᵢ cover closure U ⊇ U and each lies in the range of ιᵢ.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.ShrunkEmbeddingCover.coverMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : AnalyticMap (C.sigma.restrict C.opens) (M.restrict U)

The cover map ⨆ᵢ ιᵢ⁻¹(Vᵢ ∩ U) → U, the restriction of the coproduct map (Kollár's g : X^* → X over U).

Equations

• C.coverMap = Hironaka.Manifold.AnalyticMap.restrictMap C.desc C.opens U ⋯

theorem Hironaka.Manifold.ShrunkEmbeddingCover.isLocalDiffeomorph_coverMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑C.coverMap

The cover map is a local analytic isomorphism.

theorem Hironaka.Manifold.ShrunkEmbeddingCover.surjective_coverMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : Function.Surjective ⇑C.coverMap

The cover map is surjective onto U.

theorem Hironaka.Manifold.ShrunkEmbeddingCover.isCoprodOfOpenEmbeddings_coverMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} (C : ShrunkEmbeddingCover M U) : Manifold.IsCoprodOfOpenEmbeddings C.coverMap

The cover map is a coproduct of open embeddings.