The direct limit of a chain of open embeddings: the manifold

The direct limit Limit of DirectLimit/Chain.lean is an analytic manifold, and the inclusions of the pieces are analytic open embeddings: limitManifold : AnalyticManifold 𝕜 E with its IsManifold, T2Space and SecondCountableTopology instances, Włodarczyk's glued manifold M̃ [Wlo09, §4.1] (the increasing union of compact subsets of [Kol07, 44]; [BM97, §13]).

Hausdorff: two points lie in a common piece (exists_common_toLimit), separated there, and the inclusion is an open map. Second countable: the pieces' images are an open countable cover by second countable subspaces (secondCountableTopology_of_countable_cover). Charts: for a nonempty piece X n the inclusion is an open partial homeomorphism pieceOpenEmb n (IsOpenEmbedding.toOpenPartialHomeomorph, the pattern of BlowUp/GluedCharts.lean), and every chart φ of X n gives the chart limitChart n φ := (pieceOpenEmb n).symm ≫ₕ φ of the limit; the atlas is all of them. The chart change between a chart from X n and one from X m is ψ ∘ transition n m ∘ φ.symm with transition n m : X n ⊇ toLimit n ⁻¹' range (toLimit m) → X m the transition through the limit ((pieceOpenEmb m).symm ∘ toLimit n), and transition is analytic: at a point x with local inverse Φ of the composite embedding X m → X (max n m) at transition n m x (isLocalDiffeomorph_iter), transition n m = Φ.symm ∘ iter (n ≤ max n m) near x. This is where Włodarczyk's canonicity supplies the identifications of the pieces on their overlaps [Wlo09, §4.1], here read through the composites (contMDiffOn_transition, limitIsManifold by isManifold_of_contDiffOn). The inclusions are then analytic (toLimit n = (limitChart n (chartAt x)).symm ∘ chartAt x near x) and local analytic isomorphisms (pieceDiffeomorph), hence analytic open embeddings onto their open images (isAnalyticOpenEmbedding_toLimitMap, isAnalyticIsoOver_toLimitMap).

• limitT2Space, limitSecondCountableTopology.
• pieceOpenEmb, repIdx, rep, limitChart, limitChartedSpace, mem_atlas_limit_iff, limitChart_mem_atlas.
• transition, contMDiffOn_transition, mem_source_trans_limitChart, limitIsManifold.
• limitManifold, contMDiff_toLimit, toLimitMap, pieceDiffeomorph, isLocalDiffeomorph_toLimit, isAnalyticOpenEmbedding_toLimitMap, isAnalyticIsoOver_toLimitMap.

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

Hausdorff and second countable

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

The limit is Hausdorff — two points lie in a common piece, are separated there, and the inclusion is an open injective map.

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

The limit is second countable — a countable open cover by the images of the pieces, each homeomorphic to a second countable manifold.

The charts of the limit

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

The inclusion of a nonempty piece as an open partial homeomorphism (source the whole piece, target its image).

Equations

• c.pieceOpenEmb n = Topology.IsOpenEmbedding.toOpenPartialHomeomorph (c.toLimit n) ⋯

theorem Manifold.OpenEmbeddingChain.pieceOpenEmb_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] (x : (c.X n).carrier) : ↑(c.pieceOpenEmb n) x = c.toLimit n x

pieceOpenEmb is the inclusion.

theorem Manifold.OpenEmbeddingChain.pieceOpenEmb_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] : (c.pieceOpenEmb n).source = Set.univ

The source of pieceOpenEmb is the whole piece.

theorem Manifold.OpenEmbeddingChain.pieceOpenEmb_target {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] : (c.pieceOpenEmb n).target = Set.range (c.toLimit n)

The target of pieceOpenEmb is the image of the piece.

theorem Manifold.OpenEmbeddingChain.pieceOpenEmb_symm_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] (x : (c.X n).carrier) : ↑(c.pieceOpenEmb n).symm (c.toLimit n x) = x

The inverse of pieceOpenEmb undoes the inclusion.

theorem Manifold.OpenEmbeddingChain.toLimit_pieceOpenEmb_symm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] {p : c.Limit} (hp : p ∈ Set.range (c.toLimit n)) : c.toLimit n (↑(c.pieceOpenEmb n).symm p) = p

The inclusion undoes the inverse of pieceOpenEmb on the image of the piece.

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

A piece containing a given point of the limit (chosen).

Equations

• c.repIdx p = ⋯.choose

noncomputable def Manifold.OpenEmbeddingChain.rep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (p : c.Limit) : (c.X (c.repIdx p)).carrier

The point of the piece repIdx p over p (chosen).

Equations

• c.rep p = ⋯.choose

theorem Manifold.OpenEmbeddingChain.toLimit_rep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (p : c.Limit) : c.toLimit (c.repIdx p) (c.rep p) = p

rep p lies over p.

theorem Manifold.OpenEmbeddingChain.nonempty_repIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (p : c.Limit) : Nonempty (c.X (c.repIdx p)).carrier

The piece repIdx p is nonempty.

noncomputable def Manifold.OpenEmbeddingChain.limitChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] (φ : OpenPartialHomeomorph (c.X n).carrier E) : OpenPartialHomeomorph c.Limit E

The chart of the limit over a nonempty piece obtained from a chart φ of the piece — the inverse of the piece's inclusion followed by φ.

Equations

• c.limitChart n φ = (c.pieceOpenEmb n).symm.trans φ

theorem Manifold.OpenEmbeddingChain.limitChart_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] (φ : OpenPartialHomeomorph (c.X n).carrier E) : (c.limitChart n φ).source = Set.range (c.toLimit n) ∩ ↑(c.pieceOpenEmb n).symm ⁻¹' φ.source

The source of limitChart n φ — the points of the image of the piece whose representative lies in φ's source.

theorem Manifold.OpenEmbeddingChain.limitChart_target {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] (φ : OpenPartialHomeomorph (c.X n).carrier E) : (c.limitChart n φ).target = φ.target

The target of limitChart n φ is the target of φ.

theorem Manifold.OpenEmbeddingChain.limitChart_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] (φ : OpenPartialHomeomorph (c.X n).carrier E) (p : c.Limit) : ↑(c.limitChart n φ) p = ↑φ (↑(c.pieceOpenEmb n).symm p)

limitChart n φ reads φ at the representative in the piece.

theorem Manifold.OpenEmbeddingChain.limitChart_symm_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] (φ : OpenPartialHomeomorph (c.X n).carrier E) (v : E) : ↑(c.limitChart n φ).symm v = c.toLimit n (↑φ.symm v)

The inverse of limitChart n φ is the inclusion after the inverse of φ.

theorem Manifold.OpenEmbeddingChain.pieceOpenEmb_symm_rep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (p : c.Limit) : ↑(c.pieceOpenEmb (c.repIdx p)).symm p = c.rep p

The inverse of the inclusion of the piece repIdx p sends p to rep p.

@[instance_reducible]

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

The charted-space structure of the limit — the charts limitChart n φ of the nonempty pieces' charts; the chart at p is the one from chartAt (rep p).

Equations

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

theorem Manifold.OpenEmbeddingChain.mem_atlas_limit_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) {Φ : OpenPartialHomeomorph c.Limit E} : Φ ∈ atlas E c.Limit ↔ ∃ (n : ℕ) (x : Nonempty (c.X n).carrier), ∃ φ ∈ atlas E (c.X n).carrier, Φ = c.limitChart n φ

The atlas of the limit consists of the charts limitChart n φ of the nonempty pieces' charts.

theorem Manifold.OpenEmbeddingChain.limitChart_mem_atlas {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] {φ : OpenPartialHomeomorph (c.X n).carrier E} (hφ : φ ∈ atlas E (c.X n).carrier) : c.limitChart n φ ∈ atlas E c.Limit

Each limitChart n φ of a chart φ of a nonempty piece lies in the atlas.

The transition between two pieces is analytic

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

The transition X n ⊇ toLimit n ⁻¹' range (toLimit m) → X m through the limit, (pieceOpenEmb m).symm ∘ toLimit n (defined everywhere, meaningful on the domain).

Equations

• c.transition n m x = ↑(c.pieceOpenEmb m).symm (c.toLimit n x)

theorem Manifold.OpenEmbeddingChain.toLimit_transition {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n m : ℕ) [Nonempty (c.X m).carrier] {x : (c.X n).carrier} (hx : c.toLimit n x ∈ Set.range (c.toLimit m)) : c.toLimit m (c.transition n m x) = c.toLimit n x

The transition is over the limit.

theorem Manifold.OpenEmbeddingChain.iter_transition {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n m : ℕ) [Nonempty (c.X m).carrier] {x : (c.X n).carrier} (hx : c.toLimit n x ∈ Set.range (c.toLimit m)) : (c.iter ⋯) (c.transition n m x) = (c.iter ⋯) x

The transition agrees with the composites in the piece max n m.

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

The domain of the transition is open.

theorem Manifold.OpenEmbeddingChain.continuousOn_transition {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n m : ℕ) [Nonempty (c.X m).carrier] : ContinuousOn (c.transition n m) (c.toLimit n ⁻¹' Set.range (c.toLimit m))

The transition is continuous on its domain.

theorem Manifold.OpenEmbeddingChain.contMDiffOn_transition {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n m : ℕ) [Nonempty (c.X m).carrier] : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (c.transition n m) (c.toLimit n ⁻¹' Set.range (c.toLimit m))

The transition is analytic on its domain: near x it is Φ.symm ∘ iter, Φ a local inverse of the composite embedding X m → X (max n m) at transition n m x (Włodarczyk's identifications of the pieces on their overlaps by canonicity, [Wlo09, §4.1], read through the composites).

The limit is an analytic manifold

theorem Manifold.OpenEmbeddingChain.mem_source_trans_limitChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n m : ℕ) [Nonempty (c.X n).carrier] [Nonempty (c.X m).carrier] (φ : OpenPartialHomeomorph (c.X n).carrier E) (ψ : OpenPartialHomeomorph (c.X m).carrier E) {v : E} (hv : v ∈ ((c.limitChart n φ).symm.trans (c.limitChart m ψ)).source) : v ∈ φ.target ∧ ↑φ.symm v ∈ c.toLimit n ⁻¹' Set.range (c.toLimit m) ∩ φ.source ∩ c.transition n m ⁻¹' ψ.source

A point v of the source of the chart change from limitChart n φ to limitChart m ψ lies in φ's target, and φ.symm v in the transition's domain, in φ's source and over ψ's source.

instance Manifold.OpenEmbeddingChain.limitIsManifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) : IsManifold (modelWithCornersSelf 𝕜 E) ⊤ c.Limit

The limit is an analytic manifold — its chart changes are the transitions read in the pieces' charts (ψ ∘ transition n m ∘ φ.symm), analytic by contMDiffOn_transition (isManifold_of_contDiffOn, contMDiffOn_iff_of_mem_maximalAtlas').

noncomputable def Manifold.OpenEmbeddingChain.limitManifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) : AnalyticManifold 𝕜 E

The direct limit as a bundled analytic manifold (Włodarczyk's glued manifold M̃, Wlo09, §4.1).

Equations

• c.limitManifold = { carrier := c.Limit, top := c.limitTopologicalSpace, charted := c.limitChartedSpace, manifold := ⋯, t2 := ⋯, secondCountable := ⋯ }

The inclusions of the pieces are analytic open embeddings

theorem Manifold.OpenEmbeddingChain.contMDiffOn_pieceOpenEmb_symm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (↑(c.pieceOpenEmb n).symm) (Set.range (c.toLimit n))

The inverse of a piece's inclusion is analytic on the image of the piece — near toLimit n y it is (chartAt y).symm ∘ limitChart n (chartAt y).

theorem Manifold.OpenEmbeddingChain.contMDiff_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (c.toLimit n)

Each inclusion is analytic — near x it is (limitChart n (chartAt x)).symm ∘ chartAt x.

def Manifold.OpenEmbeddingChain.toLimitMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) : AnalyticMap (c.X n) c.limitManifold

The inclusion of a piece as an analytic map into the limit manifold.

Equations

• c.toLimitMap n = ⟨c.toLimit n, ⋯⟩

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

toLimitMap is the inclusion.

noncomputable def Manifold.OpenEmbeddingChain.pieceDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) [Nonempty (c.X n).carrier] : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (c.X n).carrier c.Limit ⊤

The inclusion of a nonempty piece as a partial diffeomorphism onto its (open) image.

Equations

• c.pieceDiffeomorph n = { toPartialEquiv := (c.pieceOpenEmb n).toPartialEquiv, open_source := ⋯, open_target := ⋯, contMDiffOn_toFun := ⋯, contMDiffOn_invFun := ⋯ }

theorem Manifold.OpenEmbeddingChain.isLocalDiffeomorph_toLimit {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (c.toLimit n)

Each inclusion is a local analytic isomorphism (pieceDiffeomorph at every point).

theorem Manifold.OpenEmbeddingChain.isAnalyticOpenEmbedding_toLimitMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) : IsAnalyticOpenEmbedding (c.toLimitMap n)

Each inclusion is an analytic open embedding (Włodarczyk's open embeddings of desingularizations along open embeddings, [Wlo09, §4]).

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

The range of toLimitMap n is the image of the piece.

theorem Manifold.OpenEmbeddingChain.isAnalyticIsoOver_toLimitMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : OpenEmbeddingChain 𝕜 E) (n : ℕ) : (c.toLimitMap n).IsIsoOver (Set.range ⇑(c.toLimitMap n))

Each inclusion is an analytic isomorphism onto its open image (the identification U_r = Ũ of [Wlo09, Theorem 2.0.3 (1)]; the field toSpace_isIso of ExtensionCompatibleFamily).