Finite-dimensionality of the space of holomorphic 1-forms (CC1, design §2.6)

Unit: holomorphic-forms (docs/design/holomorphic-forms.md). On a compact X the space RS.Form1 X is finite-dimensional, making genus := Module.finrank ℂ (Form1 X) honest.

Route: a good cover (finitely many doubly-shrunk chart neighbourhoods V i ⋐ W i ⋐ chart sources) gives an injective linear coefficient embedding J : Form1 X →ₗ[ℂ] Π i, C(K i, ℂ) into a finite product of sup-normed spaces (K i the compact chart image of closure (V i)). The transition rule bounds all coefficients on the larger open U i ⊇ K i uniformly over the unit ball of the image, so the unit ball sits inside a product of Montel compacta (RS.isCompact_closure_montelFamily); the unit ball of the image is closed by Weierstrass convergence + reassembly through RS.Form1.ofCoeffs over restricted charts, hence compact; Riesz (FiniteDimensional.of_isCompact_closedBall₀) finishes.

Main declarations:

• RS.GoodCover, RS.GoodCover.nonempty — finite doubly-shrunk chart covers exist.
• RS.GoodCover.J — the coefficient embedding, RS.GoodCover.J_injective.
• RS.GoodCover.exists_montel_bound — the uniform coefficient bound.
• RS.GoodCover.isClosed_ball_inter_range — the unit ball of the image is closed.
• instance : FiniteDimensional ℂ (Form1 X) (compact T2 X).

A generic dense-agreement extension helper

theorem RS.eqOn_of_eqOn_of_subset_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] {f g : α → β} {s t : Set α} (hst : s ⊆ t) (hts : t ⊆ closure s) (hf : ContinuousOn f t) (hg : ContinuousOn g t) (h : Set.EqOn f g s) : Set.EqOn f g t

Two functions continuous on t that agree on a subset s with t ⊆ closure s agree on t.

Good covers

structure RS.GoodCover (X : Type u_2) [TopologicalSpace X] [ChartedSpace ℂ X] : Type u_2

A good cover: finitely many chart-centred pairs of open sets V i ⋐ W i with closure (W i) inside the chart source, the V i covering X (design §2.6 step 1).

• n : ℕ

  Number of cover elements.

• c : Fin self.n → X

  Chart centres.

• V : Fin self.n → Set X

  Inner cover sets.

• W : Fin self.n → Set X

  Outer cover sets.

• isOpen_V (i : Fin self.n) : IsOpen (self.V i)
• isOpen_W (i : Fin self.n) : IsOpen (self.W i)
• closure_V_subset (i : Fin self.n) : closure (self.V i) ⊆ self.W i
• closure_W_subset (i : Fin self.n) : closure (self.W i) ⊆ (chartAt ℂ (self.c i)).source
• iUnion_V : ⋃ (i : Fin self.n), self.V i = Set.univ

theorem RS.GoodCover.nonempty {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T2Space X] [CompactSpace X] : Nonempty (GoodCover X)

Good covers exist on compact T2 surfaces (double shrinking by local compactness + finite subcover).

noncomputable def RS.GoodCover.e {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : OpenPartialHomeomorph X ℂ

The chart of the i-th cover element.

Equations

• G.e i = chartAt ℂ (G.c i)

theorem RS.GoodCover.W_subset_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : G.W i ⊆ (G.e i).source

theorem RS.GoodCover.closureV_subset_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : closure (G.V i) ⊆ (G.e i).source

theorem RS.GoodCover.V_subset_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : G.V i ⊆ (G.e i).source

theorem RS.GoodCover.exists_mem_V {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (x : X) : ∃ (i : Fin G.n), x ∈ G.V i

def RS.GoodCover.O {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : Set ℂ

Open chart image of the inner set.

Equations

• G.O i = ↑(G.e i) '' G.V i

def RS.GoodCover.K {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : Set ℂ

Compact chart image of the closed inner set: the set on which coefficients are compared.

Equations

• G.K i = ↑(G.e i) '' closure (G.V i)

def RS.GoodCover.U {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : Set ℂ

Open chart image of the outer set: the Montel domain.

Equations

• G.U i = ↑(G.e i) '' G.W i

theorem RS.GoodCover.isOpen_O {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : IsOpen (G.O i)

theorem RS.GoodCover.isOpen_U {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : IsOpen (G.U i)

theorem RS.GoodCover.isCompact_K {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) [CompactSpace X] (i : Fin G.n) : IsCompact (G.K i)

theorem RS.GoodCover.O_subset_K {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : G.O i ⊆ G.K i

theorem RS.GoodCover.K_subset_U {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : G.K i ⊆ G.U i

theorem RS.GoodCover.O_subset_target {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : G.O i ⊆ (G.e i).target

theorem RS.GoodCover.K_subset_target {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : G.K i ⊆ (G.e i).target

theorem RS.GoodCover.U_subset_target {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : G.U i ⊆ (G.e i).target

theorem RS.GoodCover.K_subset_closure_O {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : G.K i ⊆ closure (G.O i)

theorem RS.GoodCover.symm_mem_W {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) {i : Fin G.n} {z : ℂ} (hz : z ∈ G.U i) : ↑(G.e i).symm z ∈ G.W i

theorem RS.GoodCover.mem_K_of_mem_V {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) {i : Fin G.n} {x : X} (hx : x ∈ G.V i) : ↑(G.e i) x ∈ G.K i

theorem RS.GoodCover.e_mem_maximalAtlas {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (i : Fin G.n) : G.e i ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X

Restricted charts

theorem RS.GoodCover.restr_source_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : ((G.e i).restr (G.V i)).source = (G.e i).source ∩ G.V i

theorem RS.GoodCover.mem_restr_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) {i : Fin G.n} {x : X} (hx : x ∈ G.V i) : x ∈ ((G.e i).restr (G.V i)).source

theorem RS.GoodCover.restr_target_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (i : Fin G.n) : ((G.e i).restr (G.V i)).target = G.O i

The coefficient embedding J

instance RS.GoodCover.instCompactSpaceK {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) [CompactSpace X] (i : Fin G.n) : CompactSpace ↑(G.K i)

@[reducible, inline]

abbrev RS.GoodCover.P {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) : Type

The target of the coefficient embedding: a finite product of sup-normed spaces of continuous functions on the compact sets K i.

Equations

• G.P = ((i : Fin G.n) → C(↑(G.K i), ℂ))

noncomputable def RS.GoodCover.J {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (G : GoodCover X) : Form1 X →ₗ[ℂ] G.P

The coefficient embedding: a holomorphic 1-form goes to the tuple of restrictions of its chart coefficients to the compacta K i. The norm ‖J η‖ = max_i sup_{K i} ‖coeffIn (e i) η‖ is exactly CC1's prescribed norm — it lives on P, never as an instance on Form1 X.

Equations

• G.J = { toFun := fun (η : RS.Form1 X) (i : Fin G.n) => { toFun := (G.K i).domRestrict (RS.coeffIn (G.e i) η), continuous_toFun := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RS.GoodCover.J_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (G : GoodCover X) (η : Form1 X) (i : Fin G.n) (z : ↑(G.K i)) : (G.J η i) z = coeffIn (G.e i) η ↑z

theorem RS.GoodCover.norm_coeffIn_le_of_mem_K {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (G : GoodCover X) [CompactSpace X] (η : Form1 X) {i : Fin G.n} {z : ℂ} (hz : z ∈ G.K i) : ‖coeffIn (G.e i) η z‖ ≤ ‖G.J η‖

theorem RS.GoodCover.J_injective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (G : GoodCover X) : Function.Injective ⇑G.J

The uniform Montel bound

theorem RS.GoodCover.exists_montel_bound {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (G : GoodCover X) [CompactSpace X] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (η : Form1 X), ‖G.J η‖ ≤ 1 → ∀ (i : Fin G.n), ∀ z ∈ G.U i, ‖coeffIn (G.e i) η z‖ ≤ C

Uniform bound (design §2.6 step 4): coefficients of unit-ball forms are uniformly bounded on the Montel domains U i — the transition-derivative suprema over the compact overlap pieces transfer the K j-bounds outward.

theorem RS.GoodCover.J_mem_montelFamily {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (G : GoodCover X) [CompactSpace X] {C : ℝ} (hC : ∀ (η : Form1 X), ‖G.J η‖ ≤ 1 → ∀ (i : Fin G.n), ∀ z ∈ G.U i, ‖coeffIn (G.e i) η z‖ ≤ C) {η : Form1 X} (hη : ‖G.J η‖ ≤ 1) (i : Fin G.n) : G.J η i ∈ montelFamily (G.U i) (G.K i) C

Unit-ball coefficient tuples lie in the Montel families.

Closedness of the unit ball of the image

noncomputable def RS.GoodCover.gext {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (f : G.P) (i : Fin G.n) : ℂ → ℂ

The (junk-extended) limit coefficient function on K i of a convergent tuple.

Equations

• G.gext f i z = if h : z ∈ G.K i then (f i) ⟨z, h⟩ else 0

theorem RS.GoodCover.gext_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (f : G.P) {i : Fin G.n} {z : ℂ} (hz : z ∈ G.K i) : G.gext f i z = (f i) ⟨z, hz⟩

theorem RS.GoodCover.continuousOn_gext {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (G : GoodCover X) (f : G.P) (i : Fin G.n) : ContinuousOn (G.gext f i) (G.K i)

theorem RS.GoodCover.tendstoUniformlyOn_coeffIn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (G : GoodCover X) [CompactSpace X] {η : ℕ → Form1 X} {f : G.P} (hlim : Filter.Tendsto (fun (m : ℕ) => G.J (η m)) Filter.atTop (nhds f)) (i : Fin G.n) : TendstoUniformlyOn (fun (m : ℕ) (z : ℂ) => coeffIn (G.e i) (η m) z) (G.gext f i) Filter.atTop (G.K i)

Convergence in P gives uniform convergence of the coefficient functions on each K i.

theorem RS.GoodCover.analyticOnNhd_gext {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (G : GoodCover X) [CompactSpace X] {η : ℕ → Form1 X} {f : G.P} (hlim : Filter.Tendsto (fun (m : ℕ) => G.J (η m)) Filter.atTop (nhds f)) (i : Fin G.n) : AnalyticOnNhd ℂ (G.gext f i) (G.O i)

Weierstrass: the limit coefficient functions are analytic on the open sets O i.

theorem RS.GoodCover.gext_compat {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (G : GoodCover X) [CompactSpace X] {η : ℕ → Form1 X} {f : G.P} (hlim : Filter.Tendsto (fun (m : ℕ) => G.J (η m)) Filter.atTop (nhds f)) (i j : Fin G.n) {x : X} (hxi : x ∈ G.V i) (hxj : x ∈ G.V j) : G.gext f j (↑(G.e j) x) = deriv (↑(G.e i) ∘ ↑(G.e j).symm) (↑(G.e j) x) * G.gext f i (↑(G.e i) x)

The limit coefficient functions satisfy the transition compatibility (pointwise limits of the stagewise coeffIn_trans identities).

theorem RS.GoodCover.isClosed_ball_inter_range {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (G : GoodCover X) [CompactSpace X] : IsClosed (Metric.closedBall 0 1 ∩ Set.range ⇑G.J)

Closedness (design §2.6 step 5): the unit ball of the range of J is closed in P — uniform limits of coefficient tuples are reassembled into a holomorphic 1-form via Form1.ofCoeffs over the restricted charts.

theorem RS.GoodCover.isCompact_ball_inter_range {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (G : GoodCover X) [CompactSpace X] : IsCompact (Metric.closedBall 0 1 ∩ Set.range ⇑G.J)

Compactness (Montel + closedness): the unit ball of the range of J is compact.

Riesz and the instance

instance RS.instFiniteDimensionalComplexForm1OfT2SpaceOfCompactSpace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] : FiniteDimensional ℂ (Form1 X)

Finite-dimensionality of the space of holomorphic 1-forms on a compact Riemann surface (design §2.6 step 6): the coefficient embedding has compact unit ball, so its range is finite-dimensional by Riesz, and J is injective. This is what makes genus honest.