Charted-space kit: build ChartedSpace ℂ Z + IsManifold 𝓘(ℂ) ω Z from a chart family

Unit: surfaces-and-charts (docs/design/surfaces-and-charts.md §3.3).

Toolkit for projective-line (CC5: two charts on OnePoint ℂ) and jacobian-construction (CC9: quotient charts on ℂ ⧸ Λ):

• chartedSpaceOfFamily: package a covering family c : ι → OpenPartialHomeomorph Z ℂ as a ChartedSpace ℂ Z (with @[simp] lemmas for its atlas/chartAt);
• isManifold_of_analyticOn_transitions: an atlas with ℂ-analytic transition maps is an ω-manifold;
• isManifold_of_family: family version — pairwise-analytic transitions of the generating family suffice.

This file is standalone (it does not assume a pre-existing surface).

@[reducible]

def RS.chartedSpaceOfFamily {Z : Type u_1} [TopologicalSpace Z] {ι : Type u_2} (c : ι → OpenPartialHomeomorph Z ℂ) (idx : Z → ι) (h : ∀ (z : Z), z ∈ (c (idx z)).source) : ChartedSpace ℂ Z

Package a covering family of ℂ-charts as a ChartedSpace.

Equations

• RS.chartedSpaceOfFamily c idx h = { atlas := Set.range c, chartAt := fun (z : Z) => c (idx z), mem_chart_source := h, chart_mem_atlas := ⋯ }

@[simp]

theorem RS.chartedSpaceOfFamily_chartAt {Z : Type u_1} [TopologicalSpace Z] {ι : Type u_2} (c : ι → OpenPartialHomeomorph Z ℂ) (idx : Z → ι) (h : ∀ (z : Z), z ∈ (c (idx z)).source) (z : Z) : chartAt ℂ z = c (idx z)

@[simp]

theorem RS.chartedSpaceOfFamily_atlas {Z : Type u_1} [TopologicalSpace Z] {ι : Type u_2} (c : ι → OpenPartialHomeomorph Z ℂ) (idx : Z → ι) (h : ∀ (z : Z), z ∈ (c (idx z)).source) : atlas ℂ Z = Set.range c

theorem RS.isManifold_of_analyticOn_transitions {Z : Type u_1} [TopologicalSpace Z] [ChartedSpace ℂ Z] (h : ∀ e ∈ atlas ℂ Z, ∀ e' ∈ atlas ℂ Z, AnalyticOnNhd ℂ (↑(e.symm.trans e')) (e.symm.trans e').source) : IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Z

An atlas with ℂ-analytic transition maps is an ω-manifold.

theorem RS.isManifold_of_family {Z : Type u_1} [TopologicalSpace Z] {ι : Type u_2} (c : ι → OpenPartialHomeomorph Z ℂ) (idx : Z → ι) (h : ∀ (z : Z), z ∈ (c (idx z)).source) (htrans : ∀ (i j : ι), AnalyticOnNhd ℂ (↑((c i).symm.trans (c j))) ((c i).symm.trans (c j)).source) : IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Z

Family version: pairwise-analytic transitions of the generating family suffice.