28.7. H1Genus.SerreCupProduct🔗

Jacobians.H1Genus.SerreCupProduct — source

mulLeftG

Multiplication of MGerm U by a fixed germ a : MGerm U, as an ℂ-linear map. (MGerm U is a Filter.Germ CommRing; multiplication is ℂ-bilinear because the scalar action c • g is the pointwise (c • ·) — definitionally ↑(c • g) — so c • (a*b) = (c•a)*b.)

noncomputable def mulLeftG {U : Opens X} (a : MGerm U) : MGerm U →ₗ[ℂ] MGerm U where

smul_mul_MGerm

Scalar-multiplication / ring-multiplication associativity on MGerm ((a • x) * y = a • (x*y)): the Module ℂ action is the pointwise (a • ·) (definitionally ↑(a • ·)). Proven directly to avoid an IsScalarTower ℂ (MGerm U) (MGerm U) synthesis gap (the Germ Module ℂ comes from the C*-algebra path, not registered as a scalar tower with the ring multiplication).

theorem smul_mul_MGerm {X : Type*} [TopologicalSpace X] {U : Opens X} (a : ℂ) (x y : MGerm U) :
    (a • x) * y = a • (x * y)

rawRestrictG_mul

Germ restriction is a ring hom (rawRestrictG (a*b) = rawRestrictG a * rawRestrictG b): both sides are the germ of the pointwise product precomposed with the open inclusion.

theorem rawRestrictG_mul {X : Type*} [TopologicalSpace X] {U V : Opens X} (h : V ≤ U)
    (a b : MGerm U) :
    rawRestrictG h (a * b) = rawRestrictG h a * rawRestrictG h b

globalGerm

The germ-class on ↥U of (the restriction of) a *global* meromorphic function F. This is the function-side avatar of f·ω₀ after dividing by ω₀: the cup product multiplies a 𝒪_D cochain by this germ.

noncomputable def globalGerm (F : MeromorphicFunction X) (U : Opens X) : MGerm U

rawRestrictG_globalGerm

Restriction of the global germ to a smaller open is the global germ there (F is the same global function; restriction is precomposition with the open inclusion, and (F∘val) ∘ openIncl = F∘val).

theorem rawRestrictG_globalGerm {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (F : MeromorphicFunction X)
    {U V : Opens X} (h : V ≤ U) :
    rawRestrictG h (globalGerm F U) = globalGerm F V

ordU_globalMul

The order on ↥U of (F∘val)·g is orderW F (corresponding point) plus the order of g. The key order-additivity (meromorphicOrderAt_mul) behind the poles-cancellation of the cup product.

theorem ordU_globalMul {U : Opens X} (F : MeromorphicFunction X) {g : U → ℂ}
    (hg : IsMeromorphic (U : Type _) g) (x : U) :
    ordU ((F.toFun ∘ Subtype.val) * g) x = F.orderW x.1 + ordU g x

mulConstG_omegaDGerm

Multiplying a 𝒪_D germ by f ∈ L(K−D) lands in 𝒪_K (poles cancel). If f ∈ L(K−D) (div f ≥ D−K) and s ∈ 𝒪_D(U) (div s ≥ −D), then f·s ∈ 𝒪_K(U) (div(f·s) ≥ −K): the order adds (ordU_globalMul), and −(K x) ≤ orderW f x + ordU s from −((K−D) x) ≤ orderW f x and −(D x) ≤ ordU s.

theorem mulConstG_omegaDGerm {D K : Divisor X} {f : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (K - D)) {U : Opens X} {s : MGerm U}
    (hs : s ∈ OmegaDGerm D U) :
    globalGerm f U * s ∈ OmegaDGerm K U

cupCochain0

Multiply each component of a 0-cochain by the global germ of f on U_i.

noncomputable def cupCochain0 (f : MeromorphicFunction X) : 𝔘.Cochain0 →ₗ[ℂ] 𝔘.Cochain0

cupCochain1

Multiply each component of a 1-cochain by the global germ of f on U_i ∩ U_j.

noncomputable def cupCochain1 (f : MeromorphicFunction X) : 𝔘.Cochain1 →ₗ[ℂ] 𝔘.Cochain1

cupCochain2

Multiply each component of a 2-cochain by the global germ of f on the triple intersection.

noncomputable def cupCochain2 (f : MeromorphicFunction X) : 𝔘.Cochain2 →ₗ[ℂ] 𝔘.Cochain2

cupCochain0_apply

@[simp] theorem cupCochain0_apply {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteFamily X)
    (f : MeromorphicFunction X) (c : 𝔘.Cochain0) (i : 𝔘.ι) :
    cupCochain0 𝔘 f c i = globalGerm f (𝔘.U i) * c i

cupCochain1_apply

@[simp] theorem cupCochain1_apply {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteFamily X)
    (f : MeromorphicFunction X) (c : 𝔘.Cochain1) (p : 𝔘.ι × 𝔘.ι) :
    cupCochain1 𝔘 f c p = globalGerm f (𝔘.U p.1 ⊓ 𝔘.U p.2) * c p

cupCochain2_apply

@[simp] theorem cupCochain2_apply {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteFamily X)
    (f : MeromorphicFunction X) (c : 𝔘.Cochain2) (t : 𝔘.ι × 𝔘.ι × 𝔘.ι) :
    cupCochain2 𝔘 f c t = globalGerm f (𝔘.U t.1 ⊓ 𝔘.U t.2.1 ⊓ 𝔘.U t.2.2) * c t

cupCochain1_comp_cechDelta0

Multiplying by f commutes with δ⁰ (cup ∘ δ⁰ = δ⁰ ∘ cup). On each pair (i,j), both sides equal globalGerm f (U_i∩U_j) · (g_j|_{ij} − g_i|_{ij}) — germ restriction is a ring hom and globalGerm f restricts to globalGerm f.

theorem cupCochain1_comp_cechDelta0 {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteFamily X) (f : MeromorphicFunction X) :
    (cupCochain1 𝔘 f) ∘ₗ 𝔘.cechDelta0 = 𝔘.cechDelta0 ∘ₗ (cupCochain0 𝔘 f)

cupCochain2_comp_cechDelta1

Multiplying by f commutes with δ¹ (cup ∘ δ¹ = δ¹ ∘ cup). Termwise: germ restriction is a ring hom, and globalGerm f restricts to globalGerm f, so the three alternating terms each carry the f-factor through.

theorem cupCochain2_comp_cechDelta1 {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteFamily X) (f : MeromorphicFunction X) :
    (cupCochain2 𝔘 f) ∘ₗ 𝔘.cechDelta1 = 𝔘.cechDelta1 ∘ₗ (cupCochain1 𝔘 f)

cupCochain0_sections0

Multiplying a 0-cochain of 𝒪_D-sections by f ∈ L(K−D) gives a 0-cochain of 𝒪_K-sections.

theorem cupCochain0_sections0 {D K : Divisor X} {f : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (K - D)) {c : 𝔘.Cochain0} (hc : c ∈ 𝔘.sections0 D) :
    cupCochain0 𝔘 f c ∈ 𝔘.sections0 K

cupCochain1_sections1

Multiplying a 1-cochain of 𝒪_D-sections by f ∈ L(K−D) gives a 1-cochain of 𝒪_K-sections.

theorem cupCochain1_sections1 {D K : Divisor X} {f : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (K - D)) {c : 𝔘.Cochain1} (hc : c ∈ 𝔘.sections1 D) :
    cupCochain1 𝔘 f c ∈ 𝔘.sections1 K

cupCochain1_cocycles1

The cup product maps 𝒪_D-cocycles to 𝒪_K-cocycles: it preserves ker δ¹ (commutation cup₂ ∘ δ¹ = δ¹ ∘ cup₁) and the sheaf condition (cupCochain1_sections1).

theorem cupCochain1_cocycles1 {D K : Divisor X} {f : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (K - D)) {c : 𝔘.Cochain1} (hc : c ∈ 𝔘.cocycles1 D) :
    cupCochain1 𝔘 f c ∈ 𝔘.cocycles1 K

cupCochain1_coboundaries1

The cup product maps 𝒪_D-coboundaries to 𝒪_K-coboundaries: cup₁(δ⁰ s) = δ⁰(cup₀ s) (commutation) and cup₀ s is a 𝒪_K-section (cupCochain0_sections0).

theorem cupCochain1_coboundaries1 {D K : Divisor X} {f : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (K - D)) {c : 𝔘.Cochain1} (hc : c ∈ 𝔘.coboundaries1 D) :
    cupCochain1 𝔘 f c ∈ 𝔘.coboundaries1 K

cupCocyclesMap

The cup product as a linear map of cocycle submodules cocycles1 D → cocycles1 K (the restriction of cupCochain1 f).

noncomputable def cupCocyclesMap {D K : Divisor X} {f : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (K - D)) :
    ↥(𝔘.cocycles1 D) →ₗ[ℂ] ↥(𝔘.cocycles1 K)

cupH1

The descended cup product on cohomology [ξ] ↦ [f·ξ], cechH1 D →ₗ[ℂ] cechH1 K. Well-defined because the cup product maps cocycles1 D → cocycles1 K (cupCochain1_cocycles1) and coboundaries1 D → coboundaries1 K (cupCochain1_coboundaries1), so it descends through the Z¹/B¹ quotient (Submodule.mapQ).

noncomputable def cupH1 {D K : Divisor X} {f : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (K - D)) :
    𝔘.cechH1 D →ₗ[ℂ] 𝔘.cechH1 K

cupH1_mk

The action of cupH1 on a class [ξ] represented by a cocycle c: cupH1 hf [c] = [f·c].

@[simp] theorem cupH1_mk {D K : Divisor X} {f : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (K - D)) (c : ↥(𝔘.cocycles1 D)) :
    cupH1 hf (Submodule.Quotient.mk c) = Submodule.Quotient.mk (cupCocyclesMap hf c)

globalGerm_add

globalGerm is additive in the meromorphic function.

theorem globalGerm_add {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (f g : MeromorphicFunction X)
    (U : Opens X) :
    globalGerm (f + g) U = globalGerm f U + globalGerm g U

globalGerm_smul

globalGerm is ℂ-homogeneous in the meromorphic function.

theorem globalGerm_smul {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (c : ℂ) (f : MeromorphicFunction X)
    (U : Opens X) :
    globalGerm (c • f) U = c • globalGerm f U

globalGerm_eq_zero_of_germZero

A germ-zero global function has zero germ on every open (orderW f ≡ ⊤ ⟹ globalGerm f U = 0): f.toFun vanishes on a punctured neighbourhood of every point, which transfers to ↥U along the open inclusion.

theorem globalGerm_eq_zero_of_germZero {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {f : MeromorphicFunction X}
    (hf : ∀ x, f.orderW x = ⊤) (U : Opens X) : globalGerm f U = 0

cupH1_add

The cup product is additive in f (over a common cocycle representative): the two cocycle-level maps agree (germ multiplication distributes over globalGerm_add), so the descended maps agree.

theorem cupH1_add {D K : Divisor X} {f g : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (K - D)) (hg : g ∈ linearSystem (X := X) (K - D))
    (hfg : f + g ∈ linearSystem (X := X) (K - D)) (ξ : 𝔘.cechH1 D) :
    cupH1 hfg ξ = cupH1 hf ξ + cupH1 hg ξ

cupH1_smul

The cup product is ℂ-homogeneous in f.

theorem cupH1_smul {D K : Divisor X} (a : ℂ) {f : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (K - D)) (haf : a • f ∈ linearSystem (X := X) (K - D))
    (ξ : 𝔘.cechH1 D) :
    cupH1 haf ξ = a • cupH1 hf ξ

cupH1_eq_zero_of_germZero

A germ-zero f gives the zero cup map (cupH1 = 0): globalGerm f U = 0 so every cochain is multiplied to 0. This is the descent condition for the junk-free lSysModule (K−D) — the cup product depends only on the germ class of f.

theorem cupH1_eq_zero_of_germZero {D K : Divisor X} {f : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (K - D)) (hf0 : ∀ x, f.orderW x = ⊤) (ξ : 𝔘.cechH1 D) :
    cupH1 hf ξ = 0

cupSubtype

The cup product as an ℂ-linear map *in f* on the linear system ↥(linearSystem (K−D)), valued in cechH1 D →ₗ[ℂ] cechH1 K.

noncomputable def cupSubtype (D K : Divisor X) :
    ↥(linearSystem (X := X) (K - D)) →ₗ[ℂ] (𝔘.cechH1 D →ₗ[ℂ] 𝔘.cechH1 K) where

cup

The bundled bilinear cup product cup : lSysModule (K−D) →ₗ[ℂ] (cechH1 D →ₗ[ℂ] cechH1 K). ℂ-linear in f (the junk-free source lSysModule) and in ξ — the algebraic input the Forster §17.5 residue pairing ⟨f, ξ⟩ = Res(f·ω₀·ξ) consumes, with the global residue Res : cechH1 K → ℂ applied afterwards. Descends from cupSubtype because a germ-zero f gives the zero cup map (cupH1_eq_zero_of_germZero), so the cup is well-defined on germ classes.

noncomputable def cup (D K : Divisor X) :
    lSysModule (K - D) →ₗ[ℂ] (𝔘.cechH1 D →ₗ[ℂ] 𝔘.cechH1 K)

cup_mk

@[simp] theorem cup_mk (D K : Divisor X) (f : ↥(linearSystem (X := X) (K - D))) (ξ : 𝔘.cechH1 D) :
    cup D K (Submodule.Quotient.mk f) ξ = cupH1 f.2 ξ