NYLL
Module

Pic0_torsion_exists_addMonoidHom_eval_eq_pairing.lean

Nyll.JacobianVarieties.Pic0.Pic0_torsion_exists_addMonoidHom_eval_eq_pairing
21 declarations indexed from sourceView source ↗

Module documentation

Torsion evaluation through Weil pairings

Constructs the additive map from torsion divisor classes to characters whose evaluation agrees with the Weil pairing of any representing divisor data.

Imports7
Imported by3

Declarations

theorem

isPrincipal_sub_of_mk_eq_i

L41 ↗
JacobianVarieties.Pic0.Proofs.TorsionEvaluation.AlgebraicCurve.isPrincipal_sub_of_mk_eq_i
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem isPrincipal_sub_of_mk_eq_i {A B : Divisor.degZero (K := K) (F := F)}
    (h : Pic0.mk A = Pic0.mk B) :
    Divisor.IsPrincipal ((A : Divisor K F) - (B : Divisor K F))
theorem

evalFun_one_i

L55 ↗
JacobianVarieties.Pic0.Proofs.TorsionEvaluation.AlgebraicCurve.evalFun_one_i
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem evalFun_one_i (D : Divisor K F) : Divisor.evalFun (1 : F) D = 1
theorem

isPrincipal_smul_left_i

L66 ↗
AlgebraicCurve.WeilDatum.isPrincipal_smul_left_i
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.isPrincipal_smul_left_i (d : WeilDatum K F n) :
    Divisor.IsPrincipal ((n : ℤ) • d.D₁)
theorem

isPrincipal_smul_right_i

L71 ↗
AlgebraicCurve.WeilDatum.isPrincipal_smul_right_i
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.isPrincipal_smul_right_i (d : WeilDatum K F n) :
    Divisor.IsPrincipal ((n : ℤ) • d.D₂)
theorem

degree_eq_zero_of_isPrincipal_i

L76 ↗
JacobianVarieties.Pic0.Proofs.TorsionEvaluation.AlgebraicCurve.WeilDatum.degree_eq_zero_of_isPrincipal_i
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem degree_eq_zero_of_isPrincipal_i [HasPrincipalDivisors K F] {D : Divisor K F}
    (hD : Divisor.IsPrincipal D) : Divisor.degree D = 0
theorem

degree_D₁_eq_zero_i

L83 ↗
AlgebraicCurve.WeilDatum.degree_D₁_eq_zero_i
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.degree_D₁_eq_zero_i [HasPrincipalDivisors K F]
    (d : WeilDatum K F n) (hn : n ≠ 0) :
    Divisor.degree d.D₁ = 0
theorem

degree_D₂_eq_zero_i

L91 ↗
AlgebraicCurve.WeilDatum.degree_D₂_eq_zero_i
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.degree_D₂_eq_zero_i [HasPrincipalDivisors K F]
    (d : WeilDatum K F n) (hn : n ≠ 0) :
    Divisor.degree d.D₂ = 0
def

degZeroLeft_i

L101 ↗
AlgebraicCurve.WeilDatum.degZeroLeft_i
Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
section ClassLayer
variable [NeZero n] [HasPrincipalDivisors K F]
Lean source · statement
def _root_.AlgebraicCurve.WeilDatum.degZeroLeft_i (d : WeilDatum K F n) :
    Divisor.degZero (K := K) (F := F)
def

degZeroRight_i

L106 ↗
AlgebraicCurve.WeilDatum.degZeroRight_i
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
section ClassLayer
variable [NeZero n] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
def _root_.AlgebraicCurve.WeilDatum.degZeroRight_i (d : WeilDatum K F n) :
    Divisor.degZero (K := K) (F := F)
theorem

coe_degZeroLeft_i

L111 ↗
JacobianVarieties.Pic0.Proofs.TorsionEvaluation.AlgebraicCurve.WeilDatum.coe_degZeroLeft_i
Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
section ClassLayer
variable [NeZero n] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem coe_degZeroLeft_i (d : WeilDatum K F n) :
    (d.degZeroLeft_i : Divisor K F) = d.D₁
theorem

coe_degZeroRight_i

L114 ↗
JacobianVarieties.Pic0.Proofs.TorsionEvaluation.AlgebraicCurve.WeilDatum.coe_degZeroRight_i
Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
section ClassLayer
variable [NeZero n] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem coe_degZeroRight_i (d : WeilDatum K F n) :
    (d.degZeroRight_i : Divisor K F) = d.D₂
theorem

mk_mem_torsion_i

L118 ↗
JacobianVarieties.Pic0.Proofs.TorsionEvaluation.AlgebraicCurve.WeilDatum.mk_mem_torsion_i
Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
section ClassLayer
variable [NeZero n] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
omit [NeZero n] [HasPrincipalDivisors K F] in
Lean source · statement
theorem mk_mem_torsion_i (D : Divisor.degZero (K := K) (F := F))
    (h : Divisor.IsPrincipal ((n : ℤ) • (D : Divisor K F))) :
    Pic0.mk D ∈ Pic0.torsion K F n
def

classLeft_i

L136 ↗
AlgebraicCurve.WeilDatum.classLeft_i
Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
section ClassLayer
variable [NeZero n] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
def _root_.AlgebraicCurve.WeilDatum.classLeft_i (d : WeilDatum K F n) :
    Pic0.torsion K F n
def

classRight_i

L142 ↗
AlgebraicCurve.WeilDatum.classRight_i
Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
section ClassLayer
variable [NeZero n] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
def _root_.AlgebraicCurve.WeilDatum.classRight_i (d : WeilDatum K F n) :
    Pic0.torsion K F n
theorem

classLeft_symm_i

L148 ↗
JacobianVarieties.Pic0.Proofs.TorsionEvaluation.AlgebraicCurve.WeilDatum.classLeft_symm_i
Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
section ClassLayer
variable [NeZero n] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem classLeft_symm_i (d : WeilDatum K F n) : d.symm.classLeft_i = d.classRight_i
theorem

classRight_symm_i

L150 ↗
JacobianVarieties.Pic0.Proofs.TorsionEvaluation.AlgebraicCurve.WeilDatum.classRight_symm_i
Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
section ClassLayer
variable [NeZero n] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem classRight_symm_i (d : WeilDatum K F n) : d.symm.classRight_i = d.classLeft_i
theorem

classLeft_addLeft_i

L152 ↗
JacobianVarieties.Pic0.Proofs.TorsionEvaluation.AlgebraicCurve.WeilDatum.classLeft_addLeft_i
Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
section ClassLayer
variable [NeZero n] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem classLeft_addLeft_i (d d' : WeilDatum K F n) (hD : d.D₂ = d'.D₂) (hf : d.f₂ = d'.f₂) :
    (d.addLeft d' hD hf).classLeft_i = d.classLeft_i + d'.classLeft_i
theorem

classRight_addLeft_i

L160 ↗
JacobianVarieties.Pic0.Proofs.TorsionEvaluation.AlgebraicCurve.WeilDatum.classRight_addLeft_i
Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
variable {n : ℕ}
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
section ClassLayer
variable [NeZero n] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem classRight_addLeft_i (d d' : WeilDatum K F n) (hD : d.D₂ = d'.D₂) (hf : d.f₂ = d'.f₂) :
    (d.addLeft d' hD hf).classRight_i = d.classRight_i
theorem

exists_datum_i

L172 ↗
JacobianVarieties.Pic0.Proofs.TorsionEvaluation.AlgebraicCurve.exists_datum_i
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Datum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
Lean source · statement
theorem exists_datum_i
    (hmove : ∀ (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))
    (x y : Pic0.torsion K F n) :
    ∃ d : WeilDatum K F n, d.classLeft_i = x ∧ d.classRight_i = y
theorem

exists_datum_pair_i

L206 ↗
JacobianVarieties.Pic0.Proofs.TorsionEvaluation.AlgebraicCurve.exists_datum_pair_i
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Datum
variable {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
Lean source · statement
theorem exists_datum_pair_i
    (hmove : ∀ (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))
    (x x' y : Pic0.torsion K F n) :
    ∃ d d' : WeilDatum K F n, d.D₂ = d'.D₂ ∧ d.f₂ = d'.f₂ ∧
      d.classLeft_i = x ∧ d'.classLeft_i = x' ∧ d.classRight_i = y ∧ d'.classRight_i = y
theorem

exists_addMonoidHom_eval_eq_pairing

L266 ↗
AlgebraicCurve.Pic0.torsion.exists_addMonoidHom_eval_eq_pairing
Source context 4 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.TorsionEvaluation
noncomputable section
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Pic0.torsion.exists_addMonoidHom_eval_eq_pairing {K F : Type*}
    [Field K] [Field F] [Algebra K F] {n : ℕ} [NeZero n] [HasPrincipalDivisors K F]
    (hrec : WeilReciprocity K F)
    (hconst : ∀ u : F, u ≠ 0 → (∀ v : Place K F, v.ord u = 0) → ∃ c : K, u = algebraMap K F c)
    (hmove : ∀ (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)) :
    ∃ hom : Pic0.torsion K F n →+ Additive (HomPic0Gm K F n),
      ∀ (d : WeilDatum K F n) (x y : Pic0.torsion K F n),
        (∃ E : Divisor.degZero (K := K) (F := F),
          (E : Divisor K F) = d.D₁ ∧ Pic0.mk E = (x : Pic0 K F)) →
        (∃ E : Divisor.degZero (K := K) (F := F),
          (E : Divisor K F) = d.D₂ ∧ Pic0.mk E = (y : Pic0 K F)) →
        (Additive.toMul (hom x)) y = d.pairing

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