FiniteDimensional ℂ (H1 D) for all D (finiteness-and-chi, gated file 2/3)

Unit: finiteness-and-chi (docs/design/finiteness-and-chi.md §6.4/§6.5, §7).

• toH1_coverW_surjective: every H1 (0 : Divisor X)-class has a T.coverW-level representative (Leray at the good cover T.coverStar, pushed down along T.ref_star_W).
• finiteDimensional_h1Cover_W: H1Cover 0 T.coverW is finite-dimensional — the Schwartz cospan assembly (§6.5), consuming TradeBounded.lean's tradePi_surjective, isCompactOperator_tradeCompact, classMap_tradeDiff_eq_zero, classMap_surjective.
• finiteDimensional_H1_zero: the unit's headline instance, FiniteDimensional ℂ (H1 (0 : Divisor X)).
• finiteDimensional_H1: FiniteDimensional ℂ (H1 D) for ALL D (§7, decision D2 — via cech's six-term skyscraper fragment, NOT twisted norms).

§6.5: assembly at a fixed ShrinkChain

theorem RS.Finiteness.toH1_coverW_surjective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] (T : ShrinkChain X) : Function.Surjective ⇑(Cech.toH1 0 T.coverW)

Every H1 (0 : Divisor X)-class already has a representative on T.coverW (push Leray's T.coverStar-level surjectivity down along the same-index refinement T.ref_star_W).

theorem RS.Finiteness.finiteDimensional_h1Cover_W {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] (T : ShrinkChain X) : FiniteDimensional ℂ (Cech.H1Cover 0 T.coverW)

§6.5's assembly: the Schwartz cospan lemma finishes off H1Cover 0 T.coverW.

@[instance_reducible]

noncomputable instance RS.Finiteness.addCommGroupH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) : AddCommGroup (Cech.H1 D)

Compat: AddCommGroup (H1 D) does not resolve by plain inferInstance in this codebase (a higher-order-instance gap resolving ∀ 𝒰, AddCommGroup (H1Cover D 𝒰) for Module.DirectLimit.addCommGroup, per cech's own recorded gotcha) — supply it explicitly.

Equations

• RS.Finiteness.addCommGroupH1 D = Module.DirectLimit.addCommGroup (fun (𝒰 : RS.Cech.FinCover ⊤) => RS.Cech.H1Cover D 𝒰) fun (x x_1 : RS.Cech.FinCover ⊤) (h : x ≤ x_1) => RS.Cech.resH1' D h

instance RS.Finiteness.finiteDimensional_H1_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] : FiniteDimensional ℂ (Cech.H1 0)

The unit's headline instance: H¹(X, 𝒪) is finite-dimensional (Forster §14).

§7: all-D finiteness (the six-term skyscraper fragment, decision D2)

instance RS.Finiteness.finiteDimensional_H1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] (D : Divisor X) : FiniteDimensional ℂ (Cech.H1 D)

All-D finiteness (§7): H¹(D) is finite-dimensional for every divisor D. With D' := D ⊔ 0: H¹(D') is finite (surjective image of H¹(0) via H1Incl_surjective); the inclusion H¹(D) ↪ H¹(D') has finite-dimensional kernel (= range (windowConnect h) by cech's six-term exactness exact_windowConnect_H1Incl, itself finite since Window D D' is) and finite-dimensional codomain H¹(D'), so H¹(D) is finite by FiniteDimensional.of_linearMap_ker_range.