From 3edf44c1809a6be356c81989a49bbb3c0c37ba88 Mon Sep 17 00:00:00 2001 From: LehengChen Date: Mon, 15 Jun 2026 16:44:10 +0800 Subject: [PATCH 1/2] port(charted-space-core): manifold structure from a ChartedSpaceCore Re-styled to OpenGA house style: architecture-layered module docstring, single-line Provenance footer, per-declaration single **Math.** docstrings (dropped **Eng.** segments). Theorem statements and proofs unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) --- OpenGALib/Manifold.lean | 1 + .../Manifold/Charts/ChartedSpaceCore.lean | 189 ++++++++++++++++++ 2 files changed, 190 insertions(+) create mode 100644 OpenGALib/Manifold/Charts/ChartedSpaceCore.lean diff --git a/OpenGALib/Manifold.lean b/OpenGALib/Manifold.lean index 3b671a6..f6d6a4c 100644 --- a/OpenGALib/Manifold.lean +++ b/OpenGALib/Manifold.lean @@ -1,3 +1,4 @@ +import OpenGALib.Manifold.Charts.ChartedSpaceCore import OpenGALib.Manifold.Charts.CoordinateBall import OpenGALib.Manifold.Charts.PrecompactBasis diff --git a/OpenGALib/Manifold/Charts/ChartedSpaceCore.lean b/OpenGALib/Manifold/Charts/ChartedSpaceCore.lean new file mode 100644 index 0000000..94a3afb --- /dev/null +++ b/OpenGALib/Manifold/Charts/ChartedSpaceCore.lean @@ -0,0 +1,189 @@ +import Mathlib.Geometry.Manifold.ChartedSpace +import Mathlib.Geometry.Manifold.IsManifold.Basic +import Mathlib.Geometry.Manifold.Instances.Real +import Mathlib.Topology.Bases + +/-! +# Manifold structure from a chart-family core + +Mathlib's `ChartedSpaceCore` is the model-agnostic input: a bare family of +charts plus the compatibility data that *generates* a topology on the +underlying set. This module is the reusable bridge that turns such a core +into a usable manifold, isolating each structural property behind a separate +hypothesis so downstream code assumes only what it needs: + +1. **Separation** — the generated topology is Hausdorff once distinct points + can be told apart by a shared chart or by disjoint chart domains. +2. **Countability** — it is second-countable once a countable subatlas + covers the space, each chart domain inheriting second countability from + the model space. +3. **Smooth structure** — smooth coordinate changes upgrade the charted + space to a smooth manifold for any chosen model with corners. +4. **Uniqueness** — the generated topology is the only one realizing the + chart family as a charted space, pinning the construction down. + +Layers 1–3 are the constructive payload consumed by manifold builders; +layer 4 is the characterization that makes the construction canonical. + +## Main results + +* `Manifold.toTopologicalSpace_t2Space` — the generated topology is Hausdorff + under a chart-separation hypothesis. +* `Manifold.toTopologicalSpace_secondCountableTopology` — the generated topology + is second-countable when a countable subatlas covers the space. +* `Manifold.toChartedSpace_isManifold` — smooth coordinate changes make the + charted space a smooth manifold. +* `Manifold.eq_toTopologicalSpace_of_chartedSpace` — the generated topology is the + unique one realizing the chart family as a charted space. + +Provenance: SmoothManifoldsLee a5f308c — Lemma_1_35. +-/ + +open scoped Manifold ContDiff + +universe u + +namespace Manifold + +variable {M : Type u} {H : Type*} [TopologicalSpace H] + +/-- **Math.** Lemma 1.35 (2): the topology generated by a chart family is Hausdorff +whenever any two distinct points are separated either by a common chart (both lie in +the source of one chart) or by disjoint chart domains. -/ +theorem toTopologicalSpace_t2Space + [T2Space H] (c : ChartedSpaceCore H M) + (hseparation : + ∀ ⦃p q : M⦄, p ≠ q → + (∃ e ∈ c.atlas, p ∈ e.source ∧ q ∈ e.source) ∨ + ∃ e ∈ c.atlas, ∃ e' ∈ c.atlas, + Disjoint e.source e'.source ∧ p ∈ e.source ∧ q ∈ e'.source) : + letI : TopologicalSpace M := c.toTopologicalSpace + T2Space M := by + letI : TopologicalSpace M := c.toTopologicalSpace + refine ⟨fun p q hpq ↦ ?_⟩ + rcases hseparation hpq with hcommon | hdisjoint + · rcases hcommon with ⟨e, he, hp, hq⟩ + -- Pull apart `p` and `q` inside a common chart using Hausdorffness of the model space. + have hepq : e p ≠ e q := fun hEq ↦ hpq <| e.injOn hp hq hEq + rcases t2_separation hepq with ⟨u, v, hu, hv, hpu, hqv, huv⟩ + refine ⟨e ⁻¹' u ∩ e.source, e ⁻¹' v ∩ e.source, ?_, ?_, ?_, ?_, ?_⟩ + · -- Basic chart preimages generate the topology by construction. + apply TopologicalSpace.GenerateOpen.basic + simp only [exists_prop, Set.mem_iUnion, Set.mem_singleton_iff] + exact ⟨e, he, u, hu, rfl⟩ + · -- The same basic-open argument works for the second neighborhood. + apply TopologicalSpace.GenerateOpen.basic + simp only [exists_prop, Set.mem_iUnion, Set.mem_singleton_iff] + exact ⟨e, he, v, hv, rfl⟩ + · exact ⟨hpu, hp⟩ + · exact ⟨hqv, hq⟩ + · -- Disjointness is preserved under preimage, and intersecting with the common source keeps it. + exact (Disjoint.preimage e huv).mono Set.inter_subset_left Set.inter_subset_left + · rcases hdisjoint with ⟨e, he, e', he', hsource, hp, hq⟩ + -- In the disjoint-chart case the chart domains themselves give the separation. + exact ⟨e.source, e'.source, c.open_source' he, c.open_source' he', hp, hq, hsource⟩ + +/-- **Math.** Lemma 1.35 (3): the topology generated by a chart family is +second-countable whenever a countable subfamily of chart domains covers the space. -/ +theorem toTopologicalSpace_secondCountableTopology + [SecondCountableTopology H] (c : ChartedSpaceCore H M) + (hcountable_cover : + ∃ s : Set (PartialEquiv M H), + s.Countable ∧ s ⊆ c.atlas ∧ ⋃ e ∈ s, e.source = Set.univ) : + letI : TopologicalSpace M := c.toTopologicalSpace + SecondCountableTopology M := by + letI : TopologicalSpace M := c.toTopologicalSpace + rcases hcountable_cover with ⟨s, hs_countable, hs_subset, hs_cover⟩ + haveI : Countable s := hs_countable.to_subtype + let U : s → Set M := fun e ↦ e.1.source + have hU_open : ∀ e : s, IsOpen (U e) := fun e ↦ c.open_source' (hs_subset e.2) + haveI : ∀ e : s, SecondCountableTopology (U e) := fun e ↦ by + -- Each chart domain is homeomorphic to an open subset of the second-countable model space. + simpa [U] using (c.openPartialHomeomorph e.1 (hs_subset e.2)).secondCountableTopology_source + have hU_cover : ⋃ e : s, U e = Set.univ := by + -- Reindex the given countable subatlas cover by the subtype of atlas elements in `s`. + simpa [U, Set.iUnion_subtype] using hs_cover + -- Exercise A.22 appears here as the standard theorem that a countable open cover by + -- second-countable subspaces yields a second-countable ambient topology. + exact TopologicalSpace.secondCountableTopology_of_countable_cover hU_open hU_cover + +/-- **Math.** Lemma 1.35 (4): a chart family whose coordinate changes are smooth with +respect to a model with corners `I` defines a smooth manifold structure on the +generated topology `c.toTopologicalSpace`. -/ +theorem toChartedSpace_isManifold + {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] + [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (c : ChartedSpaceCore H M) + (hsmooth : + ∀ e e' : PartialEquiv M H, + e ∈ c.atlas → e' ∈ c.atlas → + ContDiffOn 𝕜 ∞ (I ∘ e.symm.trans e' ∘ I.symm) + (I.symm ⁻¹' (e.symm.trans e').source ∩ Set.range I)) : + letI : TopologicalSpace M := c.toTopologicalSpace + letI : ChartedSpace H M := c.toChartedSpace + IsManifold I ∞ M := by + letI : TopologicalSpace M := c.toTopologicalSpace + letI : ChartedSpace H M := c.toChartedSpace + -- The constructed atlas is the original chart family, now as open partial homeomorphisms. + refine isManifold_of_contDiffOn I ∞ M ?_ + intro e e' he he' + rcases he with ⟨f, hf, hef⟩ + rcases hf with ⟨g, rfl⟩ + simp only [Set.mem_iUnion, Set.mem_singleton_iff] at hef + rcases hef with ⟨hg, rfl⟩ + rcases he' with ⟨f', hf', he'f'⟩ + rcases hf' with ⟨g', rfl⟩ + simp only [Set.mem_iUnion, Set.mem_singleton_iff] at he'f' + rcases he'f' with ⟨hg', rfl⟩ + -- After unpacking atlas membership, the required transition map is the original `PartialEquiv` + -- transition, so the hypothesis applies verbatim. + simpa using hsmooth g g' hg hg' + +/-- **Math.** Lemma 1.35 (1): a topology that turns the chart family of `c` into the +expected charted-space structure is forced to coincide with `c.toTopologicalSpace`. -/ +theorem eq_toTopologicalSpace_of_chartedSpace + (c : ChartedSpaceCore H M) [t : TopologicalSpace M] [ChartedSpace H M] + (hchartAt : + ∀ x : M, (_root_.chartAt H x).toPartialEquiv = c.chartAt x) + (hatlas : + ∀ e ∈ c.atlas, + ∃ e' : OpenPartialHomeomorph M H, e'.toPartialEquiv = e) : + t = c.toTopologicalSpace := by + have hchartAt_coe : + ∀ x : M, + (_root_.chartAt H x : M → H) = + c.chartAt x := fun x ↦ by + simpa using + congrArg + (fun e : PartialEquiv M H ↦ (e : M → H)) + (hchartAt x) + refine TopologicalSpace.ext_iff.mpr ?_ + intro s + constructor + · intro hs + have ht : + @IsOpen M t s ↔ + ∀ x : M, IsOpen ((c.chartAt x) '' ((c.chartAt x).source ∩ s)) := by + simpa [hchartAt, hchartAt_coe] using + ChartedSpace.isOpen_iff H s + letI : TopologicalSpace M := c.toTopologicalSpace + letI : ChartedSpace H M := c.toChartedSpace + have hc_chartAt_coe : + ∀ x : M, + (_root_.chartAt H x : M → H) = c.chartAt x := fun x ↦ rfl + have hc : + @IsOpen M c.toTopologicalSpace s ↔ + ∀ x : M, IsOpen ((c.chartAt x) '' ((c.chartAt x).source ∩ s)) := by + simpa [hc_chartAt_coe] using + ChartedSpace.isOpen_iff H s + exact hc.2 (ht.1 hs) + · intro hs + have ht : t ≤ c.toTopologicalSpace := by + rw [ChartedSpaceCore.toTopologicalSpace, TopologicalSpace.le_generateFrom_iff_subset_isOpen] + intro u hu + simp only [Set.mem_iUnion, exists_prop, Set.mem_singleton_iff] at hu + rcases hu with ⟨e, he, s, hs, rfl⟩ + rcases hatlas e he with ⟨e', rfl⟩ + simpa [Set.inter_comm] using e'.continuousOn.isOpen_inter_preimage e'.open_source hs + exact ht s hs + +end Manifold From e3c1f7588e2ba26f2448c4bb392430195a05b91e Mon Sep 17 00:00:00 2001 From: LehengChen Date: Mon, 15 Jun 2026 20:36:19 +0800 Subject: [PATCH 2/2] docs: state ChartedSpaceCore lemmas natively (drop textbook numbering) --- OpenGALib/Manifold/Charts/ChartedSpaceCore.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/OpenGALib/Manifold/Charts/ChartedSpaceCore.lean b/OpenGALib/Manifold/Charts/ChartedSpaceCore.lean index 94a3afb..ba65d3d 100644 --- a/OpenGALib/Manifold/Charts/ChartedSpaceCore.lean +++ b/OpenGALib/Manifold/Charts/ChartedSpaceCore.lean @@ -47,7 +47,7 @@ namespace Manifold variable {M : Type u} {H : Type*} [TopologicalSpace H] -/-- **Math.** Lemma 1.35 (2): the topology generated by a chart family is Hausdorff +/-- **Math.** The topology generated by a chart family is Hausdorff whenever any two distinct points are separated either by a common chart (both lie in the source of one chart) or by disjoint chart domains. -/ theorem toTopologicalSpace_t2Space @@ -83,7 +83,7 @@ theorem toTopologicalSpace_t2Space -- In the disjoint-chart case the chart domains themselves give the separation. exact ⟨e.source, e'.source, c.open_source' he, c.open_source' he', hp, hq, hsource⟩ -/-- **Math.** Lemma 1.35 (3): the topology generated by a chart family is +/-- **Math.** The topology generated by a chart family is second-countable whenever a countable subfamily of chart domains covers the space. -/ theorem toTopologicalSpace_secondCountableTopology [SecondCountableTopology H] (c : ChartedSpaceCore H M) @@ -107,7 +107,7 @@ theorem toTopologicalSpace_secondCountableTopology -- second-countable subspaces yields a second-countable ambient topology. exact TopologicalSpace.secondCountableTopology_of_countable_cover hU_open hU_cover -/-- **Math.** Lemma 1.35 (4): a chart family whose coordinate changes are smooth with +/-- **Math.** A chart family whose coordinate changes are smooth with respect to a model with corners `I` defines a smooth manifold structure on the generated topology `c.toTopologicalSpace`. -/ theorem toChartedSpace_isManifold @@ -138,7 +138,7 @@ theorem toChartedSpace_isManifold -- transition, so the hypothesis applies verbatim. simpa using hsmooth g g' hg hg' -/-- **Math.** Lemma 1.35 (1): a topology that turns the chart family of `c` into the +/-- **Math.** A topology that turns the chart family of `c` into the expected charted-space structure is forced to coincide with `c.toTopologicalSpace`. -/ theorem eq_toTopologicalSpace_of_chartedSpace (c : ChartedSpaceCore H M) [t : TopologicalSpace M] [ChartedSpace H M]