Multiplication on Čech H¹ by global meromorphic functions (cechcount unit)

Unit: cechcount (Jacobian/CechCount/), the final gate: Forster §17.8-17.9 at the Čech level.

Multiplication by a fixed global meromorphic function f : ℳ X acts on O_D-valued Čech cochains, sending the D-pole-bound to an E-pole-bound whenever the pointwise order bound MulBound f D E (∀ x, D x - E x ≤ ord_x f, in WithTop ℤ) holds. This file builds the action level by level, mirroring Colimit.lean's H1Incl construction verbatim:

• MulBound f D E and its kit (mulBound_zero, MulBound.add/smul/mul, mulBound_one, le_of_mulBound_one, mulBound_of_mem_linSys).
• mulOn f hf U : LinSysOn D U →ₗ LinSysOn E U (germ level, via LinearMap.mulLeft and MeroGermOn.restrict), commuting with the presheaf restrictions (restrictL_mulOn).
• mulC0/mulC1 (cochain level), commuting with d0/d1/resC1, hence mulZ1, mulH1Cover (Submodule.mapQ), commuting with resH1.
• mulH1 f hf : H1 D →ₗ[ℂ] H1 E (Module.DirectLimit.map), with mulH1_toH1 and the algebra laws mulH1_add, mulH1_smul, mulH1_mulH1 (composition = product), mulH1_one (= H1Incl), mulH1_H1Incl, mulH1_congr.

Surjective.lean (next file) combines these with H1Incl_surjective into the Forster 17.8 epimorphism statement mulH1_surjective.

The pointwise multiplication bound

def RS.Cech.MulBound {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : Mero X) (D E : Divisor X) : Prop

The pointwise order bound making multiplication by f carry O_D-cochains to O_E-cochains: D x - E x ≤ ord_x f for every x (in WithTop ℤ; for f = 0 the order is ⊤ everywhere, so MulBound 0 D E always holds — multiplication by 0 is the zero map).

Equations

• RS.Cech.MulBound f D E = ∀ (x : X), ↑(D x - E x) ≤ RS.MeroGermOn.ord f x

theorem RS.Cech.mulBound_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D E : Divisor X) : MulBound 0 D E

theorem RS.Cech.MulBound.add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : Mero X} {D E : Divisor X} (hf : MulBound f D E) (hg : MulBound g D E) : MulBound (f + g) D E

theorem RS.Cech.MulBound.smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : Mero X} {D E : Divisor X} (c : ℂ) (hf : MulBound f D E) : MulBound (c • f) D E

theorem RS.Cech.MulBound.mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : Mero X} {D D' E : Divisor X} (hf : MulBound f D' E) (hg : MulBound g D D') : MulBound (f * g) D E

theorem RS.Cech.mulBound_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D E : Divisor X} (h : D ≤ E) : MulBound 1 D E

theorem RS.Cech.le_of_mulBound_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D E : Divisor X} (h : MulBound 1 D E) : D ≤ E

theorem RS.Cech.mulBound_of_mem_linSys {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : Mero X} {B D E : Divisor X} (hf : f ∈ LinSys B) (h : ∀ (x : X), D x - E x ≤ -B x) : MulBound f D E

Germ level: mulOn

theorem RS.Cech.mul_restrict_mem_linSysOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : Mero X} {D E : Divisor X} (hf : MulBound f D E) (U : TopologicalSpace.Opens X) {φ : MeroGermOn X ↑U} (hφ : φ ∈ LinSysOn D ↑U) : (MeroGermOn.restrict ⋯) f * φ ∈ LinSysOn E ↑U

noncomputable def RS.Cech.mulOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) (U : TopologicalSpace.Opens X) : ↥(LinSysOn D ↑U) →ₗ[ℂ] ↥(LinSysOn E ↑U)

Multiplication by (the restriction of) a global meromorphic function on relative linear systems over an open U, under the pointwise bound MulBound f D E.

Equations

• RS.Cech.mulOn f hf U = (LinearMap.mulLeft ℂ ((RS.MeroGermOn.restrict ⋯) f)).restrict ⋯

theorem RS.Cech.mulOn_apply_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) (U : TopologicalSpace.Opens X) (φ : ↥(LinSysOn D ↑U)) : ↑((mulOn f hf U) φ) = (MeroGermOn.restrict ⋯) f * ↑φ

theorem RS.Cech.restrictL_mulOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {V U : TopologicalSpace.Opens X} (hVU : V ≤ U) (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) (φ : ↥(LinSysOn D ↑U)) : (LinSysOn.restrictL E hVU) ((mulOn f hf U) φ) = (mulOn f hf V) ((LinSysOn.restrictL D hVU) φ)

mulOn commutes with the presheaf restriction maps.

Cochain level: mulC0, mulC1

noncomputable def RS.Cech.mulC0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) (𝒰 : FinCover Ω) : C0 D 𝒰 →ₗ[ℂ] C0 E 𝒰

Multiplication by f on 0-cochains (componentwise mulOn).

Equations

• RS.Cech.mulC0 f hf 𝒰 = LinearMap.pi fun (i : Fin 𝒰.n) => RS.Cech.mulOn f hf (𝒰.U i) ∘ₗ LinearMap.proj i

theorem RS.Cech.mulC0_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) {𝒰 : FinCover Ω} (g : C0 D 𝒰) (i : Fin 𝒰.n) : (mulC0 f hf 𝒰) g i = (mulOn f hf (𝒰.U i)) (g i)

noncomputable def RS.Cech.mulC1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) (𝒰 : FinCover Ω) : C1 D 𝒰 →ₗ[ℂ] C1 E 𝒰

Multiplication by f on 1-cochains (componentwise mulOn).

Equations

• RS.Cech.mulC1 f hf 𝒰 = LinearMap.pi fun (p : Fin 𝒰.n × Fin 𝒰.n) => RS.Cech.mulOn f hf (𝒰.U p.1 ⊓ 𝒰.U p.2) ∘ₗ LinearMap.proj p

theorem RS.Cech.mulC1_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) {𝒰 : FinCover Ω} (c : C1 D 𝒰) (p : Fin 𝒰.n × Fin 𝒰.n) : (mulC1 f hf 𝒰) c p = (mulOn f hf (𝒰.U p.1 ⊓ 𝒰.U p.2)) (c p)

theorem RS.Cech.mulC1_d0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) (𝒰 : FinCover Ω) (g : C0 D 𝒰) : (mulC1 f hf 𝒰) ((d0 D 𝒰) g) = (d0 E 𝒰) ((mulC0 f hf 𝒰) g)

Multiplication commutes with the coboundary d0.

theorem RS.Cech.mulC1_mem_Z1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) {𝒰 : FinCover Ω} {c : C1 D 𝒰} (hc : c ∈ Z1 D 𝒰) : (mulC1 f hf 𝒰) c ∈ Z1 E 𝒰

Multiplication preserves cocycles.

theorem RS.Cech.mulC1_mem_B1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) {𝒰 : FinCover Ω} {c : C1 D 𝒰} (hc : c ∈ B1 D 𝒰) : (mulC1 f hf 𝒰) c ∈ B1 E 𝒰

Multiplication preserves coboundaries.

Cocycle and cover-level H¹

noncomputable def RS.Cech.mulZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) (𝒰 : FinCover Ω) : ↥(Z1 D 𝒰) →ₗ[ℂ] ↥(Z1 E 𝒰)

Multiplication on 1-cocycles.

Equations

• RS.Cech.mulZ1 f hf 𝒰 = (RS.Cech.mulC1 f hf 𝒰).restrict ⋯

theorem RS.Cech.mulZ1_apply_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) {𝒰 : FinCover Ω} (c : ↥(Z1 D 𝒰)) : ↑((mulZ1 f hf 𝒰) c) = (mulC1 f hf 𝒰) ↑c

noncomputable def RS.Cech.mulH1Cover {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) (𝒰 : FinCover Ω) : H1Cover D 𝒰 →ₗ[ℂ] H1Cover E 𝒰

Multiplication on cover-level H¹.

Equations

• RS.Cech.mulH1Cover f hf 𝒰 = (Submodule.comap (RS.Cech.Z1 D 𝒰).subtype (RS.Cech.B1 D 𝒰)).mapQ (Submodule.comap (RS.Cech.Z1 E 𝒰).subtype (RS.Cech.B1 E 𝒰)) (RS.Cech.mulZ1 f hf 𝒰) ⋯

theorem RS.Cech.mulH1Cover_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) {𝒰 : FinCover Ω} (c : ↥(Z1 D 𝒰)) : (mulH1Cover f hf 𝒰) ((H1Cover.mk D 𝒰) c) = (H1Cover.mk E 𝒰) ((mulZ1 f hf 𝒰) c)

theorem RS.Cech.mulC1_resC1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) (c : C1 D 𝒰) : (mulC1 f hf 𝒱) ((resC1 D τ hτ) c) = (resC1 E τ hτ) ((mulC1 f hf 𝒰) c)

Multiplication commutes with refinement of 1-cochains.

theorem RS.Cech.mulH1Cover_resH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Ω : TopologicalSpace.Opens X} (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) {𝒰 𝒱 : FinCover Ω} (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : IsRefIdx 𝒰 𝒱 τ) (ξ : H1Cover D 𝒰) : (mulH1Cover f hf 𝒱) ((resH1 D τ hτ) ξ) = (resH1 E τ hτ) ((mulH1Cover f hf 𝒰) ξ)

Multiplication commutes with refinement of cover-level H¹.

The colimit map mulH1

noncomputable def RS.Cech.mulH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) : H1 D →ₗ[ℂ] H1 E

Multiplication on Čech H¹ by a global meromorphic function f under the pointwise bound MulBound f D E (Forster §17.8's sheaf morphism O_D → O_E, g ↦ f·g, at the colimit level). Built via Module.DirectLimit.map, mirroring H1Incl.

Equations

• RS.Cech.mulH1 f hf = Module.DirectLimit.map (fun (𝒰 : RS.Cech.FinCover ⊤) => RS.Cech.mulH1Cover f hf 𝒰) ⋯

@[simp]

theorem RS.Cech.mulH1_toH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : Mero X) {D E : Divisor X} (hf : MulBound f D E) (𝒰 : FinCover ⊤) (c : H1Cover D 𝒰) : (mulH1 f hf) ((toH1 D 𝒰) c) = (toH1 E 𝒰) ((mulH1Cover f hf 𝒰) c)

Algebra laws for mulH1

theorem RS.Cech.mulH1_congr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : Mero X} (hfg : f = g) {D E : Divisor X} (hf : MulBound f D E) (hg : MulBound g D E) (ξ : H1 D) : (mulH1 f hf) ξ = (mulH1 g hg) ξ

mulH1 only depends on the function, not on the bound proof (and transports along equality of functions).

theorem RS.Cech.mulH1_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : Mero X} {D E : Divisor X} (hf : MulBound f D E) (hg : MulBound g D E) (hfg : MulBound (f + g) D E) (ξ : H1 D) : (mulH1 (f + g) hfg) ξ = (mulH1 f hf) ξ + (mulH1 g hg) ξ

theorem RS.Cech.mulH1_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : Mero X} {D E : Divisor X} (a : ℂ) (hf : MulBound f D E) (haf : MulBound (a • f) D E) (ξ : H1 D) : (mulH1 (a • f) haf) ξ = a • (mulH1 f hf) ξ

theorem RS.Cech.mulH1_mulH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : Mero X} {D D' E : Divisor X} (hf : MulBound f D' E) (hg : MulBound g D D') (hfg : MulBound (f * g) D E) (ξ : H1 D) : (mulH1 f hf) ((mulH1 g hg) ξ) = (mulH1 (f * g) hfg) ξ

Composition of multiplications is multiplication by the product.

theorem RS.Cech.mulH1_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {D E : Divisor X} (h1 : MulBound 1 D E) (hDE : D ≤ E) (ξ : H1 D) : (mulH1 1 h1) ξ = (H1Incl D hDE) ξ

Multiplication by 1 is the divisor inclusion.

theorem RS.Cech.mulH1_H1Incl {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : Mero X} {D D' E : Divisor X} (h : D ≤ D') (hf' : MulBound f D' E) (hf : MulBound f D E) (ξ : H1 D) : (mulH1 f hf') ((H1Incl D h) ξ) = (mulH1 f hf) ξ

Multiplication absorbs a preceding divisor inclusion.