The linear system L(D) and l(D) (CC3, D4)

Unit: meromorphic-and-divisors (docs/design/meromorphic-and-divisors.md §4.7, D4, proof plan §6.7).

• LinSys D : Submodule ℂ (ℳ X) (D4's carrier: the ord inequality, no case split; 0 ∈ L(D) by ⊤-arithmetic). mem_linSys_iff_eq_zero_or_le_divisor recovers CC3's frozen disjunction as a theorem on a connected surface.
• l D := Module.finrank ℂ (LinSys D).
• linSys_zero_eq_span_one/l_zero (Liouville), vanishing lemmas (linSys_eq_bot_of_nonpos_of_ne_zero), the conditional linSys_eq_bot_of_degree_neg.
• LinSysOn D U (relative version, Čech cochain spaces; junk-gated on IsOpen U, matching D3), restrict_mem_linSysOn, mem_linSys_iff_forall_restrict (bookkeeping toward H⁰(𝔘, O_D) = L(D)).

Deviation from the design doc's listing (noted honestly): linSysMulEquiv (the multiplication LinearEquiv L(D) ≃ₗ L(D - divisor φ)) is not included — the pointwise WithTop ℤ bookkeeping for the two-sided bound is more delicate than the time budget allowed; see the final report for the precise missing step. Everything else in §4.7 is proved.

Pointwise arithmetic on Divisor X (Compat helpers)

theorem RS.Divisor.add_apply {X : Type u_1} [TopologicalSpace X] (D E : Divisor X) (x : X) : (D + E) x = D x + E x

theorem RS.Divisor.neg_apply {X : Type u_1} [TopologicalSpace X] (D : Divisor X) (x : X) : (-D) x = -D x

theorem RS.Divisor.sub_apply {X : Type u_1} [TopologicalSpace X] (D E : Divisor X) (x : X) : (D - E) x = D x - E x

LinSys D

noncomputable def RS.LinSys {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) : Submodule ℂ (Mero X)

CC3's L(D) (carrier per D4; 0 ∈ L(D) by ⊤-arithmetic, not fiat).

Equations

• RS.LinSys D = { carrier := {φ : RS.Mero X | ∀ (x : X), ↑(-D x) ≤ RS.MeroGermOn.ord φ x}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem RS.mem_linSys_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D : Divisor X} {φ : Mero X} : φ ∈ LinSys D ↔ ∀ (x : X), ↑(-D x) ≤ MeroGermOn.ord φ x

theorem RS.mem_linSys_iff_eq_zero_or_le_divisor {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D : Divisor X} [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [ConnectedSpace X] {φ : Mero X} : φ ∈ LinSys D ↔ φ = 0 ∨ -D ≤ divisor φ

CC3's frozen shape, recovered as a characterization on connected X.

noncomputable def RS.l {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) : ℕ

CC3: l D. Finiteness is NOT this unit's business (Čech/finiteness proves FiniteDimensional); until then finrank junk-returns 0 on infinite-dimensional spaces — no lemma here depends on finiteness.

Equations

• RS.l D = Module.finrank ℂ ↥(RS.LinSys D)

theorem RS.linSys_mono {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D E : Divisor X} (h : D ≤ E) : LinSys D ≤ LinSys E

theorem RS.one_mem_linSys_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D : Divisor X} : 1 ∈ LinSys D ↔ 0 ≤ D

theorem RS.algebraMap_mem_linSys {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D : Divisor X} (h : 0 ≤ D) (c : ℂ) : (algebraMap ℂ (Mero X)) c ∈ LinSys D

Vanishing / constancy results

theorem RS.linSys_zero_eq_span_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] : LinSys 0 = ℂ ∙ 1

theorem RS.l_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] : l 0 = 1

theorem RS.linSys_eq_bot_of_nonpos_of_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D : Divisor X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] (h : D ≤ 0) (hD : D ≠ 0) : LinSys D = ⊥

theorem RS.l_eq_zero_of_nonpos_of_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D : Divisor X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] (h : D ≤ 0) (hD : D ≠ 0) : l D = 0

theorem RS.linSys_eq_bot_of_degree_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D : Divisor X} [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] (hdeg : ∀ (φ : Mero X), φ ≠ 0 → Function.locallyFinsuppWithin.degree (divisor φ) = 0) (h : Function.locallyFinsuppWithin.degree D < 0) : LinSys D = ⊥

deg D < 0 → L(D) = 0, CONDITIONAL on deg ∘ divisor = 0 — that input is owned by proper-map-degree (argument principle / degree counting).

Relative version (Čech cochain spaces)

noncomputable def RS.LinSysOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) (U : Set X) : Submodule ℂ (MeroGermOn X U)

Relative L(D) (CC8 Čech cochain spaces). Junk-gated on IsOpen U (D3): when U is not open, the condition is vacuous (every class qualifies), matching ord's own junk convention so that zero_mem' holds unconditionally.

Equations

• RS.LinSysOn D U = { carrier := {φ : RS.MeroGermOn X U | IsOpen U → ∀ x ∈ U, ↑(-D x) ≤ φ.ord x}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem RS.mem_linSysOn_iff_of_isOpen {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {D : Divisor X} (hU : IsOpen U) {φ : MeroGermOn X U} : φ ∈ LinSysOn D U ↔ ∀ x ∈ U, ↑(-D x) ≤ φ.ord x

theorem RS.restrict_mem_linSysOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U V : Set X} {D : Divisor X} (h : V ⊆ U) (hV : IsOpen V) (hU : IsOpen U) {φ : MeroGermOn X U} (hφ : φ ∈ LinSysOn D U) : (MeroGermOn.restrict h) φ ∈ LinSysOn D V

theorem RS.mem_linSys_iff_forall_restrict {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D : Divisor X} {ι : Type u_2} {W : ι → Set X} (hW : ∀ (i : ι), IsOpen (W i)) (hcov : ⋃ (i : ι), W i = Set.univ) {φ : Mero X} : φ ∈ LinSys D ↔ ∀ (i : ι), (MeroGermOn.restrict ⋯) φ ∈ LinSysOn D (W i)