Construct torsion classes from disjoint divisor data and prove the pairing laws from divisor evaluation and Weil reciprocity. A moving property provides simultaneous representatives; perfection is separately supplied when producing the duality equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Divisortheorem evalFun_one (D : Divisor K F) : evalFun (1 : F) D = 1Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ}theorem isPrincipal_smul_left (d : WeilDatum K F n) :
Divisor.IsPrincipal ((n : ℤ) • d.D₁)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ}theorem isPrincipal_smul_right (d : WeilDatum K F n) :
Divisor.IsPrincipal ((n : ℤ) • d.D₂)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ}theorem degree_D₁_eq_zero (d : WeilDatum K F n) [HasPrincipalDivisors K F] (hn : n ≠ 0) :
Divisor.degree d.D₁ = 0Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ}theorem degree_D₂_eq_zero (d : WeilDatum K F n) [HasPrincipalDivisors K F] (hn : n ≠ 0) :
Divisor.degree d.D₂ = 0The first divisor of a Weil datum, with its proved degree-zero property.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]def degZeroLeft (d : WeilDatum K F n) : Divisor.degZero (K := K) (F := F)The second divisor of a Weil datum, with its proved degree-zero property.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]def degZeroRight (d : WeilDatum K F n) : Divisor.degZero (K := K) (F := F)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]theorem coe_degZeroLeft (d : WeilDatum K F n) :
(d.degZeroLeft : Divisor K F) = d.D₁Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]theorem coe_degZeroRight (d : WeilDatum K F n) :
(d.degZeroRight : Divisor K F) = d.D₂Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
omit [NeZero n] [HasPrincipalDivisors K F] intheorem mk_mem_torsion (D : Divisor.degZero (K := K) (F := F))
(h : Divisor.IsPrincipal ((n : ℤ) • (D : Divisor K F))) :
Pic0.mk D ∈ Pic0.torsion K F nThe torsion class of the first divisor of a Weil datum.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]def classLeft (d : WeilDatum K F n) : Pic0.torsion K F nThe torsion class of the second divisor of a Weil datum.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]def classRight (d : WeilDatum K F n) : Pic0.torsion K F nSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]theorem coe_classLeft (d : WeilDatum K F n) :
(d.classLeft : Pic0 K F) = Pic0.mk d.degZeroLeftSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]theorem coe_classRight (d : WeilDatum K F n) :
(d.classRight : Pic0 K F) = Pic0.mk d.degZeroRightSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]theorem classLeft_symm (d : WeilDatum K F n) : d.symm.classLeft = d.classRightSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]theorem classRight_symm (d : WeilDatum K F n) : d.symm.classRight = d.classLeftSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]theorem classLeft_addLeft (d d' : WeilDatum K F n) (hD : d.D₂ = d'.D₂) (hf : d.f₂ = d'.f₂) :
(d.addLeft d' hD hf).classLeft = d.classLeft + d'.classLeftSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]theorem classRight_addLeft (d d' : WeilDatum K F n) (hD : d.D₂ = d'.D₂) (hf : d.f₂ = d'.f₂) :
(d.addLeft d' hD hf).classRight = d.classRightSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem ord_f₁_eq_zero_of_mem_support {v : Place K F} (hv : v ∈ d.D₂.support) :
v.ord d.f₁ = 0Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem ord_f₂_eq_zero_of_mem_support {v : Place K F} (hv : v ∈ d.D₁.support) :
v.ord d.f₂ = 0Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem rational_of_mem_support_left {v : Place K F} (hv : v ∈ d.D₁.support) :
v.IsRationalSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem rational_of_mem_support_right {v : Place K F} (hv : v ∈ d.D₂.support) :
v.IsRationalSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem evalAt_f₁_ne_zero {v : Place K F} (hv : v ∈ d.D₂.support) :
v.evalAt d.f₁ ≠ 0Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem evalAt_f₂_ne_zero {v : Place K F} (hv : v ∈ d.D₁.support) :
v.evalAt d.f₂ ≠ 0Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section GaloisAction
open scoped Pointwise
namespace Place
variable (σ : F ≃ₐ[K] F) (v : Place K F)theorem mem_smul_toValuationSubring_iff (f : F) :
σ f ∈ (σ • v).toValuationSubring ↔ f ∈ v.toValuationSubringSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section GaloisAction
open scoped Pointwise
namespace Place
variable (σ : F ≃ₐ[K] F) (v : Place K F)theorem isRational_smul (hv : v.IsRational) : (σ • v).IsRationalSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section GaloisAction
open scoped Pointwise
namespace Place
variable (σ : F ≃ₐ[K] F) (v : Place K F)theorem residue_smul {f : F} (hf : f ∈ v.toValuationSubring) :
residue (σ • v).toValuationSubring
(⟨σ f, (mem_smul_toValuationSubring_iff σ v f).mpr hf⟩ :
(σ • v).toValuationSubring)
= smulResidueAlgEquiv σ v (residue v.toValuationSubring ⟨f, hf⟩)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section GaloisAction
open scoped Pointwise
namespace Place
variable (σ : F ≃ₐ[K] F) (v : Place K F)theorem evalAt_smul (hv : v.IsRational) {f : F} (hf : f ∈ v.toValuationSubring) :
(σ • v).evalAt (σ f) = v.evalAt fSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section GaloisAction
open scoped Pointwise
namespace Divisor
variable (σ : F ≃ₐ[K] F)theorem evalFun_smul {f : F} (D : Divisor K F)
(hrat : ∀ v ∈ D.support, Place.IsRational v)
(hmem : ∀ v ∈ D.support, f ∈ v.toValuationSubring) :
evalFun (σ f) (σ • D) = evalFun f DTransport the divisors and functions of a Weil datum by a field automorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section GaloisAction
open scoped Pointwise
namespace WeilDatum
variable {n : ℕ} (σ : F ≃ₐ[K] F)def galSmul (d : WeilDatum K F n) : WeilDatum K F n where
D₁ := σ • d.D₁
D₂ := σ • d.D₂
f₁ := σ d.f₁
f₂ := σ d.f₂
f₁_ne_zero := by
exact (_root_.map_ne_zero σ).mpr d.f₁_ne_zero
f₂_ne_zero := by
exact (_root_.map_ne_zero σ).mpr d.f₂_ne_zero
ord_f₁ := by
intro v
rw [show v = σ • (σ⁻¹ • v) from (smul_inv_smul σ v).symm, Place.ord_smul,
Divisor.smul_apply_smul]
exact d.ord_f₁ (σ⁻¹ • v)
ord_f₂ := by
intro v
rw [show v = σ • (σ⁻¹ • v) from (smul_inv_smul σ v).symm, Place.ord_smul,
Divisor.smul_apply_smul]
exact d.ord_f₂ (σ⁻¹ • v)
disjoint := by
intro v
rw [Divisor.smul_apply, Divisor.smul_apply]
exact d.disjoint (σ⁻¹ • v)
rational := by
intro v hv
rw [Divisor.smul_apply, Divisor.smul_apply] at hv
have h1 : (σ⁻¹ • v).IsRational := d.rational (σ⁻¹ • v) hv
have h2 := Place.isRational_smul σ (σ⁻¹ • v) h1
rwa [smul_inv_smul] at h2Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section GaloisAction
open scoped Pointwise
namespace WeilDatum
variable {n : ℕ} (σ : F ≃ₐ[K] F)theorem galSmul_pairing (d : WeilDatum K F n) : (d.galSmul σ).pairing = d.pairingSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section GaloisAction
open scoped Pointwise
namespace WeilDatum
variable {n : ℕ} (σ : F ≃ₐ[K] F)
variable [NeZero n] [HasPrincipalDivisors K F]theorem coe_classLeft_galSmul (d : WeilDatum K F n) :
((d.galSmul σ).classLeft : Pic0 K F) = σ • (d.classLeft : Pic0 K F)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section GaloisAction
open scoped Pointwise
namespace WeilDatum
variable {n : ℕ} (σ : F ≃ₐ[K] F)
variable [NeZero n] [HasPrincipalDivisors K F]theorem coe_classRight_galSmul (d : WeilDatum K F n) :
((d.galSmul σ).classRight : Pic0 K F) = σ • (d.classRight : Pic0 K F)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section GaloisAction
open scoped Pointwisetheorem Pic0.smul_mem_torsion (σ : F ≃ₐ[K] F) {n : ℕ} {x : Pic0 K F}
(hx : x ∈ Pic0.torsion K F n) : σ • x ∈ Pic0.torsion K F nSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ}theorem pairing_eq_of_addPrincipalLeft (hrec : WeilReciprocity K F)
(d d' : WeilDatum K F n) {E : Divisor K F} {h : F} (hh : h ≠ 0)
(hE : ∀ v : Place K F, E v = v.ord h)
(hD₁ : d'.D₁ = d.D₁ + E) (hD₂ : d'.D₂ = d.D₂)
(hf₁ : d'.f₁ = d.f₁ * h ^ (n : ℤ)) (hf₂ : d'.f₂ = d.f₂) :
d'.pairing = d.pairingSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem evalFun_f₁_ne_zero : Divisor.evalFun d.f₁ d.D₂ ≠ 0Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem evalFun_f₂_ne_zero : Divisor.evalFun d.f₂ d.D₁ ≠ 0Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem pairing_ne_zero : d.pairing ≠ 0Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem evalFun_f₁_pow :
Divisor.evalFun d.f₁ d.D₂ ^ n = Divisor.evalFun d.f₁ ((n : ℤ) • d.D₂)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem evalFun_f₂_pow :
Divisor.evalFun d.f₂ d.D₁ ^ n = Divisor.evalFun d.f₂ ((n : ℤ) • d.D₁)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem pairing_pow_eq_one (h : WeilReciprocity K F) : d.pairing ^ n = 1Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem symm_pairing_eq_inv : d.symm.pairing = d.pairing⁻¹Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem pairing_mul_symm_pairing : d.pairing * d.symm.pairing = 1Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
variable {n : ℕ} (d : WeilDatum K F n)theorem addLeft_pairing (d' : WeilDatum K F n) (hD : d.D₂ = d'.D₂) (hf : d.f₂ = d'.f₂) :
(d.addLeft d' hD hf).pairing = d.pairing * d'.pairingA divisorial pairing with compatibility and a moving property for torsion representatives.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) instructure DivisorialWeilPairingData (n : ℕ) [NeZero n] [HasPrincipalDivisors K F] where
/-- The value of the pairing on two torsion classes. -/
pair : Pic0.torsion K F n → Pic0.torsion K F n → K
/-- Agreement with divisor evaluation on each Weil datum. -/
compatible : ∀ d : WeilDatum K F n, pair d.classLeft d.classRight = d.pairing
/-- Choose a rational divisor representative away from a given finite set of places. -/
move : ∀ (x : Pic0.torsion K F n) (S : Finset (Place K F)),
∃ D : Divisor.degZero (K := K) (F := F),
Pic0.mk D = (x : Pic0 K F) ∧
(∀ v ∈ (D : Divisor K F).support, Place.IsRational v) ∧
(∀ v ∈ (D : Divisor K F).support, v ∉ S)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) in
namespace DivisorialWeilPairingData
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (e : DivisorialWeilPairingData K F n)
omit [NeZero n] [HasPrincipalDivisors K F] intheorem exists_witness (x : Pic0.torsion K F n) (D : Divisor.degZero (K := K) (F := F))
(hD : Pic0.mk D = (x : Pic0 K F)) :
∃ f : F, f ≠ 0 ∧ ∀ v : Place K F, v.ord f = n * (D : Divisor K F) vSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) in
namespace DivisorialWeilPairingData
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (e : DivisorialWeilPairingData K F n)
include e intheorem exists_datum (x y : Pic0.torsion K F n) :
∃ d : WeilDatum K F n, d.classLeft = x ∧ d.classRight = ySurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) in
namespace DivisorialWeilPairingData
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (e : DivisorialWeilPairingData K F n)
include e intheorem exists_datum_pair (x x' y : Pic0.torsion K F n) :
∃ d d' : WeilDatum K F n, d.D₂ = d'.D₂ ∧ d.f₂ = d'.f₂ ∧
d.classLeft = x ∧ d'.classLeft = x' ∧ d.classRight = y ∧ d'.classRight = ySurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) in
namespace DivisorialWeilPairingData
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (e : DivisorialWeilPairingData K F n)theorem pair_ne_zero (x y : Pic0.torsion K F n) : e.pair x y ≠ 0Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) in
namespace DivisorialWeilPairingData
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (e : DivisorialWeilPairingData K F n)theorem pair_add_left (x x' y : Pic0.torsion K F n) :
e.pair (x + x') y = e.pair x y * e.pair x' ySurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) in
namespace DivisorialWeilPairingData
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (e : DivisorialWeilPairingData K F n)theorem pair_mul_pair_swap (x y : Pic0.torsion K F n) :
e.pair x y * e.pair y x = 1Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) in
namespace DivisorialWeilPairingData
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (e : DivisorialWeilPairingData K F n)theorem pair_zero_left (y : Pic0.torsion K F n) : e.pair 0 y = 1Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) in
namespace DivisorialWeilPairingData
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (e : DivisorialWeilPairingData K F n)theorem pair_zero_right (x : Pic0.torsion K F n) : e.pair x 0 = 1Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) in
namespace DivisorialWeilPairingData
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (e : DivisorialWeilPairingData K F n)theorem pair_swap_eq_inv (x y : Pic0.torsion K F n) : e.pair y x = (e.pair x y)⁻¹Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) in
namespace DivisorialWeilPairingData
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (e : DivisorialWeilPairingData K F n)theorem pair_add_right (x y y' : Pic0.torsion K F n) :
e.pair x (y + y') = e.pair x y * e.pair x y'Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) in
namespace DivisorialWeilPairingData
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (e : DivisorialWeilPairingData K F n)theorem pair_pow_eq_one (hrec : WeilReciprocity K F) (x y : Pic0.torsion K F n) :
e.pair x y ^ n = 1Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) in
namespace DivisorialWeilPairingData
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (e : DivisorialWeilPairingData K F n)theorem pair_self_eq_one (hrec : WeilReciprocity K F) (hodd : Odd n)
(x : Pic0.torsion K F n) : e.pair x x = 1Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Carrier
variable (K F) in
namespace DivisorialWeilPairingData
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (e : DivisorialWeilPairingData K F n)theorem pair_smul (σ : F ≃ₐ[K] F) (x y : Pic0.torsion K F n) :
e.pair ⟨σ • (x : Pic0 K F), Pic0.smul_mem_torsion σ x.2⟩
⟨σ • (y : Pic0 K F), Pic0.smul_mem_torsion σ y.2⟩ = e.pair x yThe character in the second argument defined by the divisorial pairing.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Bridge
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
namespace DivisorialWeilPairingData
variable (e : DivisorialWeilPairingData K F n)def toChar (x : Pic0.torsion K F n) : HomPic0Gm K F n where
toFun y := e.pair x y
map_zero_eq_one' := e.pair_zero_right x
map_add_eq_mul' y y' := e.pair_add_right x y y'Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Bridge
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
namespace DivisorialWeilPairingData
variable (e : DivisorialWeilPairingData K F n)theorem toChar_apply (x y : Pic0.torsion K F n) : e.toChar x y = e.pair x yThe additive homomorphism to characters defined by the divisorial pairing.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Bridge
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
namespace DivisorialWeilPairingData
variable (e : DivisorialWeilPairingData K F n)def toHom : Pic0.torsion K F n →+ Additive (HomPic0Gm K F n)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Bridge
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
namespace DivisorialWeilPairingData
variable (e : DivisorialWeilPairingData K F n)theorem toHom_apply_apply (x y : Pic0.torsion K F n) :
(Additive.toMul (e.toHom x)) y = e.pair x yPerfection means that the induced homomorphism to characters is bijective.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Bridge
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
namespace DivisorialWeilPairingData
variable (e : DivisorialWeilPairingData K F n)def Perfect : PropThe duality equivalence obtained from a proved perfect divisorial pairing.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Bridge
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
namespace DivisorialWeilPairingData
variable (e : DivisorialWeilPairingData K F n)def toWeilPairingData (h : e.Perfect) : WeilPairingData K F n where
toHom := e.toHom
bijective := hSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Bridge
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
namespace DivisorialWeilPairingData
variable (e : DivisorialWeilPairingData K F n)theorem toWeilPairingData_eval (h : e.Perfect) (x y : Pic0.torsion K F n) :
(e.toWeilPairingData h).eval x y = e.pair x yExistence of divisor representatives defining a perfect Weil pairing.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Bridge
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (K F) indef ExistsPerfectDivisorialWeilPairing (n : ℕ) [NeZero n] : PropSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Bridge
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
variable (K F) intheorem nonempty_weilPairingData_of_existsPerfectDivisorialWeilPairing
(h : ExistsPerfectDivisorialWeilPairing K F n) :
Nonempty (WeilPairingData K F n)