Maps out of the direct limit of a chain of analytic open embeddings

The universal property of the direct limit limitManifold of DirectLimit/Manifold.lean: a family of analytic maps f n : X n → Y compatible with the transition maps (f (n+1) ∘ ι n = f n) induces an analytic map limitDesc f hf : limitManifold → Y with limitDesc ∘ toLimit n = f n, Włodarczyk's glued map prin : M̃ → M [Wlo09, §4.1] for the blow-downs of the end results. When moreover the transition maps are the preimages of an increasing sequence of sets V n of Y (range (ι n) = f (n+1) ⁻¹' V n), the preimage of V n under the induced map is exactly the n-th piece (preimage_limitDesc_eq_range_toLimit: σ⁻¹(M_n) = M'_n), so the inclusion of the n-th piece is an analytic isomorphism onto limitDesc⁻¹(V n) (isAnalyticIsoOver_toLimitMap_limitDesc; the identification U_r = Ũ of [Wlo09, Theorem 2.0.3 (1)], the field toSpace_isIso of ExtensionCompatibleFamily).

The induced map is defined on the quotient (Quotient.lift), well defined because the family is compatible with the composites (apply_iter); it is analytic since on the image of the n-th piece it is f n ∘ (pieceOpenEmb n).symm (contMDiff_limitDescFun). For the preimage, a point toLimit m y with f m y ∈ V n and m > n descends step by step: f m y ∈ V (m-1) by monotonicity, so y = ι (m-1) y' with f (m-1) y' = f m y, and toLimit m y = toLimit (m-1) y' (toLimit_mem_range_of_apply_mem); conversely f n x ∈ V n since ι n x ∈ range (ι n) (apply_mem_of_range_eq; no separate hypothesis range (f n) ⊆ V n is needed).

• apply_iter, limitDescFun, limitDescFun_toLimit, contMDiff_limitDescFun, limitDesc, limitDesc_toLimit, limitDesc_comp_toLimitMap.
• apply_mem_of_range_eq, toLimit_mem_range_of_apply_mem, preimage_limitDesc_eq_range_toLimit, preimage_limitDesc_eq_range_toLimitMap, isAnalyticIsoOver_toLimitMap_limitDesc.

Maps out of the limit

theorem Manifold.OpenEmbeddingChain.apply_iter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {Y : AnalyticManifold 𝕜 E} (f : (n : ℕ) → AnalyticMap (c.X n) Y) (hf : ∀ (n : ℕ) (x : (c.X n).carrier), (f (n + 1)) ((c.ι n) x) = (f n) x) {n m : ℕ} (h : n ≤ m) (x : (c.X n).carrier) : (f m) ((c.iter h) x) = (f n) x

A family compatible with the transition maps is compatible with the composite embeddings.

def Manifold.OpenEmbeddingChain.limitDescFun {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {Y : AnalyticManifold 𝕜 E} (f : (n : ℕ) → AnalyticMap (c.X n) Y) (hf : ∀ (n : ℕ) (x : (c.X n).carrier), (f (n + 1)) ((c.ι n) x) = (f n) x) : c.Limit → Y.carrier

The underlying function of the map out of the limit induced by a compatible family: f n on the n-th piece (Quotient.lift); Włodarczyk's glued map, [Wlo09, §4.1].

Equations

• c.limitDescFun f hf = Quotient.lift (fun (a : (n : ℕ) × (c.X n).carrier) => (f a.fst) a.snd) ⋯

theorem Manifold.OpenEmbeddingChain.limitDescFun_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {Y : AnalyticManifold 𝕜 E} (f : (n : ℕ) → AnalyticMap (c.X n) Y) (hf : ∀ (n : ℕ) (x : (c.X n).carrier), (f (n + 1)) ((c.ι n) x) = (f n) x) (n : ℕ) (x : (c.X n).carrier) : c.limitDescFun f hf (c.toLimit n x) = (f n) x

The induced function restricts to f n on the n-th piece.

theorem Manifold.OpenEmbeddingChain.contMDiff_limitDescFun {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {Y : AnalyticManifold 𝕜 E} (f : (n : ℕ) → AnalyticMap (c.X n) Y) (hf : ∀ (n : ℕ) (x : (c.X n).carrier), (f (n + 1)) ((c.ι n) x) = (f n) x) : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (c.limitDescFun f hf)

The induced function is analytic — on the image of the n-th piece it is f n ∘ (pieceOpenEmb n).symm.

def Manifold.OpenEmbeddingChain.limitDesc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {Y : AnalyticManifold 𝕜 E} (f : (n : ℕ) → AnalyticMap (c.X n) Y) (hf : ∀ (n : ℕ) (x : (c.X n).carrier), (f (n + 1)) ((c.ι n) x) = (f n) x) : AnalyticMap c.limitManifold Y

The analytic map out of the limit induced by a family of analytic maps compatible with the transition maps (Włodarczyk's glued map prin : M̃ → M, [Wlo09, §4.1]).

Equations

• c.limitDesc f hf = ⟨c.limitDescFun f hf, ⋯⟩

theorem Manifold.OpenEmbeddingChain.limitDesc_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {Y : AnalyticManifold 𝕜 E} (f : (n : ℕ) → AnalyticMap (c.X n) Y) (hf : ∀ (n : ℕ) (x : (c.X n).carrier), (f (n + 1)) ((c.ι n) x) = (f n) x) (n : ℕ) (x : (c.X n).carrier) : (c.limitDesc f hf) (c.toLimit n x) = (f n) x

The induced map restricts to f n on the n-th piece.

theorem Manifold.OpenEmbeddingChain.limitDesc_comp_toLimitMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {Y : AnalyticManifold 𝕜 E} (f : (n : ℕ) → AnalyticMap (c.X n) Y) (hf : ∀ (n : ℕ) (x : (c.X n).carrier), (f (n + 1)) ((c.ι n) x) = (f n) x) (n : ℕ) : ContMDiffMap.comp (c.limitDesc f hf) (c.toLimitMap n) = f n

limitDesc f hf ∘ toLimitMap n = f n as analytic maps (the field map_toSpace of ExtensionCompatibleFamily).

The preimages of an increasing sequence of sets are the pieces

theorem Manifold.OpenEmbeddingChain.apply_mem_of_range_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {Y : AnalyticManifold 𝕜 E} (f : (n : ℕ) → AnalyticMap (c.X n) Y) (hf : ∀ (n : ℕ) (x : (c.X n).carrier), (f (n + 1)) ((c.ι n) x) = (f n) x) (V : ℕ → Set Y.carrier) (hι : ∀ (n : ℕ), Set.range ⇑(c.ι n) = ⇑(f (n + 1)) ⁻¹' V n) (n : ℕ) (x : (c.X n).carrier) : (f n) x ∈ V n

When the transition maps are the preimages of the sets V n, f n maps the n-th piece into V n (ι n x lies in the range of ι n); no separate hypothesis is needed.

theorem Manifold.OpenEmbeddingChain.toLimit_mem_range_of_apply_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {Y : AnalyticManifold 𝕜 E} (f : (n : ℕ) → AnalyticMap (c.X n) Y) (hf : ∀ (n : ℕ) (x : (c.X n).carrier), (f (n + 1)) ((c.ι n) x) = (f n) x) (V : ℕ → Set Y.carrier) (hV : ∀ (n : ℕ), V n ⊆ V (n + 1)) (hι : ∀ (n : ℕ), Set.range ⇑(c.ι n) = ⇑(f (n + 1)) ⁻¹' V n) {n m : ℕ} (y : (c.X m).carrier) (hy : (f m) y ∈ V n) : c.toLimit m y ∈ Set.range (c.toLimit n)

A point of the m-th piece mapped into V n lies in the image of the n-th piece — descend from m to n one transition map at a time (V increasing).

theorem Manifold.OpenEmbeddingChain.preimage_limitDesc_eq_range_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {Y : AnalyticManifold 𝕜 E} (f : (n : ℕ) → AnalyticMap (c.X n) Y) (hf : ∀ (n : ℕ) (x : (c.X n).carrier), (f (n + 1)) ((c.ι n) x) = (f n) x) (V : ℕ → Set Y.carrier) (hV : ∀ (n : ℕ), V n ⊆ V (n + 1)) (hι : ∀ (n : ℕ), Set.range ⇑(c.ι n) = ⇑(f (n + 1)) ⁻¹' V n) (n : ℕ) : ⇑(c.limitDesc f hf) ⁻¹' V n = Set.range (c.toLimit n)

When the transition maps are the preimages of an increasing sequence of sets V n, the preimage of V n under the induced map is the image of the n-th piece (σ⁻¹(M_n) = M'_n for the glued blow-down).

theorem Manifold.OpenEmbeddingChain.preimage_limitDesc_eq_range_toLimitMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {Y : AnalyticManifold 𝕜 E} (f : (n : ℕ) → AnalyticMap (c.X n) Y) (hf : ∀ (n : ℕ) (x : (c.X n).carrier), (f (n + 1)) ((c.ι n) x) = (f n) x) (V : ℕ → Set Y.carrier) (hV : ∀ (n : ℕ), V n ⊆ V (n + 1)) (hι : ∀ (n : ℕ), Set.range ⇑(c.ι n) = ⇑(f (n + 1)) ⁻¹' V n) (n : ℕ) : ⇑(c.limitDesc f hf) ⁻¹' V n = Set.range ⇑(c.toLimitMap n)

preimage_limitDesc_eq_range_toLimit with the range of the bundled inclusion (the form stated in the limit manifold's carrier, for rewriting).

theorem Manifold.OpenEmbeddingChain.isAnalyticIsoOver_toLimitMap_limitDesc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {Y : AnalyticManifold 𝕜 E} (f : (n : ℕ) → AnalyticMap (c.X n) Y) (hf : ∀ (n : ℕ) (x : (c.X n).carrier), (f (n + 1)) ((c.ι n) x) = (f n) x) (V : ℕ → Set Y.carrier) (hV : ∀ (n : ℕ), V n ⊆ V (n + 1)) (hι : ∀ (n : ℕ), Set.range ⇑(c.ι n) = ⇑(f (n + 1)) ⁻¹' V n) (n : ℕ) : (c.toLimitMap n).IsIsoOver (⇑(c.limitDesc f hf) ⁻¹' V n)

The inclusion of the n-th piece is an analytic isomorphism onto limitDesc⁻¹(V n) (the identification U_r = Ũ of [Wlo09, Theorem 2.0.3 (1)]; the field toSpace_isIso of ExtensionCompatibleFamily).