NYLL
Module

DivisorialWeilPairingData_pair_correspondence_eq_pair_correspondence.lean

Nyll.JacobianVarieties.WeilPairing.DivisorialWeilPairingData_pair_correspondence_eq_pair_correspondence
12 declarations indexed from sourceView source ↗

Module documentation

Adjointness of divisor correspondences for the Weil pairing

Move divisor representatives apart and compare evaluation after pullback and norm.

Imports9
Imported by1

Declarations

theorem

isRational_engine

L59 ↗
JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing.AlgebraicCurve.WC8Sol.isRational_engine
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC8Sol
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem isRational_engine [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [IsAlgClosed K] [IsCurveOver K F] (w : Place K F') :
    w.IsRational
theorem

hratF

L70 ↗
JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing.AlgebraicCurve.WC8Sol.hratF
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC8Sol
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem hratF [IsAlgClosed K] [IsCurveOver K F] (v : Place K F) : v.IsRational
def

Uset

L76 ↗
JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing.AlgebraicCurve.WC8Sol.Uset
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC8Sol
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section UsetSec
open Classical in
Lean source · statement
def Uset [HasPrincipalDivisors K F'] (φ ψ : F →ₐ[K] F')
    (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (S : Finset (Place K F)) : Finset (Place K F)
theorem

mem_Uset_of

L81 ↗
JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing.AlgebraicCurve.WC8Sol.mem_Uset_of
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC8Sol
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section UsetSec
Lean source · statement
theorem mem_Uset_of [HasPrincipalDivisors K F'] {φ ψ : F →ₐ[K] F'}
    {hφ : φ.toRingHom.IsIntegral} {hψ : ψ.toRingHom.IsIntegral}
    {S : Finset (Place K F)} {w : Place K F'} (hw : w.restrictAlong ψ hψ ∈ S) :
    w.restrictAlong φ hφ ∈ Uset φ ψ hφ hψ S
def

normAlong

L90 ↗
JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing.AlgebraicCurve.WC8Sol.normAlong
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC8Sol
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
def normAlong (u : F →ₐ[K] F') (g : F') : F
theorem

ord_map_eq

L94 ↗
JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing.AlgebraicCurve.WC8Sol.ord_map_eq
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC8Sol
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem ord_map_eq [HasPrincipalDivisors K F'] (u : F →ₐ[K] F')
    (hu : u.toRingHom.IsIntegral) {n : ℕ} {a : F} {A : Divisor K F}
    (ha : ∀ v : Place K F, v.ord a = n * A v) (w : Place K F') :
    w.ord (u a) = n * (Divisor.pullbackAlong u hu A) w
theorem

map_ne_zero'

L108 ↗
JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing.AlgebraicCurve.WC8Sol.map_ne_zero'
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC8Sol
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem map_ne_zero' (u : F →ₐ[K] F') {a : F} (ha : a ≠ 0) : u a ≠ 0
theorem

ord_norm_eq

L111 ↗
JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing.AlgebraicCurve.WC8Sol.ord_norm_eq
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC8Sol
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem ord_norm_eq [HasPrincipalDivisors K F'] (u : F →ₐ[K] F')
    (hu : u.toRingHom.IsIntegral) (hfin : FiniteAlong K u)
    (hN : NormFormulaAlong K u hfin) {n : ℕ} {g : F'} (hg : g ≠ 0) {D' : Divisor K F'}
    (hD' : ∀ w : Place K F', w.ord g = n * D' w) (v : Place K F) :
    v.ord (normAlong u g) = n * (Divisor.pushforwardAlong u hu D') v
theorem

normAlong_ne_zero

L126 ↗
JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing.AlgebraicCurve.WC8Sol.normAlong_ne_zero
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC8Sol
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem normAlong_ne_zero (u : F →ₐ[K] F') (hfin : FiniteAlong K u)
    {g : F'} (hg : g ≠ 0) : normAlong u g ≠ 0
theorem

pullbackAlong_eq_zero

L132 ↗
JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing.AlgebraicCurve.WC8Sol.pullbackAlong_eq_zero
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC8Sol
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem pullbackAlong_eq_zero [HasPrincipalDivisors K F'] {u : F →ₐ[K] F'}
    {hu : u.toRingHom.IsIntegral} {A : Divisor K F} {w : Place K F'}
    (hA : A (w.restrictAlong u hu) = 0) :
    Divisor.pullbackAlong u hu A w = 0
theorem

correspondence_apply_eq_zero

L138 ↗
JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing.AlgebraicCurve.WC8Sol.correspondence_apply_eq_zero
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC8Sol
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem correspondence_apply_eq_zero [HasPrincipalDivisors K F']
    {φ ψ : F →ₐ[K] F'} {hφ : φ.toRingHom.IsIntegral} {hψ : ψ.toRingHom.IsIntegral}
    {A : Divisor K F} {v : Place K F}
    (h : ∀ w : Place K F', w.restrictAlong ψ hψ = v → A (w.restrictAlong φ hφ) = 0) :
    Divisor.correspondence φ ψ hφ hψ A v = 0
theorem

pair_correspondence_eq_pair_correspondence

L166 ↗
AlgebraicCurve.DivisorialWeilPairingData.pair_correspondence_eq_pair_correspondence
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.CorrespondencePairing
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open _root_.AlgebraicCurve
open AlgebraicCurve.WC8Sol in
Lean source · statement
theorem _root_.AlgebraicCurve.DivisorialWeilPairingData.pair_correspondence_eq_pair_correspondence
    {K F : Type*} [Field K] [Field F] [Algebra K F] [IsAlgClosed K] [CharZero K]
    [IsCurveOver K F]
    {F' : Type*} [Field F'] [Algebra K F'] [HasPrincipalDivisors K F']
    (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (hFIφ : FundamentalIdentityAlong K φ hφ) (hfinψ : FiniteAlong K ψ)
    (hNψ : NormFormulaAlong K ψ hfinψ)
    (hFIψ : FundamentalIdentityAlong K ψ hψ) (hfinφ : FiniteAlong K φ)
    (hNφ : NormFormulaAlong K φ hfinφ)
    {n : ℕ} [NeZero n] (e : DivisorialWeilPairingData K F n)
    (x y : Pic0 K F) (hx : (n : ℤ) • x = 0) (hy : (n : ℤ) • y = 0)
    (hcx : (n : ℤ) • Pic0.correspondence φ ψ hφ hψ hFIφ hfinψ hNψ x = 0)
    (hcy : (n : ℤ) • Pic0.correspondence ψ φ hψ hφ hFIψ hfinφ hNφ y = 0) :
    e.pair ⟨Pic0.correspondence φ ψ hφ hψ hFIφ hfinψ hNψ x, Pic0.mem_torsion.mpr hcx⟩
        ⟨y, Pic0.mem_torsion.mpr hy⟩
      = e.pair ⟨x, Pic0.mem_torsion.mpr hx⟩
          ⟨Pic0.correspondence ψ φ hψ hφ hFIψ hfinφ hNφ y, Pic0.mem_torsion.mpr hcy⟩

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