Multiplication epimorphisms on Čech H¹ (cechcount unit, Forster 17.8)

For a nonzero global meromorphic function f and any admissible bound MulBound f D E, the multiplication map mulH1 f hf : H¹(D) → H¹(E) is surjective (Forster §17.8's lemma, primal form). Proof: factor through the intermediate divisor D₁ := E + divisor f:

• D ≤ D₁ (that is what the bound says, since f ≠ 0 has finite order everywhere), so H1Incl : H¹(D) → H¹(D₁) is surjective (H1Incl_surjective, the six-term part (g));
• multiplication H¹(D₁) → H¹(E) by f at the exact bound is bijective, with inverse multiplication by f⁻¹ (the composition laws mulH1_mulH1/mulH1_one and f·f⁻¹ = 1 in the function field ℳ X);
• mulH1 f hf agrees with the composite (mulH1_H1Incl).

theorem RS.Cech.mulH1_surjective {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : Mero X} (hf0 : f ≠ 0) {D E : Divisor X} (hf : MulBound f D E) : Function.Surjective ⇑(mulH1 f hf)

Forster 17.8 (primal form): multiplication by a nonzero meromorphic function is surjective on Čech H¹, for any admissible divisor bound.