NYLL
Module

WeilDatum_pairing_eq_of_isPrincipal_sub.lean

Nyll.JacobianVarieties.WeilPairing.WeilDatum_pairing_eq_of_isPrincipal_sub
28 declarations indexed from sourceView source ↗

Module documentation

The Weil pairing is unchanged when the defining divisors change by principal divisors.

Imports12
Imported by2

Declarations

theorem

prod_zpow_eq_zpow_sum_i

L43 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.prod_zpow_eq_zpow_sum_i
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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 prod_zpow_eq_zpow_sum_i {c : K} (hc : c ≠ 0) {ι : Type*} (s : Finset ι)
    (m : ι → ℤ) : ∏ i ∈ s, c ^ m i = c ^ (∑ i ∈ s, m i)
theorem

support_zsmul_subset_i

L50 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.support_zsmul_subset_i
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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 support_zsmul_subset_i (c : ℤ) (D : Divisor K F) :
    ((c • D : Divisor K F)).support ⊆ D.support
theorem

isPrincipal_neg_i

L57 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.isPrincipal_neg_i
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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_neg_i {D : Divisor K F} (h : Divisor.IsPrincipal D) :
    Divisor.IsPrincipal (-D)
theorem

isPrincipal_add_i

L63 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.isPrincipal_add_i
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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_add_i {A B : Divisor K F} (hA : Divisor.IsPrincipal A)
    (hB : Divisor.IsPrincipal B) : Divisor.IsPrincipal (A + B)
theorem

isPrincipal_sub_of_mk_eq_i

L70 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.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.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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_algebraMap_of_degree_eq_zero_i

L84 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.evalFun_algebraMap_of_degree_eq_zero_i
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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_algebraMap_of_degree_eq_zero_i {c : K} (hc : c ≠ 0) {D : Divisor K F}
    (hdeg : Divisor.degree D = 0) (hrat : ∀ v ∈ D.support, Place.IsRational v) :
    Divisor.evalFun (algebraMap K F c) D = 1
theorem

isPrincipal_smul_left_i

L108 ↗
AlgebraicCurve.WeilDatum.isPrincipal_smul_left_i
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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

L113 ↗
AlgebraicCurve.WeilDatum.isPrincipal_smul_right_i
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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

L118 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.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.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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

L125 ↗
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.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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

L133 ↗
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.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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

L143 ↗
AlgebraicCurve.WeilDatum.degZeroLeft_i
Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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

L149 ↗
AlgebraicCurve.WeilDatum.degZeroRight_i
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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

L154 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.WeilDatum.coe_degZeroLeft_i
Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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

L157 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.WeilDatum.coe_degZeroRight_i
Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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

L161 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.WeilDatum.mk_mem_torsion_i
Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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

L180 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.WeilDatum.classLeft_i
Documentation

The torsion class represented by the left divisor of the Weil datum.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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 classLeft_i (d : WeilDatum K F n) : Pic0.torsion K F n
def

classRight_i

L185 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.WeilDatum.classRight_i
Documentation

The torsion class represented by the right divisor of the Weil datum.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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 classRight_i (d : WeilDatum K F n) : Pic0.torsion K F n
theorem

ord_f₁_eq_zero_of_mem_support_i

L191 ↗
AlgebraicCurve.WeilDatum.ord_f₁_eq_zero_of_mem_support_i
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.ord_f₁_eq_zero_of_mem_support_i
    (d : WeilDatum K F n) {v : Place K F}
    (hv : v ∈ d.D₂.support) : v.ord d.f₁ = 0
theorem

ord_f₂_eq_zero_of_mem_support_i

L197 ↗
AlgebraicCurve.WeilDatum.ord_f₂_eq_zero_of_mem_support_i
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.ord_f₂_eq_zero_of_mem_support_i
    (d : WeilDatum K F n) {v : Place K F}
    (hv : v ∈ d.D₁.support) : v.ord d.f₂ = 0
theorem

rational_of_mem_support_left_i

L203 ↗
AlgebraicCurve.WeilDatum.rational_of_mem_support_left_i
Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.rational_of_mem_support_left_i (d : WeilDatum K F n)
    {v : Place K F}
    (hv : v ∈ d.D₁.support) : v.IsRational
theorem

rational_of_mem_support_right_i

L209 ↗
AlgebraicCurve.WeilDatum.rational_of_mem_support_right_i
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.rational_of_mem_support_right_i
    (d : WeilDatum K F n) {v : Place K F}
    (hv : v ∈ d.D₂.support) : v.IsRational
theorem

evalAt_f₁_ne_zero_i

L215 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.WeilDatum.evalAt_f₁_ne_zero_i
Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem evalAt_f₁_ne_zero_i (d : WeilDatum K F n) {v : Place K F}
    (hv : v ∈ d.D₂.support) : v.evalAt d.f₁ ≠ 0
theorem

evalAt_f₂_ne_zero_i

L220 ↗
AlgebraicCurve.WeilDatum.evalAt_f₂_ne_zero_i
Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.evalAt_f₂_ne_zero_i (d : WeilDatum K F n)
    {v : Place K F}
    (hv : v ∈ d.D₁.support) : v.evalAt d.f₂ ≠ 0
theorem

pairing_eq_of_addPrincipalLeft_i

L228 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.WeilDatum.pairing_eq_of_addPrincipalLeft_i
Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem pairing_eq_of_addPrincipalLeft_i (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.pairing
theorem

pairing_eq_of_isPrincipal_sub_left_i

L295 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.WeilDatum.pairing_eq_of_isPrincipal_sub_left_i
Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem pairing_eq_of_isPrincipal_sub_left_i [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)
    (d d' : WeilDatum K F n) (hD₂ : d'.D₂ = d.D₂) (hf₂ : d'.f₂ = d.f₂)
    (hprin : Divisor.IsPrincipal (d'.D₁ - d.D₁)) :
    d'.pairing = d.pairing
theorem

pairing_eq_of_isPrincipal_sub_right_i

L350 ↗
JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub.AlgebraicCurve.WeilDatum.pairing_eq_of_isPrincipal_sub_right_i
Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
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
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
open _root_.AlgebraicCurve.WeilDatum
Lean source · statement
theorem pairing_eq_of_isPrincipal_sub_right_i [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)
    (d d' : WeilDatum K F n) (hD₁ : d'.D₁ = d.D₁) (hf₁ : d'.f₁ = d.f₁)
    (hprin : Divisor.IsPrincipal (d'.D₂ - d.D₂)) :
    d'.pairing = d.pairing
theorem

pairing_eq_of_isPrincipal_sub

L373 ↗
AlgebraicCurve.WeilDatum.pairing_eq_of_isPrincipal_sub
Source context 4 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilDatum_pairing_eq_of_isPrincipal_sub
noncomputable section
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.WeilDatum.pairing_eq_of_isPrincipal_sub {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))
    (d d' : WeilDatum K F n)
    (hL : Divisor.IsPrincipal (d'.D₁ - d.D₁)) (hR : Divisor.IsPrincipal (d'.D₂ - d.D₂)) :
    d'.pairing = d.pairing

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