NYLL
Module

SerrePairing.lean

Nyll.AlgebraicCurves.Cohomology.SerrePairing
31 declarations indexed from sourceView source ↗

Module documentation

Serre Pairing

Imports3
Imported by8

Declarations

theorem

ord_nonneg_of_mem_toValuationSubring

L33 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem_toValuationSubring
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
Lean source · statement
theorem ord_nonneg_of_mem_toValuationSubring {f : F} (hf : f ∈ v.toValuationSubring) :
    0 ≤ v.ord f
theorem

mul_eq_zero_or_ord_nonneg

L46 ↗
AlgebraicCurve.Place.mul_eq_zero_or_ord_nonneg
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
Lean source · statement
theorem mul_eq_zero_or_ord_nonneg {f g : F} (hf : f = 0 ∨ 0 ≤ v.ord f) (hg : 0 ≤ v.ord g) :
    f * g = 0 ∨ 0 ≤ v.ord (f * g)
theorem

differentialCoeff_add

L59 ↗
AlgebraicCurve.Place.differentialCoeff_add
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem differentialCoeff_add (ω η : Ω[F⁄K]) :
    v.differentialCoeff (ω + η) = v.differentialCoeff ω + v.differentialCoeff η
theorem

differentialCoeff_smul_algebraMap

L64 ↗
AlgebraicCurve.Place.differentialCoeff_smul_algebraMap
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem differentialCoeff_smul_algebraMap (c : K) (ω : Ω[F⁄K]) :
    v.differentialCoeff (c • ω) = algebraMap K F c * v.differentialCoeff ω
theorem

ord_differentialCoeff_nonneg_of_mem_regularDifferentials

L68 ↗
AlgebraicCurve.Place.ord_differentialCoeff_nonneg_of_mem_regularDifferentials
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem ord_differentialCoeff_nonneg_of_mem_regularDifferentials {ω : Ω[F⁄K]}
    (hω : ω ∈ regularDifferentials K F) : 0 ≤ v.ord (v.differentialCoeff ω)
theorem

eq_zero_or_ord_nonneg_of_mem_lSpaceOn_zero

L76 ↗
AlgebraicCurve.eq_zero_or_ord_nonneg_of_mem_lSpaceOn_zero
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem eq_zero_or_ord_nonneg_of_mem_lSpaceOn_zero {S : Set (Place K F)} {f : F}
    (hf : f ∈ lSpaceOn S (0 : Divisor K F)) {v : Place K F} (hv : v ∈ S) :
    f = 0 ∨ 0 ≤ v.ord f
theorem

coe_extendOffChart_mem_adeleSpace

L82 ↗
AlgebraicCurve.coe_extendOffChart_mem_adeleSpace
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem coe_extendOffChart_mem_adeleSpace [HasPrincipalDivisors K F] (S₀ : Set (Place K F)) (f :
  F) :
    ((extendOffChart K S₀ f : ↥(repartitions K F)) : Place K F → F) ∈ adeleSpace K F
theorem

kaehlerResidueTerm_add_right

L95 ↗
AlgebraicCurve.kaehlerResidueTerm_add_right
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
Lean source · statement
theorem kaehlerResidueTerm_add_right (ω : Ω[F⁄K]) (α β : Place K F → F) (v : Place K F) :
    kaehlerResidueTerm ω (α + β) v = kaehlerResidueTerm ω α v + kaehlerResidueTerm ω β v
theorem

kaehlerResidueTerm_smul_right

L100 ↗
AlgebraicCurve.kaehlerResidueTerm_smul_right
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
Lean source · statement
theorem kaehlerResidueTerm_smul_right (ω : Ω[F⁄K]) (c : K) (α : Place K F → F) (v : Place K F) :
    kaehlerResidueTerm ω (c • α) v = c * kaehlerResidueTerm ω α v
theorem

kaehlerResidueTerm_eq_zero_of_apply_eq_zero

L106 ↗
AlgebraicCurve.kaehlerResidueTerm_eq_zero_of_apply_eq_zero
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
Lean source · statement
theorem kaehlerResidueTerm_eq_zero_of_apply_eq_zero (ω : Ω[F⁄K]) {α : Place K F → F}
    {v : Place K F} (h : α v = 0) : kaehlerResidueTerm ω α v = 0
def

residueSumOffChart

L111 ↗
AlgebraicCurve.residueSumOffChart
Documentation

Sum the residues of the differential against the repartition extended off a chart.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
Lean source · statement
def residueSumOffChart (S₀ : Set (Place K F)) (ω : Ω[F⁄K]) (f : F) : K
theorem

residueSumOffChart_def

L114 ↗
AlgebraicCurve.residueSumOffChart_def
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
Lean source · statement
theorem residueSumOffChart_def (S₀ : Set (Place K F)) (ω : Ω[F⁄K]) (f : F) :
    residueSumOffChart S₀ ω f
      = ∑ᶠ v, kaehlerResidueTerm ω ((extendOffChart K S₀ f : ↥(repartitions K F)) : Place K F → F)
        v
theorem

kaehlerResidueTerm_extendOffChart

L121 ↗
AlgebraicCurve.kaehlerResidueTerm_extendOffChart
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
open Classical in
Lean source · full declaration
theorem kaehlerResidueTerm_extendOffChart (S₀ : Set (Place K F)) (ω : Ω[F⁄K]) (f : F) (v : Place K
  F) :
    kaehlerResidueTerm ω ((extendOffChart K S₀ f : ↥(repartitions K F)) : Place K F → F) v
      = if v ∈ S₀ then 0 else kaehlerResidueTerm ω (diagonalHom K F f) v := by
  classical
  split_ifs with hv
  · exact kaehlerResidueTerm_eq_zero_of_apply_eq_zero ω (coe_extendOffChart_apply_of_mem f hv)
  · unfold kaehlerResidueTerm
    rw [coe_extendOffChart_apply_of_not_mem f hv, diagonalHom_apply]
theorem

kaehlerResidueTerm_add_left

L133 ↗
AlgebraicCurve.kaehlerResidueTerm_add_left
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem kaehlerResidueTerm_add_left (ω η : Ω[F⁄K]) (α : Place K F → F) (v : Place K F) :
    kaehlerResidueTerm (ω + η) α v = kaehlerResidueTerm ω α v + kaehlerResidueTerm η α v
theorem

kaehlerResidueTerm_smul_left

L138 ↗
AlgebraicCurve.kaehlerResidueTerm_smul_left
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem kaehlerResidueTerm_smul_left (c : K) (ω : Ω[F⁄K]) (α : Place K F → F) (v : Place K F) :
    kaehlerResidueTerm (c • ω) α v = c * kaehlerResidueTerm ω α v
theorem

kaehlerResidueTerm_zero_left

L144 ↗
AlgebraicCurve.kaehlerResidueTerm_zero_left
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem kaehlerResidueTerm_zero_left (α : Place K F → F) (v : Place K F) :
    kaehlerResidueTerm (0 : Ω[F⁄K]) α v = 0
theorem

kaehlerResidueTerm_eq_zero_of_regular

L148 ↗
AlgebraicCurve.kaehlerResidueTerm_eq_zero_of_regular
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem kaehlerResidueTerm_eq_zero_of_regular {ω : Ω[F⁄K]} (hω : ω ∈ regularDifferentials K F)
    {α : Place K F → F} {v : Place K F} (hα : α v = 0 ∨ 0 ≤ v.ord (α v)) :
    kaehlerResidueTerm ω α v = 0
theorem

residueSumOffChart_eq_zero_of_mem_lSpaceOn_right

L154 ↗
AlgebraicCurve.residueSumOffChart_eq_zero_of_mem_lSpaceOn_right
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem residueSumOffChart_eq_zero_of_mem_lSpaceOn_right {S₀ S₁ : Set (Place K F)}
    (hcover : S₀ ∪ S₁ = Set.univ) {ω : Ω[F⁄K]} (hω : ω ∈ regularDifferentials K F) {f : F}
    (hf : f ∈ lSpaceOn S₁ (0 : Divisor K F)) : residueSumOffChart S₀ ω f = 0
theorem

residueSumOffChart_eq_finsum_of_mem_lSpaceOn_left

L167 ↗
AlgebraicCurve.residueSumOffChart_eq_finsum_of_mem_lSpaceOn_left
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem residueSumOffChart_eq_finsum_of_mem_lSpaceOn_left {S₀ : Set (Place K F)} {ω : Ω[F⁄K]}
    (hω : ω ∈ regularDifferentials K F) {f : F} (hf : f ∈ lSpaceOn S₀ (0 : Divisor K F)) :
    residueSumOffChart S₀ ω f = ∑ᶠ v, kaehlerResidueTerm ω (diagonalHom K F f) v
theorem

residueSumOffChart_support_finite

L179 ↗
AlgebraicCurve.residueSumOffChart_support_finite
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
variable [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
Lean source · full declaration
theorem residueSumOffChart_support_finite (S₀ : Set (Place K F)) (ω : Ω[F⁄K]) (f : F) :
    (Function.support fun v =>
      kaehlerResidueTerm ω ((extendOffChart K S₀ f : ↥(repartitions K F)) : Place K F → F)
        v).Finite := by
  rcases eq_or_ne ω 0 with rfl | hω
  · refine Set.Finite.subset Set.finite_empty fun v hv => ?_
    exact hv (kaehlerResidueTerm_zero_left _ v)
  · exact kaehlerResidueTerm_support_finite_of_adeleSpace hω (coe_extendOffChart_mem_adeleSpace S₀
      f)
theorem

residueSumOffChart_add_right

L189 ↗
AlgebraicCurve.residueSumOffChart_add_right
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
variable [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
Lean source · statement
theorem residueSumOffChart_add_right (S₀ : Set (Place K F)) (ω : Ω[F⁄K]) (f g : F) :
    residueSumOffChart S₀ ω (f + g) = residueSumOffChart S₀ ω f + residueSumOffChart S₀ ω g
theorem

residueSumOffChart_smul_right

L197 ↗
AlgebraicCurve.residueSumOffChart_smul_right
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
variable [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
Lean source · statement
theorem residueSumOffChart_smul_right (S₀ : Set (Place K F)) (ω : Ω[F⁄K]) (c : K) (f : F) :
    residueSumOffChart S₀ ω (c • f) = c * residueSumOffChart S₀ ω f
theorem

residueSumOffChart_add_left

L204 ↗
AlgebraicCurve.residueSumOffChart_add_left
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
variable [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
Lean source · statement
theorem residueSumOffChart_add_left (S₀ : Set (Place K F)) (ω η : Ω[F⁄K]) (f : F) :
    residueSumOffChart S₀ (ω + η) f = residueSumOffChart S₀ ω f + residueSumOffChart S₀ η f
theorem

residueSumOffChart_smul_left

L211 ↗
AlgebraicCurve.residueSumOffChart_smul_left
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
variable [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
Lean source · statement
theorem residueSumOffChart_smul_left (S₀ : Set (Place K F)) (c : K) (ω : Ω[F⁄K]) (f : F) :
    residueSumOffChart S₀ (c • ω) f = c * residueSumOffChart S₀ ω f
def

residueSumOffChartLinear

L218 ↗
AlgebraicCurve.residueSumOffChartLinear
Documentation

The residue sum off a chart as a linear functional on the function field.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
variable [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
Lean source · full declaration
def residueSumOffChartLinear (S₀ : Set (Place K F)) (ω : Ω[F⁄K]) : F →ₗ[K] K where
  toFun := residueSumOffChart S₀ ω
  map_add' := residueSumOffChart_add_right S₀ ω
  map_smul' c f := by rw [RingHom.id_apply, smul_eq_mul, residueSumOffChart_smul_right]
theorem

residueSumOffChartLinear_apply

L223 ↗
AlgebraicCurve.residueSumOffChartLinear_apply
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
variable [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
Lean source · statement
theorem residueSumOffChartLinear_apply (S₀ : Set (Place K F)) (ω : Ω[F⁄K]) (f : F) :
    residueSumOffChartLinear S₀ ω f = residueSumOffChart S₀ ω f
theorem

residueSumOffChart_eq_zero_of_mem_lSpaceOn_left

L226 ↗
AlgebraicCurve.residueSumOffChart_eq_zero_of_mem_lSpaceOn_left
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
variable [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
Lean source · statement
theorem residueSumOffChart_eq_zero_of_mem_lSpaceOn_left (hRT : ResidueTheorem K F)
    {S₀ : Set (Place K F)} {ω : Ω[F⁄K]} (hω : ω ∈ regularDifferentials K F) {f : F}
    (hf : f ∈ lSpaceOn S₀ (0 : Divisor K F)) : residueSumOffChart S₀ ω f = 0
theorem

range_cechDiff_le_ker_residueSumOffChart

L235 ↗
AlgebraicCurve.range_cechDiff_le_ker_residueSumOffChart
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
variable [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
Lean source · statement
theorem range_cechDiff_le_ker_residueSumOffChart (hRT : ResidueTheorem K F)
    {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ) {ω : Ω[F⁄K]}
    (hω : ω ∈ regularDifferentials K F) :
    LinearMap.range (cechDiff S₀ S₁ (0 : Divisor K F))
      ≤ LinearMap.ker ((residueSumOffChartLinear S₀ ω).comp (lSpaceOn (S₀ ∩ S₁) (0 : Divisor K
        F)).subtype)
def

serrePairing

L249 ↗
AlgebraicCurve.serrePairing
Documentation

The residue pairing between regular differentials and two-chart first cohomology.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
variable [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
Lean source · full declaration
def serrePairing (hRT : ResidueTheorem K F) {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ =
  Set.univ) :
    ↥(regularDifferentials K F) →ₗ[K] cechH1 S₀ S₁ (0 : Divisor K F) →ₗ[K] K where
  toFun ω := (LinearMap.range (cechDiff S₀ S₁ (0 : Divisor K F))).liftQ
      ((residueSumOffChartLinear S₀ (ω : Ω[F⁄K])).comp (lSpaceOn (S₀ ∩ S₁) (0 : Divisor K
        F)).subtype)
      (range_cechDiff_le_ker_residueSumOffChart hRT hcover ω.2)
  map_add' ω η := by
    refine Submodule.linearMap_qext _ (LinearMap.ext fun f => ?_)
    change residueSumOffChart S₀ ((ω : Ω[F⁄K]) + η) (f : F)
      = residueSumOffChart S₀ ω f + residueSumOffChart S₀ η f
    exact residueSumOffChart_add_left S₀ ω η f
  map_smul' c ω := by
    refine Submodule.linearMap_qext _ (LinearMap.ext fun f => ?_)
    change residueSumOffChart S₀ (c • (ω : Ω[F⁄K])) (f : F) = c • residueSumOffChart S₀ ω f
    rw [smul_eq_mul]
    exact residueSumOffChart_smul_left S₀ c ω f
theorem

serrePairing_apply_mk

L267 ↗
AlgebraicCurve.serrePairing_apply_mk
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
variable [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
Lean source · statement
theorem serrePairing_apply_mk (hRT : ResidueTheorem K F) {S₀ S₁ : Set (Place K F)}
    (hcover : S₀ ∪ S₁ = Set.univ) (ω : ↥(regularDifferentials K F))
    (f : ↥(lSpaceOn (S₀ ∩ S₁) (0 : Divisor K F))) :
    serrePairing hRT hcover ω (Submodule.Quotient.mk f) = residueSumOffChart S₀ (ω : Ω[F⁄K]) (f :
      F)
theorem

serrePairing_apply_mk_eq_finsum_ite

L275 ↗
AlgebraicCurve.serrePairing_apply_mk_eq_finsum_ite
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
variable [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
open Classical in
Lean source · full declaration
theorem serrePairing_apply_mk_eq_finsum_ite (hRT : ResidueTheorem K F) {S₀ S₁ : Set (Place K F)}
    (hcover : S₀ ∪ S₁ = Set.univ) (ω : ↥(regularDifferentials K F))
    (f : ↥(lSpaceOn (S₀ ∩ S₁) (0 : Divisor K F))) :
    serrePairing hRT hcover ω (Submodule.Quotient.mk f)
      = ∑ᶠ v, if v ∈ S₀ then 0 else kaehlerResidueTerm (ω : Ω[F⁄K]) (diagonalHom K F (f : F)) v
        := by
  rw [serrePairing_apply_mk, residueSumOffChart_def]
  exact finsum_congr fun v => kaehlerResidueTerm_extendOffChart S₀ _ _ v

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.