The integral Serre pairing for Čech cochains on a two-chart cover.
The sum of the residue functionals of the Laurent charts.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R) {ι : Type w} [Fintype ι]def residueSum (Λ : ι → 𝒰.LaurentChart) : Ω[𝒰.A01⁄R] →ₗ[R] RSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R) {ι : Type w} [Fintype ι]theorem residueSum_apply (Λ : ι → 𝒰.LaurentChart) (η : Ω[𝒰.A01⁄R]) :
𝒰.residueSum Λ η = ∑ i, (Λ i).residue ηThe residue sum vanishes on the image of the Cech differential.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R) {ι : Type w} [Fintype ι]def ResiduesVanishOnCoboundaries (Λ : ι → 𝒰.LaurentChart) : PropSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R) {ι : Type w} [Fintype ι]theorem residuesVanishOnCoboundaries_iff (Λ : ι → 𝒰.LaurentChart) :
𝒰.ResiduesVanishOnCoboundaries Λ ↔
(∀ ω : Ω[𝒰.A0⁄R], 𝒰.residueSum Λ (𝒰.kaehler.r0 ω) = 0) ∧
∀ ω : Ω[𝒰.A1⁄R], 𝒰.residueSum Λ (𝒰.kaehler.r1 ω) = 0The residue-sum functional descended to first cohomology of differentials.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R) {ι : Type w} [Fintype ι]def kaehlerTrace (Λ : ι → 𝒰.LaurentChart) (hv : 𝒰.ResiduesVanishOnCoboundaries Λ) : 𝒰.kaehler.H1
→ₗ[R] RSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R) {ι : Type w} [Fintype ι]theorem kaehlerTrace_mk (Λ : ι → 𝒰.LaurentChart) (hv : 𝒰.ResiduesVanishOnCoboundaries Λ)
(η : Ω[𝒰.A01⁄R]) :
𝒰.kaehlerTrace Λ hv (Submodule.Quotient.mk η) = ∑ i, (Λ i).residue ηThe two-chart Serre pairing defined by the Laurent-chart residue sum.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R) {ι : Type w} [Fintype ι]def serrePairingInt (Λ : ι → 𝒰.LaurentChart) (hv : 𝒰.ResiduesVanishOnCoboundaries Λ) :
𝒰.kaehler.H0 →ₗ[R] 𝒰.structureSheaf.H1 →ₗ[R] RSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R) {ι : Type w} [Fintype ι]theorem serrePairingInt_apply_mk (Λ : ι → 𝒰.LaurentChart) (hv : 𝒰.ResiduesVanishOnCoboundaries Λ)
(ω : 𝒰.kaehler.H0) (f : 𝒰.A01) :
𝒰.serrePairingInt Λ hv ω (Submodule.Quotient.mk f) = ∑ i, (Λ i).residue (f • 𝒰.kaehler.r0
ω.val.1)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R) {ι : Type w} [Fintype ι]theorem serrePairingInt_apply_mk' (Λ : ι → 𝒰.LaurentChart) (hv : 𝒰.ResiduesVanishOnCoboundaries Λ)
(ω : 𝒰.kaehler.H0) (f : 𝒰.A01) :
𝒰.serrePairingInt Λ hv ω (Submodule.Quotient.mk f) = ∑ i, (Λ i).residue (f • 𝒰.kaehler.r1
ω.val.2)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R) {ι : Type w} [Fintype ι]theorem serrePairingInt_eq_kaehlerTrace_cupProduct (Λ : ι → 𝒰.LaurentChart)
(hv : 𝒰.ResiduesVanishOnCoboundaries Λ) (ω : 𝒰.kaehler.H0) (x : 𝒰.structureSheaf.H1) :
𝒰.serrePairingInt Λ hv ω x = 𝒰.kaehlerTrace Λ hv (𝒰.kaehler.cupProduct ω x)