Module

DivisorialWeilPairingData_toHom_injective_of_divisible_coprime_of_isAlgClosed.lean

Nyll.JacobianVarieties.WeilPairing.DivisorialWeilPairingData_toHom_injective_of_divisible_coprime_of_isAlgClosed

16 declarations indexed from sourceView source ↗

Module documentation

Nondegeneracy of the divisorial Weil pairing

Use a nontrivial Kummer automorphism and moved divisors to detect every nonzero torsion class. Norm evaluation and Weil reciprocity give injectivity of the pairing map.

Imports21

Mathlib.Util.WithWeakNamespace
Nyll.JacobianVarieties.WeilPairing.Divisorial
Nyll.AlgebraicCurves.Divisors.Maps
Nyll.AlgebraicCurves.Divisors.Semilinear
Nyll.AlgebraicCurves.Places.Place_restrict_ofAlgAut_smul
Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_ofAlgAut_smul_place
Nyll.AlgebraicCurves.Places.Place_exists_restrict_eq
Nyll.AlgebraicCurves.Divisors.Pic0_mk_eq_zero_iff
Nyll.AlgebraicCurves.Divisors.Divisor_evalFun_pullback
Nyll.AlgebraicCurves.Divisors.Divisor_evalFun_algebraMap_pushforward
Nyll.AlgebraicCurves.Divisors.Divisor_pushforward_div_of_isSeparable
Nyll.AlgebraicCurves.Places.Place_inertiaDeg_eq_one_of_isRational
Nyll.AlgebraicCurves.Places.Place_isRational_of_isAlgClosed
Nyll.AlgebraicCurves.Geometry.WeilReciprocity_of_isAlgClosed
Nyll.JacobianVarieties.WeilPairing.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable_of_hasPrincipalDivisors
Nyll.JacobianVarieties.Pic0.Pic0_exists_ord_eq_mul_and_forall_pow_ne_of_ne_zero
Mathlib.FieldTheory.KummerExtension
Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
Mathlib.FieldTheory.IsSepClosed
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.FieldTheory.RatFunc.Basic

Imported by3

theorem

ord_eq_pullback_of_pow_eq_algebraMap

L94 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.Divisor.ord_eq_pullback_of_pow_eq_algebraMap

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
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.WeilInjection.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

L121 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.Divisor.exists_mem_support_restrict_eq_of_mem_support_pushforward

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
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.WeilInjection.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

natCast_ne_zero_of_algebra

L137 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.natCast_ne_zero_of_algebra

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
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 natCast_ne_zero_of_algebra {n : ℕ} (hn : (n : K) ≠ 0) : (n : F) ≠ 0

theorem

exists_apply_ne_zero_of_mk_ne_zero

L144 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.Divisor.exists_apply_ne_zero_of_mk_ne_zero

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
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.WeilInjection.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

L160 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.Place.restrict_restrictScalars_smul

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
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.WeilInjection.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

L176 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.isScalarTower_ratFunc_splittingField

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section model
variable {K : Type*} [Field 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 [FiniteDimensional (RatFunc K) F] in

Lean source · statement

theorem isScalarTower_ratFunc_splittingField :
    IsScalarTower K (RatFunc K) q.SplittingField

theorem

finiteDimensional_ratFunc_splittingField

L185 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.finiteDimensional_ratFunc_splittingField

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section model
variable {K : Type*} [Field 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 K F] [IsScalarTower K (RatFunc K) F] in

Lean source · statement

theorem finiteDimensional_ratFunc_splittingField :
    FiniteDimensional (RatFunc K) q.SplittingField

theorem

isSeparable_splittingField

L191 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.isSeparable_splittingField

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section model
variable {K : Type*} [Field 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] [Algebra K F] in

Lean source · statement

theorem isSeparable_splittingField (hq : q.Separable) :
    Algebra.IsSeparable F q.SplittingField

theorem

hasPrincipalDivisors_splittingField

L197 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.hasPrincipalDivisors_splittingField

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
noncomputable section
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section model
variable {K : Type*} [Field 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

Lean source · statement

theorem hasPrincipalDivisors_splittingField [HasPrincipalDivisors K F] (hq : q.Separable) :
    HasPrincipalDivisors K q.SplittingField

theorem

mem_range_algebraMap_of_pow_eq_one

L207 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.KummerCover.mem_range_algebraMap_of_pow_eq_one

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
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

L215 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.KummerCover.not_mem_range_of_pow_eq

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
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

L233 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.DivisorialWeilPairingData.exists_pair_ne_one_of_pow_eq_of_smul_eq

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
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]
    (e : DivisorialWeilPairingData K F n)
    (hratF : ∀ v : Place K F, v.IsRational) (hratL : ∀ w : Place K L, w.IsRational)
    (hrecL : WeilReciprocity K L)
    (hdiv : ∀ 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

L449 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.DivisorialWeilPairingData.exists_pair_ne_one_of_ne_zero_of_kummer

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
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]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]
    [HasPrincipalDivisors K F] {n : ℕ} [NeZero n] (hn : (n : K) ≠ 0)
    (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'],
      ∀ (m : ℤ), (m : K) ≠ 0 → ∀ x : Pic0 K L', ∃ y, m • 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

L480 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.DivisorialWeilPairingData.toHom_injective_of_forall_exists_pair_ne_one

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
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

L496 ↗

JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.KummerCover.exists_root_aut_eq_const_mul

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
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] {n : ℕ} [NeZero n]
    (hn : (n : K) ≠ 0)
    {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_coprime_of_isAlgClosed

L541 ↗

AlgebraicCurve.DivisorialWeilPairingData.toHom_injective_of_divisible_coprime_of_isAlgClosed

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.WeilInjection
attribute [-instance]
  AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
  RatFunc.denom_X_pow
  RatFunc.powerBasisAdjoinXPow_dim
  RatFunc.powerBasisAdjoinXPow_gen
  RatFunc.intDegree_X_pow
  RatFunc.num_X_pow
open
  _root_.JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.DivisorialWeilPairingData
  renaming toHom_injective_of_forall_exists_pair_ne_one → injectiveOfDetects,
    exists_pair_ne_one_of_ne_zero_of_kummer → detectsByKummer in
open _root_.JacobianVarieties.WeilPairing.Proofs.WeilInjection.AlgebraicCurve.KummerCover
  renaming exists_root_aut_eq_const_mul → kummerWitness in
with_weak_namespace _root_.AlgebraicCurve.DivisorialWeilPairingData

Lean source · statement

theorem toHom_injective_of_divisible_coprime_of_isAlgClosed.{u, v}
    {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F] [IsAlgClosed K]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]
    [HasPrincipalDivisors K F] {n : ℕ} [NeZero n] (hn : (n : K) ≠ 0)
    (hdiv : ∀ (L' : Type v) [Field L'] [Algebra K L'] [Algebra (RatFunc K) L']
      [IsScalarTower K (RatFunc K) L'] [FiniteDimensional (RatFunc K) L'],
      ∀ (m : ℤ), (m : K) ≠ 0 → ∀ x : Pic0 K L', ∃ y, m • y = x)
    (e : DivisorialWeilPairingData K F n) : Function.Injective e.toHom

Module documentation

Nondegeneracy of the divisorial Weil pairing

Declarations