NYLL
Module

DivisorialWeilPairingData_toHom_injective_of_divisible.lean

Nyll.JacobianVarieties.WeilPairing.DivisorialWeilPairingData_toHom_injective_of_divisible
16 declarations indexed from sourceView source ↗

Module documentation

Injectivity of the divisorial Weil pairing from divisibility over finite function-field extensions. The proof uses Kummer covers and Weil reciprocity to detect each nonzero torsion class.

Imports20
Imported by1

Declarations

theorem

ord_eq_pullback_of_pow_eq_algebraMap

L73 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.Divisor.ord_eq_pullback_of_pow_eq_algebraMap
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section E7
variable {K F L : Type*} [Field K] [Field F] [Field L]
variable [Algebra K F] [Algebra K L] [Algebra F L] [IsScalarTower K F L]
variable [Algebra.IsIntegral F L] [HasPrincipalDivisors K L]
open scoped
  _root_.JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.Divisor in
Lean source · statement
theorem Divisor.ord_eq_pullback_of_pow_eq_algebraMap {n : ℕ} [NeZero n]
    {f : F} {D : Divisor K F} (hfD : ∀ v : Place K F, v.ord f = n * D v)
    {h : L} (hh : h ^ n = algebraMap F L f) :
    ∀ w : Place K L, w.ord h = Divisor.pullback L D w
theorem

exists_mem_support_restrict_eq_of_mem_support_pushforward

L101 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.Divisor.exists_mem_support_restrict_eq_of_mem_support_pushforward
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section PushforwardSupport
variable {K F L : Type*} [Field K] [Field F] [Field L]
variable [Algebra K F] [Algebra K L] [Algebra F L] [IsScalarTower K F L]
variable [Algebra.IsIntegral F L]
open scoped
  _root_.JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.Divisor in
Lean source · statement
theorem Divisor.exists_mem_support_restrict_eq_of_mem_support_pushforward
    (B : Divisor K L) {v : Place K F} (hv : v ∈ (Divisor.pushforward F B).support) :
    ∃ w ∈ B.support, w.restrict F = v
theorem

charZero_of_algebra

L117 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.charZero_of_algebra
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section generic
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem charZero_of_algebra [CharZero K] : CharZero F
theorem

exists_apply_ne_zero_of_mk_ne_zero

L122 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.Divisor.exists_apply_ne_zero_of_mk_ne_zero
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section generic
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped
  _root_.JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.Divisor in
Lean source · statement
theorem Divisor.exists_apply_ne_zero_of_mk_ne_zero
    {D : Divisor.degZero (K := K) (F := F)} (hD : Pic0.mk D ≠ 0) :
    ∃ v : Place K F, (D : Divisor K F) v ≠ 0
theorem

restrict_restrictScalars_smul

L139 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.Place.restrict_restrictScalars_smul
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section generic
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section bare
variable {L : Type*} [Field L] [Algebra K L] [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L]
open scoped
  _root_.JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.Place in
Lean source · statement
theorem Place.restrict_restrictScalars_smul (σ : L ≃ₐ[F] L) (W : Place K L) :
    ((σ.restrictScalars K) • W).restrict F = W.restrict F
theorem

isScalarTower_ratFunc_splittingField

L155 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.isScalarTower_ratFunc_splittingField
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section model
variable {K : Type*} [Field K] [CharZero K]
  {F : Type*} [Field F] [Algebra K F]
  [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]
  (q : F[X])
omit [CharZero K] [FiniteDimensional (RatFunc K) F] in
Lean source · statement
theorem isScalarTower_ratFunc_splittingField :
    IsScalarTower K (RatFunc K) q.SplittingField
theorem

finiteDimensional_ratFunc_splittingField

L164 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.finiteDimensional_ratFunc_splittingField
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section model
variable {K : Type*} [Field K] [CharZero K]
  {F : Type*} [Field F] [Algebra K F]
  [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]
  (q : F[X])
omit [CharZero K] [Algebra K F] [IsScalarTower K (RatFunc K) F] in
Lean source · statement
theorem finiteDimensional_ratFunc_splittingField :
    FiniteDimensional (RatFunc K) q.SplittingField
theorem

hasPrincipalDivisors_splittingField

L168 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.hasPrincipalDivisors_splittingField
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section model
variable {K : Type*} [Field K] [CharZero K]
  {F : Type*} [Field F] [Algebra K F]
  [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]
  (q : F[X])
Lean source · statement
theorem hasPrincipalDivisors_splittingField : HasPrincipalDivisors K q.SplittingField
theorem

isSeparable_splittingField

L176 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.isSeparable_splittingField
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section model
variable {K : Type*} [Field K] [CharZero K]
  {F : Type*} [Field F] [Algebra K F]
  [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]
  (q : F[X])
omit [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] in
include K in
Lean source · statement
theorem isSeparable_splittingField : Algebra.IsSeparable F q.SplittingField
theorem

mem_range_algebraMap_of_pow_eq_one

L184 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.KummerCover.mem_range_algebraMap_of_pow_eq_one
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerCover
Lean source · statement
theorem mem_range_algebraMap_of_pow_eq_one {K L : Type*} [Field K] [Field L]
    [Algebra K L] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity K n]
    {μ : L} (hμ : μ ^ n = 1) : μ ∈ Set.range (algebraMap K L)
theorem

not_mem_range_of_pow_eq

L192 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.KummerCover.not_mem_range_of_pow_eq
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerCover
Lean source · statement
theorem not_mem_range_of_pow_eq {F L : Type*} [Field F] [Field L] [Algebra F L]
    {p : ℕ} {f : F} {α : L} (hf : ∀ g : F, g ^ p ≠ f) (hα : α ^ p = algebraMap F L f) :
    α ∉ Set.range (algebraMap F L)
theorem

exists_pair_ne_one_of_pow_eq_of_smul_eq

L210 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.DivisorialWeilPairingData.exists_pair_ne_one_of_pow_eq_of_smul_eq
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Core
variable {K F L : Type*} [Field K] [Field F] [Field L]
  [Algebra K F] [Algebra K L] [Algebra F L] [IsScalarTower K F L]
namespace DivisorialWeilPairingData
open _root_.AlgebraicCurve.DivisorialWeilPairingData
open _root_.AlgebraicCurve.DivisorialWeilPairingData
Lean source · statement
theorem exists_pair_ne_one_of_pow_eq_of_smul_eq
    {n : ℕ} [NeZero n] [HasPrincipalDivisors K F] [HasPrincipalDivisors K L]
    [FiniteDimensional F L] [Algebra.IsSeparable F L] [CharZero F]
    (e : DivisorialWeilPairingData K F n)
    (hratF : ∀ v : Place K F, v.IsRational) (hratL : ∀ w : Place K L, w.IsRational)
    (hrecL : WeilReciprocity K L)
    (hdiv : ∀ (n : ℤ), n ≠ 0 → ∀ x : Pic0 K L, ∃ y, n • y = x)
    (x : Pic0.torsion K F n) (hx0 : (x : Pic0 K F) ≠ 0)
    {D : Divisor.degZero (K := K) (F := F)} (hD : Pic0.mk D = (x : Pic0 K F))
    {f : F} (hf : f ≠ 0) (hfD : ∀ v : Place K F, v.ord f = n * (D : Divisor K F) v)
    {h : L} (hh : h ^ n = algebraMap F L f)
    {σ : L ≃ₐ[F] L} {ζ : K} (hζ : ζ ≠ 1) (hσ : σ h = algebraMap K L ζ * h) :
    ∃ y : Pic0.torsion K F n, e.pair x y ≠ 1
theorem

exists_pair_ne_one_of_ne_zero_of_kummer

L426 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.DivisorialWeilPairingData.exists_pair_ne_one_of_ne_zero_of_kummer
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Export
universe u v
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
namespace DivisorialWeilPairingData
open _root_.AlgebraicCurve.DivisorialWeilPairingData
open _root_.AlgebraicCurve.DivisorialWeilPairingData
open Polynomial in
Lean source · statement
theorem exists_pair_ne_one_of_ne_zero_of_kummer [IsAlgClosed K] [CharZero K]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]
    [HasPrincipalDivisors K F] {n : ℕ} [NeZero n] (e : DivisorialWeilPairingData K F n)
    (hdiv : ∀ (L' : Type v) [Field L'] [Algebra K L'] [Algebra (RatFunc K) L']
      [IsScalarTower K (RatFunc K) L'] [FiniteDimensional (RatFunc K) L'],
      ∀ (n : ℤ), n ≠ 0 → ∀ x : Pic0 K L', ∃ y, n • y = x)
    (hkum : ∀ f : F, f ≠ 0 → (∀ b : F, b ^ n ≠ f) →
      ∃ (h : (X ^ n - C f).SplittingField)
        (σ : (X ^ n - C f).SplittingField ≃ₐ[F] (X ^ n - C f).SplittingField) (ζ : K),
        ζ ≠ 1 ∧ h ^ n = algebraMap F (X ^ n - C f).SplittingField f ∧
          σ h = algebraMap K (X ^ n - C f).SplittingField ζ * h)
    (x : Pic0.torsion K F n) (hx0 : x ≠ 0) :
    ∃ y : Pic0.torsion K F n, e.pair x y ≠ 1
theorem

toHom_injective_of_forall_exists_pair_ne_one

L454 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.DivisorialWeilPairingData.toHom_injective_of_forall_exists_pair_ne_one
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Export
universe u v
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
namespace DivisorialWeilPairingData
open _root_.AlgebraicCurve.DivisorialWeilPairingData
open _root_.AlgebraicCurve.DivisorialWeilPairingData
variable [HasPrincipalDivisors K F] {n : ℕ} [NeZero n]
Lean source · statement
theorem toHom_injective_of_forall_exists_pair_ne_one (e : DivisorialWeilPairingData K F n)
    (hdet : ∀ x : Pic0.torsion K F n, x ≠ 0 → ∃ y, e.pair x y ≠ 1) :
    Function.Injective e.toHom
theorem

exists_root_aut_eq_const_mul

L469 ↗
JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve.KummerCover.exists_root_aut_eq_const_mul
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Export
universe u v
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
open Polynomial in
Lean source · statement
theorem KummerCover.exists_root_aut_eq_const_mul [IsAlgClosed K] [CharZero K] {n : ℕ}
    [NeZero n]
    {f : F} (hf : f ≠ 0) (hnp : ∀ b : F, b ^ n ≠ f) :
    ∃ (h : (X ^ n - C f).SplittingField)
      (σ : (X ^ n - C f).SplittingField ≃ₐ[F] (X ^ n - C f).SplittingField) (ζ : K),
      ζ ≠ 1 ∧ h ^ n = algebraMap F (X ^ n - C f).SplittingField f ∧
        σ h = algebraMap K (X ^ n - C f).SplittingField ζ * h
theorem

toHom_injective_of_divisible

L510 ↗
AlgebraicCurve.DivisorialWeilPairingData.toHom_injective_of_divisible
Documentation

Divisibility over finite extensions makes the divisorial Weil pairing injective.

Source context 6 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
  AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
open _root_.AlgebraicCurve
  _root_.JacobianVarieties.WeilPairing.Proofs.DivisiblePairingInjection.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.DivisorialWeilPairingData.toHom_injective_of_divisible.{u, v} {K :
  Type u} {F : Type v} [Field K] [Field F] [Algebra K F] [IsAlgClosed K] [CharZero K]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]
    [HasPrincipalDivisors K F] {n : ℕ} [NeZero n]
    (hdiv : ∀ (L' : Type v) [Field L'] [Algebra K L'] [Algebra (RatFunc K) L']
      [IsScalarTower K (RatFunc K) L'] [FiniteDimensional (RatFunc K) L'],
      ∀ (n : ℤ), n ≠ 0 → ∀ x : Pic0 K L', ∃ y, n • y = x)
    (e : DivisorialWeilPairingData K F n) : Function.Injective e.toHom

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