port(charted-space-core): 由图册核造流形（ChartedSpaceCore）

OpenGALib/Manifold.lean

@@ -1,3 +1,4 @@
+import OpenGALib.Manifold.Charts.ChartedSpaceCore
 import OpenGALib.Manifold.Charts.CoordinateBall
 import OpenGALib.Manifold.Charts.PrecompactBasis
 

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.** 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.** 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.** 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.** 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