The Čech count: dim H¹(𝒪_X) ≤ genus X (cechcount unit, Forster 17.9/17.16)

The final theorem of the challenge. Write g := genus X, h⁰¹ := dim_ℂ H¹(𝒪_X) (Čech).

Step 1 (the ledger). For a point P and any n > 2g - 2, Riemann–Roch (RS.riemannRoch + linSys_eq_bot_of_degree_neg' + deg_canonical) gives l(nP) = n + 1 - g, and the Čech χ-ledger (RS.Finiteness.chi_eq_chi_zero_add_degree, with l(0) = 1) turns this into the constancy h¹(nP) = h⁰¹ - g — independent of n.

Step 2 (the growth contradiction, Forster 17.9's count in primal form). Suppose h⁰¹ > g, so c := h⁰¹ - g ≥ 1 and h¹(nP) = c > 0 for every large n. Fix ξ ≠ 0 in H¹(n₀P) (possible since dim = c > 0) and consider the linear map Φ : L(mP) →ₗ H¹((n₀+m)P), f ↦ (f·) ξ (the Čech multiplication mulH1). For m := g + h⁰¹ + 1 the domain has dimension m + 1 - g = h⁰¹ + 2 > c, the target dimension c, so Φ is not injective: some f ≠ 0 in L(mP) has (f·) ξ = 0. But multiplication by a nonzero f is surjective H¹(n₀P) → H¹((n₀+m)P) (mulH1_surjective, Forster 17.8) between spaces of the same finite dimension c, hence injective — forcing ξ = 0. Contradiction; so h⁰¹ ≤ g.

Exports: RS.cechCount (= RS.finrank_H1_zero_le_genus).

theorem RS.cechCount {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Module.finrank ℂ (Cech.H1 0) ≤ genus X

The Čech count (the final theorem of the challenge; Forster §17.9's dimension count, Hodge-free): the first Čech cohomology of the structure sheaf has dimension at most the genus.

theorem RS.finrank_H1_zero_le_genus {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Module.finrank ℂ (Cech.H1 0) ≤ genus X

Alias for cechCount in the project's descriptive naming style.