Charted-space kit, generalized to an arbitrary NormedSpace ℂ codomain

Unit: jacobian-construction (docs/design/jacobian-construction.md §4.2.1). Surface's Jacobian/Surface/ChartedSpaceKit.lean hardcodes the chart codomain to literal ℂ; this file is a textually near-identical generalization to an arbitrary {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] (needed for V := Fin n → ℂ, the ambient space of the Jacobian torus). A non-blocking request to generalize the upstream file instead is filed in docs/requests/surfaces-and-charts.md; the two are rfl-compatible (identical proofs).

Namespace RS (Compat section, primed names to avoid clashing with Surface's originals):

• chartedSpaceOfFamily': package a covering family c : ι → OpenPartialHomeomorph Z E as a ChartedSpace E Z;
• isManifold_of_analyticOn_transitions': an atlas with ℂ-analytic transition maps is an ω-manifold (model 𝓘(ℂ, E));
• isManifold_of_family': family version.

@[reducible]

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

Package a covering family of E-valued 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} {E : Type u_3} [NormedAddCommGroup E] (c : ι → OpenPartialHomeomorph Z E) (idx : Z → ι) (h : ∀ (z : Z), z ∈ (c (idx z)).source) (z : Z) : chartAt E z = c (idx z)

@[simp]

theorem RS.chartedSpaceOfFamily'_atlas {Z : Type u_1} [TopologicalSpace Z] {ι : Type u_2} {E : Type u_3} [NormedAddCommGroup E] (c : ι → OpenPartialHomeomorph Z E) (idx : Z → ι) (h : ∀ (z : Z), z ∈ (c (idx z)).source) : atlas E Z = Set.range c

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

An atlas with ℂ-analytic transition maps is an ω-manifold (model 𝓘(ℂ, E)).

theorem RS.isManifold_of_family' {Z : Type u_1} [TopologicalSpace Z] {ι : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ι → OpenPartialHomeomorph Z E) (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 ℂ E) ⊤ Z

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