NYLL
Module

ConstantExtension.lean

Nyll.JacobianVarieties.WeilPairing.ConstantExtension
7 declarations indexed from sourceView source ↗

Module documentation

Divisorial Weil pairing under algebraically closed constant extension

The actual unique valuation lifts define conorm on divisors and Picard groups. Transporting a Weil datum along those lifts preserves its pairing through the coefficient embedding. Hence the constructed divisorial Weil pairings commute with this actual conorm, without an assumed pairing comparison.

Imports4
Imported by2

Declarations

theorem

ord_map_eq_mul_con

L44 ↗
JacobianVarieties.WeilPairing.ord_map_eq_mul_con
Documentation

The divisor of an extended function is the actual conorm of its divisor.

Source context 7 commands

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

noncomputable section
open AlgebraicCurve
open JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc
namespace JacobianVarieties.WeilPairing
attribute [local instance] IsCurveOver.toHasPrincipalDivisors
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  [IsAlgClosed K] [IsAlgClosed K'] [IsCurveOver K F] [IsCurveOver K' F']
  (hfg : ∃ x : F, Transcendental K x ∧
    FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
omit [IsAlgClosed K'] [IsCurveOver K' F'] in
Lean source · statement
theorem ord_map_eq_mul_con
    (n : ℕ) (D : Divisor K F) (f : F) (hf : f ≠ 0)
    (hdiv : ∀ v : Place K F, v.ord f = (n : ℤ) * D v)
    (v' : Place K' F') :
    v'.ord (algebraMap F F' f) = (n : ℤ) * con hfg hfg' hgen D v'
def

constantExtensionDatum

L59 ↗
JacobianVarieties.WeilPairing.constantExtensionDatum
Documentation

Transport a Weil datum by the actual constant-extension conorm.

Source context 6 commands

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

noncomputable section
open AlgebraicCurve
open JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc
namespace JacobianVarieties.WeilPairing
attribute [local instance] IsCurveOver.toHasPrincipalDivisors
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  [IsAlgClosed K] [IsAlgClosed K'] [IsCurveOver K F] [IsCurveOver K' F']
  (hfg : ∃ x : F, Transcendental K x ∧
    FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · full declaration
def constantExtensionDatum {n : ℕ} (d : WeilDatum K F n) : WeilDatum K' F' n where
  D₁ := con hfg hfg' hgen d.D₁
  D₂ := con hfg hfg' hgen d.D₂
  f₁ := algebraMap F F' d.f₁
  f₂ := algebraMap F F' d.f₂
  f₁_ne_zero := (map_ne_zero _).mpr d.f₁_ne_zero
  f₂_ne_zero := (map_ne_zero _).mpr d.f₂_ne_zero
  ord_f₁ := ord_map_eq_mul_con hfg hfg' hgen n d.D₁ d.f₁ d.f₁_ne_zero d.ord_f₁
  ord_f₂ := ord_map_eq_mul_con hfg hfg' hgen n d.D₂ d.f₂ d.f₂_ne_zero d.ord_f₂
  disjoint := by
    intro v'
    classical
    by_cases hv : ∃ v, lift hfg hfg' hgen v = v'
    · obtain ⟨v, rfl⟩ := hv
      rw [con_apply_lift, con_apply_lift]
      exact d.disjoint v
    · push Not at hv
      exact Or.inl (con_apply_of_forall_ne hfg hfg' hgen d.D₁ v' hv)
  rational := fun v' _ =>
    v'.isRational_iff_deg_eq_one.mpr (IsCurveOver.deg_eq_one_of_isAlgClosed v')
theorem

constantExtensionDatum_pairing

L82 ↗
JacobianVarieties.WeilPairing.constantExtensionDatum_pairing
Documentation

The transported pairing value is the coefficient image of the original value; this follows from actual residue evaluation.

Source context 6 commands

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

noncomputable section
open AlgebraicCurve
open JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc
namespace JacobianVarieties.WeilPairing
attribute [local instance] IsCurveOver.toHasPrincipalDivisors
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  [IsAlgClosed K] [IsAlgClosed K'] [IsCurveOver K F] [IsCurveOver K' F']
  (hfg : ∃ x : F, Transcendental K x ∧
    FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem constantExtensionDatum_pairing {n : ℕ} (d : WeilDatum K F n) :
    (constantExtensionDatum hfg hfg' hgen d).pairing = algebraMap K K' d.pairing
def

constantExtensionTorsion

L107 ↗
JacobianVarieties.WeilPairing.constantExtensionTorsion
Documentation

The actual conorm homomorphism restricted to n-torsion classes.

Source context 6 commands

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

noncomputable section
open AlgebraicCurve
open JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc
namespace JacobianVarieties.WeilPairing
attribute [local instance] IsCurveOver.toHasPrincipalDivisors
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  [IsAlgClosed K] [IsAlgClosed K'] [IsCurveOver K F] [IsCurveOver K' F']
  (hfg : ∃ x : F, Transcendental K x ∧
    FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · full declaration
def constantExtensionTorsion (n : ℕ) : Pic0.torsion K F n →+ Pic0.torsion K' F' n where
  toFun x := ⟨conPic0 hfg hfg' hgen x.1, by
    rw [Pic0.mem_torsion, ← map_zsmul, Pic0.mem_torsion.mp x.2, map_zero]⟩
  map_zero' := Subtype.ext (conPic0 hfg hfg' hgen).map_zero
  map_add' x y := Subtype.ext ((conPic0 hfg hfg' hgen).map_add x.1 y.1)
theorem

constantExtensionDatum_classLeft

L113 ↗
JacobianVarieties.WeilPairing.constantExtensionDatum_classLeft
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
open JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc
namespace JacobianVarieties.WeilPairing
attribute [local instance] IsCurveOver.toHasPrincipalDivisors
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  [IsAlgClosed K] [IsAlgClosed K'] [IsCurveOver K F] [IsCurveOver K' F']
  (hfg : ∃ x : F, Transcendental K x ∧
    FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem constantExtensionDatum_classLeft {n : ℕ} [NeZero n] (d : WeilDatum K F n) :
    (constantExtensionDatum hfg hfg' hgen d).classLeft =
      constantExtensionTorsion hfg hfg' hgen n d.classLeft
theorem

constantExtensionDatum_classRight

L124 ↗
JacobianVarieties.WeilPairing.constantExtensionDatum_classRight
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
open JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc
namespace JacobianVarieties.WeilPairing
attribute [local instance] IsCurveOver.toHasPrincipalDivisors
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  [IsAlgClosed K] [IsAlgClosed K'] [IsCurveOver K F] [IsCurveOver K' F']
  (hfg : ∃ x : F, Transcendental K x ∧
    FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem constantExtensionDatum_classRight {n : ℕ} [NeZero n] (d : WeilDatum K F n) :
    (constantExtensionDatum hfg hfg' hgen d).classRight =
      constantExtensionTorsion hfg hfg' hgen n d.classRight
theorem

pair_constantExtension

L137 ↗
JacobianVarieties.WeilPairing.pair_constantExtension
Documentation

Constructed divisorial Weil pairings commute with the actual conorm under algebraically closed constant extension.

Source context 6 commands

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

noncomputable section
open AlgebraicCurve
open JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc
namespace JacobianVarieties.WeilPairing
attribute [local instance] IsCurveOver.toHasPrincipalDivisors
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  [IsAlgClosed K] [IsAlgClosed K'] [IsCurveOver K F] [IsCurveOver K' F']
  (hfg : ∃ x : F, Transcendental K x ∧
    FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
Lean source · statement
theorem pair_constantExtension {n : ℕ} [NeZero n]
    (w : DivisorialWeilPairingData K F n) (w' : DivisorialWeilPairingData K' F' n)
    (x y : Pic0.torsion K F n) :
    w'.pair (constantExtensionTorsion hfg hfg' hgen n x)
      (constantExtensionTorsion hfg hfg' hgen n y) = algebraMap K K' (w.pair x y)

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