The direct limit of a chain of analytic open embeddings: the space

An ℕ-chain X 0 → X 1 → ⋯ of analytic manifolds along analytic open embeddings ι n : X n → X (n+1) (OpenEmbeddingChain), and its direct limit ⋃ₙ X n as a topological space: Włodarczyk's manifold obtained by gluing the pieces Ũ_i along their overlaps [Wlo09, §4.1], in the linear case of an exhaustion M_0 ⊆ M_1 ⊆ ⋯ (Kollár's remark that resolution on neighbourhoods of compact sets gives resolution of analytic spaces which are increasing unions of compact subsets [Kol07, 44]; [BM97, §13]). It is used by Hironaka/Resolution/Analytic/Functor/LimitFamily.lean for the end results of a compatible family along the embeddings of end results.

The limit is the quotient of the disjoint union Σ n, X n by the identification of two points that agree in a common later piece under the composite embeddings iter : X n → X m (n ≤ m), an equivalence relation because the composites are injective (LimitRel, setoid, Limit). Each piece maps in by toLimit n, injectively, with toLimit (n+1) ∘ ι n = toLimit n; the union of the images is everything. The quotient topology makes every toLimit n an open embedding: a set of X n is open in the limit iff its saturation meets every piece X m in an open set, and that trace is the preimage under iter : X m → X (max m n) of the image under iter : X n → X (max m n), open since the composites are open maps (preimage_toLimit_image, isOpenMap_toLimit, isOpenEmbedding_toLimit). The manifold structure is DirectLimit/Manifold.lean, the maps out of the limit DirectLimit/Cocone.lean.

• OpenEmbeddingChain, iter with iter_self, iter_succ, iter_trans, iter_injective, isLocalDiffeomorph_iter, isAnalyticOpenEmbedding_iter, isOpenEmbedding_iter.
• LimitRel, setoid, Limit, toLimit with toLimit_eq_iff_iter, toLimit_iter, toLimit_succ, toLimit_injective, toLimit_surjective, exists_common_toLimit, range_toLimit_mono, iUnion_range_toLimit.
• limitTopologicalSpace, continuous_toLimit, preimage_toLimit_image, isOpenMap_toLimit, isOpenEmbedding_toLimit, isOpen_range_toLimit.

The gluing is elementary and not in the sources in this form.

structure Manifold.OpenEmbeddingChain (𝕜 : Type) [RCLike 𝕜] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Type (max (u + 1) u_2)

An ℕ-chain of analytic manifolds X 0 → X 1 → ⋯ along analytic open embeddings: the end results of a compatible family along an exhaustion M_0 ⊆ M_1 ⊆ ⋯ with the embeddings of end results, abstractly ([Wlo09, §4.1]; [Kol07, 44]).

• X : ℕ → AnalyticManifold 𝕜 E

  The pieces.

• ι (n : ℕ) : AnalyticMap (self.X n) (self.X (n + 1))

  The transition maps.

• isAnalyticOpenEmbedding (n : ℕ) : IsAnalyticOpenEmbedding (self.ι n)

  Each transition map is an analytic open embedding.

The composite embeddings

def Manifold.OpenEmbeddingChain.iter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {n m : ℕ} : n ≤ m → AnalyticMap (c.X n) (c.X m)

The composite embedding X n → X m for n ≤ m, ι (m-1) ∘ ⋯ ∘ ι n (Nat.leRecOn).

Equations

• c.iter h = Nat.leRecOn h (fun {k : ℕ} (g : AnalyticMap (c.X n) (c.X k)) => ContMDiffMap.comp (c.ι k) g) ContMDiffMap.id

theorem Manifold.OpenEmbeddingChain.iter_self {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) : c.iter ⋯ = ContMDiffMap.id

The composite from a piece to itself is the identity.

theorem Manifold.OpenEmbeddingChain.iter_self_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) (h : n ≤ n) (x : (c.X n).carrier) : (c.iter h) x = x

iter_self, pointwise and for any proof of n ≤ n.

theorem Manifold.OpenEmbeddingChain.iter_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {n m : ℕ} (h : n ≤ m) (h' : n ≤ m + 1) : c.iter h' = ContMDiffMap.comp (c.ι m) (c.iter h)

The composite to m + 1 is ι m after the composite to m.

theorem Manifold.OpenEmbeddingChain.iter_succ_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {n m : ℕ} (h : n ≤ m) (h' : n ≤ m + 1) (x : (c.X n).carrier) : (c.iter h') x = (c.ι m) ((c.iter h) x)

iter_succ, pointwise.

theorem Manifold.OpenEmbeddingChain.iter_one_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) (h : n ≤ n + 1) (x : (c.X n).carrier) : (c.iter h) x = (c.ι n) x

The composite of one step is the transition map.

theorem Manifold.OpenEmbeddingChain.iter_trans {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {n m k : ℕ} (h₁ : n ≤ m) (h₂ : m ≤ k) (x : (c.X n).carrier) : (c.iter h₂) ((c.iter h₁) x) = (c.iter ⋯) x

The composites compose (functoriality of iter).

theorem Manifold.OpenEmbeddingChain.iter_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {n m : ℕ} (h : n ≤ m) : Function.Injective ⇑(c.iter h)

The composites are injective (each ι n is).

theorem Manifold.OpenEmbeddingChain.isLocalDiffeomorph_iter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {n m : ℕ} (h : n ≤ m) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(c.iter h)

The composites are local analytic isomorphisms (each ι n is; BlowUpSequence.isLocalDiffeomorph_comp).

theorem Manifold.OpenEmbeddingChain.isAnalyticOpenEmbedding_iter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {n m : ℕ} (h : n ≤ m) : IsAnalyticOpenEmbedding (c.iter h)

The composites are analytic open embeddings.

theorem Manifold.OpenEmbeddingChain.isOpenEmbedding_iter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {n m : ℕ} (h : n ≤ m) : Topology.IsOpenEmbedding ⇑(c.iter h)

The composites are topological open embeddings (a continuous injective open map).

The direct limit

def Manifold.OpenEmbeddingChain.LimitRel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (a b : (n : ℕ) × (c.X n).carrier) : Prop

Two points of pieces are identified when they agree in a common later piece (the gluing of the pieces along their overlaps, [Wlo09, §4.1]).

Equations

• c.LimitRel a b = ∃ (k : ℕ) (h₁ : a.fst ≤ k) (h₂ : b.fst ≤ k), (c.iter h₁) a.snd = (c.iter h₂) b.snd

theorem Manifold.OpenEmbeddingChain.LimitRel.iter_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {a b : (n : ℕ) × (c.X n).carrier} (hab : c.LimitRel a b) {k : ℕ} (h₁ : a.fst ≤ k) (h₂ : b.fst ≤ k) : (c.iter h₁) a.snd = (c.iter h₂) b.snd

Identified points agree in EVERY common later piece (injectivity of the composites at a piece above both).

theorem Manifold.OpenEmbeddingChain.limitRel_refl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (a : (n : ℕ) × (c.X n).carrier) : c.LimitRel a a

The identification is reflexive.

theorem Manifold.OpenEmbeddingChain.limitRel_symm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {a b : (n : ℕ) × (c.X n).carrier} (h : c.LimitRel a b) : c.LimitRel b a

The identification is symmetric.

theorem Manifold.OpenEmbeddingChain.limitRel_trans {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {a b d : (n : ℕ) × (c.X n).carrier} (hab : c.LimitRel a b) (hbd : c.LimitRel b d) : c.LimitRel a d

The identification is transitive (compare in a piece above both witnesses).

def Manifold.OpenEmbeddingChain.setoid {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) : Setoid ((n : ℕ) × (c.X n).carrier)

The identification of the pieces along the chain, as a setoid.

Equations

• c.setoid = { r := c.LimitRel, iseqv := ⋯ }

def Manifold.OpenEmbeddingChain.Limit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) : Type u

The direct limit ⋃ₙ X n: the pieces identified along the chain (Włodarczyk's glued manifold M̃, [Wlo09, §4.1]).

Equations

• c.Limit = Quotient c.setoid

def Manifold.OpenEmbeddingChain.toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) (x : (c.X n).carrier) : c.Limit

The inclusion of the n-th piece into the limit.

Equations

• c.toLimit n x = ⟦⟨n, x⟩⟧

theorem Manifold.OpenEmbeddingChain.toLimit_eq_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {n m : ℕ} {x : (c.X n).carrier} {y : (c.X m).carrier} : c.toLimit n x = c.toLimit m y ↔ c.LimitRel ⟨n, x⟩ ⟨m, y⟩

Two points of pieces have the same image iff they are identified.

theorem Manifold.OpenEmbeddingChain.toLimit_eq_iff_iter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {n m k : ℕ} (h₁ : n ≤ k) (h₂ : m ≤ k) {x : (c.X n).carrier} {y : (c.X m).carrier} : c.toLimit n x = c.toLimit m y ↔ (c.iter h₁) x = (c.iter h₂) y

Two points of pieces have the same image iff they agree in any given common later piece.

theorem Manifold.OpenEmbeddingChain.toLimit_iter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {n m : ℕ} (h : n ≤ m) (x : (c.X n).carrier) : c.toLimit m ((c.iter h) x) = c.toLimit n x

The inclusions are compatible with the composite embeddings.

theorem Manifold.OpenEmbeddingChain.toLimit_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) (x : (c.X n).carrier) : c.toLimit (n + 1) ((c.ι n) x) = c.toLimit n x

The inclusions are compatible with the transition maps, toLimit (n+1) ∘ ι n = toLimit n.

theorem Manifold.OpenEmbeddingChain.toLimit_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) : Function.Injective (c.toLimit n)

Each inclusion is injective.

theorem Manifold.OpenEmbeddingChain.toLimit_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (p : c.Limit) : ∃ (n : ℕ) (x : (c.X n).carrier), c.toLimit n x = p

Every point of the limit comes from some piece.

theorem Manifold.OpenEmbeddingChain.exists_common_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (p q : c.Limit) : ∃ (k : ℕ) (x : (c.X k).carrier) (y : (c.X k).carrier), c.toLimit k x = p ∧ c.toLimit k y = q

Two points of the limit come from a common piece.

theorem Manifold.OpenEmbeddingChain.range_toLimit_mono {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {n m : ℕ} (h : n ≤ m) : Set.range (c.toLimit n) ⊆ Set.range (c.toLimit m)

The images of the pieces increase.

theorem Manifold.OpenEmbeddingChain.iUnion_range_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) : ⋃ (n : ℕ), Set.range (c.toLimit n) = Set.univ

The images of the pieces cover the limit.

The topology of the limit

@[instance_reducible]

instance Manifold.OpenEmbeddingChain.limitTopologicalSpace {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) : TopologicalSpace c.Limit

The quotient topology on the limit.

Equations

• c.limitTopologicalSpace = { IsOpen := Manifold.OpenEmbeddingChain.limitTopologicalSpace._aux_1 c, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

theorem Manifold.OpenEmbeddingChain.continuous_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) : Continuous (c.toLimit n)

The inclusions are continuous.

theorem Manifold.OpenEmbeddingChain.preimage_toLimit_image {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n m : ℕ) (U : Set (c.X n).carrier) : Sigma.mk m ⁻¹' Quotient.mk c.setoid ⁻¹' c.toLimit n '' U = ⇑(c.iter ⋯) ⁻¹' ⇑(c.iter ⋯) '' U

The trace on the m-th piece of the saturation of a set U of the n-th piece — the preimage under X m → X (max m n) of the image of U under X n → X (max m n).

theorem Manifold.OpenEmbeddingChain.isOpenMap_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) : IsOpenMap (c.toLimit n)

The inclusions are open maps — the saturation of an open set meets every piece in an open set (preimage_toLimit_image, the composites being open embeddings).

theorem Manifold.OpenEmbeddingChain.isOpenEmbedding_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) : Topology.IsOpenEmbedding (c.toLimit n)

The inclusions are open embeddings.

theorem Manifold.OpenEmbeddingChain.isOpen_range_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) : IsOpen (Set.range (c.toLimit n))

The image of each piece is open in the limit.