NYLL
Module

DivisorialWeilPairingData_pair_semilinearSmul.lean

Nyll.JacobianVarieties.WeilPairing.DivisorialWeilPairingData_pair_semilinearSmul
10 declarations indexed from sourceView source ↗

Module documentation

Semilinear equivariance of the divisorial Weil pairing

Transport rational places, residue evaluations, and divisor witnesses along a semilinear automorphism to compare the resulting Weil pairing values.

Imports2
Imported by1

Declarations

theorem

mem_smul_toValuationSubring_iff

L43 ↗
JacobianVarieties.WeilPairing.Proofs.SemilinearPairing.H1bPort.mem_smul_toValuationSubring_iff
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.SemilinearPairing
open AlgebraicCurve
noncomputable section
open IsLocalRing
namespace H1bPort
open AlgebraicCurve.SemilinearAut
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)
Lean source · statement
theorem mem_smul_toValuationSubring_iff (f : F) :
    g • f ∈ (g • v).toValuationSubring ↔ f ∈ v.toValuationSubring
theorem

isRational_smul

L54 ↗
JacobianVarieties.WeilPairing.Proofs.SemilinearPairing.H1bPort.isRational_smul
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.SemilinearPairing
open AlgebraicCurve
noncomputable section
open IsLocalRing
namespace H1bPort
open AlgebraicCurve.SemilinearAut
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)
Lean source · statement
theorem isRational_smul (hv : v.IsRational) : (g • v).IsRational
theorem

residue_smul

L60 ↗
JacobianVarieties.WeilPairing.Proofs.SemilinearPairing.H1bPort.residue_smul
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.SemilinearPairing
open AlgebraicCurve
noncomputable section
open IsLocalRing
namespace H1bPort
open AlgebraicCurve.SemilinearAut
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)
Lean source · statement
theorem residue_smul {f : F} (hf : f ∈ v.toValuationSubring) :
    residue (g • v).toValuationSubring
        (⟨g • f, (mem_smul_toValuationSubring_iff g v f).mpr hf⟩ :
          (g • v).toValuationSubring)
      = smulResidueRingEquiv g v (residue v.toValuationSubring ⟨f, hf⟩)
theorem

evalAt_smul

L71 ↗
JacobianVarieties.WeilPairing.Proofs.SemilinearPairing.H1bPort.evalAt_smul
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.SemilinearPairing
open AlgebraicCurve
noncomputable section
open IsLocalRing
namespace H1bPort
open AlgebraicCurve.SemilinearAut
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)
Lean source · statement
theorem evalAt_smul (hv : v.IsRational) {f : F} (hf : f ∈ v.toValuationSubring) :
    (g • v).evalAt (g • f) = baseAut g (v.evalAt f)
theorem

evalFun_smul

L80 ↗
JacobianVarieties.WeilPairing.Proofs.SemilinearPairing.H1bPort.evalFun_smul
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.SemilinearPairing
open AlgebraicCurve
noncomputable section
open IsLocalRing
namespace H1bPort
open AlgebraicCurve.SemilinearAut
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)
Lean source · statement
theorem evalFun_smul {f : F} (D : Divisor K F)
    (hrat : ∀ v ∈ D.support, Place.IsRational v)
    (hmem : ∀ v ∈ D.support, f ∈ v.toValuationSubring) :
    Divisor.evalFun (g • f) (g • D) = baseAut g (Divisor.evalFun f D)
def

semilinearSmul

L100 ↗
JacobianVarieties.WeilPairing.Proofs.SemilinearPairing.H1bPort.semilinearSmul
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.SemilinearPairing
open AlgebraicCurve
noncomputable section
open IsLocalRing
namespace H1bPort
open AlgebraicCurve.SemilinearAut
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)
variable {n : ℕ}
Lean source · full declaration
def semilinearSmul (d : WeilDatum K F n) : WeilDatum K F n where
  D₁ := g • d.D₁
  D₂ := g • d.D₂
  f₁ := g • d.f₁
  f₂ := g • d.f₂
  f₁_ne_zero := fun h0 => d.f₁_ne_zero (by
    have h1 : g⁻¹ • (g • d.f₁) = g⁻¹ • (0 : F) := congrArg (g⁻¹ • ·) h0
    rwa [inv_smul_smul, smul_zero] at h1)
  f₂_ne_zero := fun h0 => d.f₂_ne_zero (by
    have h1 : g⁻¹ • (g • d.f₂) = g⁻¹ • (0 : F) := congrArg (g⁻¹ • ·) h0
    rwa [inv_smul_smul, smul_zero] at h1)
  ord_f₁ := by
    intro v
    rw [show v = g • (g⁻¹ • v) from (smul_inv_smul g v).symm, ord_smul,
      divisor_smul_apply_smul]
    exact d.ord_f₁ (g⁻¹ • v)
  ord_f₂ := by
    intro v
    rw [show v = g • (g⁻¹ • v) from (smul_inv_smul g v).symm, ord_smul,
      divisor_smul_apply_smul]
    exact d.ord_f₂ (g⁻¹ • v)
  disjoint := by
    intro v
    rw [divisor_smul_apply, divisor_smul_apply]
    exact d.disjoint (g⁻¹ • v)
  rational := by
    intro v hv
    rw [divisor_smul_apply, divisor_smul_apply] at hv
    have h1 : (g⁻¹ • v).IsRational := d.rational (g⁻¹ • v) hv
    have h2 := isRational_smul g (g⁻¹ • v) h1
    rwa [smul_inv_smul] at h2
theorem

semilinearSmul_pairing

L132 ↗
JacobianVarieties.WeilPairing.Proofs.SemilinearPairing.H1bPort.semilinearSmul_pairing
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.SemilinearPairing
open AlgebraicCurve
noncomputable section
open IsLocalRing
namespace H1bPort
open AlgebraicCurve.SemilinearAut
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)
variable {n : ℕ}
Lean source · statement
theorem semilinearSmul_pairing (d : WeilDatum K F n) :
    (semilinearSmul g d).pairing = baseAut g d.pairing
theorem

coe_classLeft_semilinearSmul

L147 ↗
JacobianVarieties.WeilPairing.Proofs.SemilinearPairing.H1bPort.coe_classLeft_semilinearSmul
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.SemilinearPairing
open AlgebraicCurve
noncomputable section
open IsLocalRing
namespace H1bPort
open AlgebraicCurve.SemilinearAut
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)
variable {n : ℕ}
variable [NeZero n] [HasPrincipalDivisors K F]
Lean source · statement
theorem coe_classLeft_semilinearSmul (d : WeilDatum K F n) :
    ((semilinearSmul g d).classLeft : Pic0 K F) = g • (d.classLeft : Pic0 K F)
theorem

coe_classRight_semilinearSmul

L152 ↗
JacobianVarieties.WeilPairing.Proofs.SemilinearPairing.H1bPort.coe_classRight_semilinearSmul
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.SemilinearPairing
open AlgebraicCurve
noncomputable section
open IsLocalRing
namespace H1bPort
open AlgebraicCurve.SemilinearAut
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)
variable {n : ℕ}
variable [NeZero n] [HasPrincipalDivisors K F]
Lean source · statement
theorem coe_classRight_semilinearSmul (d : WeilDatum K F n) :
    ((semilinearSmul g d).classRight : Pic0 K F) = g • (d.classRight : Pic0 K F)
theorem

pair_semilinearSmul

L159 ↗
AlgebraicCurve.DivisorialWeilPairingData.pair_semilinearSmul
Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.SemilinearPairing
open AlgebraicCurve
noncomputable section
open IsLocalRing
Lean source · statement
theorem _root_.AlgebraicCurve.DivisorialWeilPairingData.pair_semilinearSmul {K F : Type*} [Field K]
    [Field F] [Algebra K F] {n : ℕ} [NeZero n]
    [HasPrincipalDivisors K F]
    (e : DivisorialWeilPairingData K F n) (g : SemilinearAut K F)
    (x y : Pic0.torsion K F n) :
    e.pair (g • x) (g • y) = SemilinearAut.baseAut g (e.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.