NYLL
Module

SerrePairing_eq_of_cechH1ToH1_eq.lean

Nyll.AlgebraicCurves.Cohomology.SerrePairing_eq_of_cechH1ToH1_eq
6 declarations indexed from sourceView source ↗

Module documentation

Serre Pairing eq of cech H1To H1 eq

Imports12
Imported by2

Declarations

theorem

ord_nonneg_of_mem_t0

L47 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem_t0
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.SerrePairingCechH1ToH1
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_mem_t0 (v : Place K F) {f : F} (hf : f ∈
  v.toValuationSubring) : 0 ≤ v.ord f
theorem

canonicalDivisorOf_nonneg_of_mem_regularDifferentials_t0

L62 ↗
AlgebraicCurves.Cohomology.Proofs.SerrePairingCechH1ToH1.AlgebraicCurve.canonicalDivisorOf_nonneg_of_mem_regularDifferentials_t0
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.SerrePairingCechH1ToH1
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
section Generic
variable [HasCanonicalLocalResidueKStar K F] [∀ v : Place K F, v.DCoordGenerates] [Nontrivial
  Ω[F⁄K]]
  [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
omit [HasCanonicalLocalResidueKStar K F] [HasPrincipalDivisors K F] in
Lean source · statement
theorem canonicalDivisorOf_nonneg_of_mem_regularDifferentials_t0 {ω : Ω[F⁄K]} (hω0 : ω ≠ 0)
    (hω : ω ∈ regularDifferentials K F) : 0 ≤ canonicalDivisorOf hω0
theorem

serrePairing_apply_mk_eq_weilOfKaehler_t0

L71 ↗
AlgebraicCurves.Cohomology.Proofs.SerrePairingCechH1ToH1.AlgebraicCurve.serrePairing_apply_mk_eq_weilOfKaehler_t0
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.SerrePairingCechH1ToH1
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
section Generic
variable [HasCanonicalLocalResidueKStar K F] [∀ v : Place K F, v.DCoordGenerates] [Nontrivial
  Ω[F⁄K]]
  [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
Lean source · statement
theorem serrePairing_apply_mk_eq_weilOfKaehler_t0 (hRT : ResidueTheorem K F) {S₀ S₁ : Set (Place K
  F)}
    (hcover : S₀ ∪ S₁ = Set.univ) (ω : ↥(regularDifferentials K F)) (hω : (ω : Ω[F⁄K]) ≠ 0)
    (f : ↥(lSpaceOn (S₀ ∩ S₁) (0 : Divisor K F))) :
    serrePairing hRT hcover ω (Submodule.Quotient.mk f)
      = weilOfKaehler K F hω ⟨((extendOffChart K S₀ (f : F) : ↥(repartitions K F)) : Place K F → F),
          coe_extendOffChart_mem_adeleSpace S₀ (f : F)⟩
theorem

omegaSpace_zero_apply_eq_of_mk_eq

L81 ↗
AlgebraicCurves.Cohomology.Proofs.SerrePairingCechH1ToH1.AlgebraicCurve.omegaSpace_zero_apply_eq_of_mk_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.SerrePairingCechH1ToH1
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
section Generic
variable [HasCanonicalLocalResidueKStar K F] [∀ v : Place K F, v.DCoordGenerates] [Nontrivial
  Ω[F⁄K]]
  [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
omit [HasCanonicalLocalResidueKStar K F] [∀ (v : Place K F), v.DCoordGenerates]
  [Nontrivial Ω[F⁄K]] [HasCanonicalDivisor (K := K) (F := F)] in
Lean source · statement
theorem omegaSpace_zero_apply_eq_of_mk_eq {μ : Module.Dual K ↥(adeleSpace K F)}
    (hμ : μ ∈ omegaSpace (K := K) (F := F) (0 : Divisor K F))
    (a b : ↥(repartitions K F)) (ha : (a : Place K F → F) ∈ adeleSpace K F)
    (hb : (b : Place K F → F) ∈ adeleSpace K F)
    (h : (Submodule.Quotient.mk a : H1 (0 : Divisor K F)) = Submodule.Quotient.mk b) :
    μ ⟨(a : Place K F → F), ha⟩ = μ ⟨(b : Place K F → F), hb⟩
theorem

serrePairing_eq_of_cechH1ToH1_eq'

L108 ↗
AlgebraicCurves.Cohomology.Proofs.SerrePairingCechH1ToH1.AlgebraicCurve.serrePairing_eq_of_cechH1ToH1_eq'
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.SerrePairingCechH1ToH1
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
section Generic
variable [HasCanonicalLocalResidueKStar K F] [∀ v : Place K F, v.DCoordGenerates] [Nontrivial
  Ω[F⁄K]]
  [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
Lean source · statement
theorem serrePairing_eq_of_cechH1ToH1_eq' (hRT : ResidueTheorem K F) {S₀ S₁ T₀ T₁ : Set (Place K F)}
    (hS : S₀ ∪ S₁ = Set.univ) (hT : T₀ ∪ T₁ = Set.univ)
    (ω : ↥(regularDifferentials K F)) (x : cechH1 S₀ S₁ (0 : Divisor K F)) (y : cechH1 T₀ T₁ (0 :
      Divisor K F))
    (h : cechH1ToH1 hS 0 x = cechH1ToH1 hT 0 y) :
    serrePairing hRT hS ω x = serrePairing hRT hT ω y
theorem

serrePairing_eq_of_cechH1ToH1_eq

L133 ↗
AlgebraicCurve.serrePairing_eq_of_cechH1ToH1_eq
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.SerrePairingCechH1ToH1
open KaehlerDifferential
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Cohomology.Proofs.SerrePairingCechH1ToH1.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.serrePairing_eq_of_cechH1ToH1_eq {K : Type*} {F : Type*} [Field K]
  [Field F] [Algebra K F]
    [HasCanonicalLocalResidueKStar K F] [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
    [HasCanonicalDivisor (K := K) (F := F)] [HasPrincipalDivisors K F]
    (hRT : ResidueTheorem K F) {S₀ S₁ T₀ T₁ : Set (Place K F)}
    (hS : S₀ ∪ S₁ = Set.univ) (hT : T₀ ∪ T₁ = Set.univ)
    (ω : ↥(regularDifferentials K F)) (x : cechH1 S₀ S₁ (0 : Divisor K F)) (y : cechH1 T₀ T₁ (0 :
      Divisor K F))
    (h : cechH1ToH1 hS 0 x = cechH1ToH1 hT 0 y) :
    serrePairing hRT hS ω x = serrePairing hRT hT ω y

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