NYLL
Module

DivisorialWeilPairingData_pair_pullbackAlong_eq_pair_pushforwardAlongHom.lean

Nyll.JacobianVarieties.WeilPairing.DivisorialWeilPairingData_pair_pullbackAlong_eq_pair_pushforwardAlongHom
10 declarations indexed from sourceView source ↗

Module documentation

Pullback and norm adjointness in characteristic zero

Disjoint divisor representatives and the existing separable evaluation formula identify the pairing of a pullback with the pairing against the norm class.

Imports7
Imported by1

Declarations

theorem

hratF

L58 ↗
JacobianVarieties.WeilPairing.Proofs.PullPushPairing.AlgebraicCurve.WeilAdjClass.hratF
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.PullPushPairing
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
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilAdjClass
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

normAlong

L62 ↗
JacobianVarieties.WeilPairing.Proofs.PullPushPairing.AlgebraicCurve.WeilAdjClass.normAlong
Documentation

The field norm for the algebra structure determined by the given embedding.

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.PullPushPairing
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
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilAdjClass
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

L66 ↗
JacobianVarieties.WeilPairing.Proofs.PullPushPairing.AlgebraicCurve.WeilAdjClass.ord_map_eq
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.PullPushPairing
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
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilAdjClass
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'

L80 ↗
JacobianVarieties.WeilPairing.Proofs.PullPushPairing.AlgebraicCurve.WeilAdjClass.map_ne_zero'
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.PullPushPairing
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
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilAdjClass
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

L83 ↗
JacobianVarieties.WeilPairing.Proofs.PullPushPairing.AlgebraicCurve.WeilAdjClass.ord_norm_eq
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.PullPushPairing
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
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilAdjClass
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

L98 ↗
JacobianVarieties.WeilPairing.Proofs.PullPushPairing.AlgebraicCurve.WeilAdjClass.normAlong_ne_zero
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.PullPushPairing
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
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilAdjClass
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

L104 ↗
JacobianVarieties.WeilPairing.Proofs.PullPushPairing.AlgebraicCurve.WeilAdjClass.pullbackAlong_eq_zero
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.PullPushPairing
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
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilAdjClass
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

pushforwardAlong_apply_eq_zero

L110 ↗
JacobianVarieties.WeilPairing.Proofs.PullPushPairing.AlgebraicCurve.WeilAdjClass.pushforwardAlong_apply_eq_zero
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.PullPushPairing
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
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilAdjClass
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem pushforwardAlong_apply_eq_zero {u : F →ₐ[K] F'} {hu : u.toRingHom.IsIntegral}
    {B : Divisor K F'} {v : Place K F}
    (h : ∀ w : Place K F', w.restrictAlong u hu = v → B w = 0) :
    Divisor.pushforwardAlong u hu B v = 0
theorem

mk_pullbackAlong_eq

L129 ↗
JacobianVarieties.WeilPairing.Proofs.PullPushPairing.AlgebraicCurve.WeilAdjClass.mk_pullbackAlong_eq
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.PullPushPairing
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
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WeilAdjClass
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem mk_pullbackAlong_eq [HasPrincipalDivisors K F] [HasPrincipalDivisors K F'] (u : F →ₐ[K] F')
    (hu : u.toRingHom.IsIntegral)
    (hFI : FundamentalIdentityAlong K u hu) (D E : Divisor.degZero (K := K) (F := F))
    (h : Pic0.mk D = Pic0.mk E) :
    Pic0.mk (⟨Divisor.pullbackAlong u hu (D : Divisor K F),
        Divisor.pullbackAlong_mem_degZero u hu hFI D.2⟩ :
        Divisor.degZero (K := K) (F := F')) =
      Pic0.mk ⟨Divisor.pullbackAlong u hu (E : Divisor K F),
        Divisor.pullbackAlong_mem_degZero u hu hFI E.2⟩
theorem

pair_pullbackAlong_eq_pair_pushforwardAlongHom

L161 ↗
AlgebraicCurve.DivisorialWeilPairingData.pair_pullbackAlong_eq_pair_pushforwardAlongHom
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurve.DivisorialWeilPairingData
open JacobianVarieties.WeilPairing.Proofs.PullPushPairing.AlgebraicCurve.WeilAdjClass in
open _root_.AlgebraicCurve.WeilDatum in
Lean source · statement
theorem pair_pullbackAlong_eq_pair_pushforwardAlongHom
    {K F : Type*} [Field K] [Field F] [Algebra K F] [IsAlgClosed K] [CharZero K] [IsCurveOver K F]
    {F' : Type*} [Field F'] [Algebra K F'] [IsCurveOver K F']
    (u : F →ₐ[K] F') (hu : u.toRingHom.IsIntegral)
    (hFI : FundamentalIdentityAlong K u hu) (hfin : FiniteAlong K u)
    (hN : NormFormulaAlong K u hfin)
    {n : ℕ} [NeZero n] (e' : DivisorialWeilPairingData K F' n) (e : DivisorialWeilPairingData K F n)
    (x : Pic0 K F) (hx : (n : ℤ) • x = 0)
    (y : Pic0 K F') (hy : (n : ℤ) • y = 0)
    (D₀ : Divisor.degZero (K := K) (F := F)) (hD₀ : Pic0.mk D₀ = x)
    (x' : Pic0 K F') (hx'def : x' = Pic0.mk ⟨Divisor.pullbackAlong u hu (D₀ : Divisor K F),
        Divisor.pullbackAlong_mem_degZero u hu hFI D₀.2⟩) (hx' : (n : ℤ) • x' = 0)
    (hy₀ : (n : ℤ) • Pic0.pushforwardAlongHom u hu hfin hN y = 0) :
    e'.pair ⟨x', Pic0.mem_torsion.mpr hx'⟩ ⟨y, Pic0.mem_torsion.mpr hy⟩
      = e.pair ⟨x, Pic0.mem_torsion.mpr hx⟩
        ⟨Pic0.pushforwardAlongHom u hu hfin hN y, Pic0.mem_torsion.mpr hy₀⟩

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