Module

HasPrincipalDivisors_of_finiteDimensional_of_isSeparable_of_hasPrincipalDivisors.lean

Nyll.JacobianVarieties.WeilPairing.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable_of_hasPrincipalDivisors

14 declarations indexed from sourceView source ↗

Module documentation

Principal divisors in finite separable extensions

Bound the support of valuations by the coefficients of minimal polynomials. The resulting divisor pushes forward to the norm divisor, so its degree is zero.

Imports9

Imported by2

def

badOf

L50 ↗

JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal.AlgebraicCurve.HPDSepExt.badOf

Documentation

The finite support of a principal divisor of a nonzero coefficient.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HPDSepExt
open _root_.AlgebraicCurve
open Polynomial
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L]
  [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L] [HasPrincipalDivisors K F]
open Classical in

Lean source · statement

def badOf (c : F) : Finset (Place K F)

theorem

ord_eq_zero_of_not_mem_badOf

L53 ↗

JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal.AlgebraicCurve.HPDSepExt.ord_eq_zero_of_not_mem_badOf

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HPDSepExt
open _root_.AlgebraicCurve
open Polynomial
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L]
  [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L] [HasPrincipalDivisors K F]

Lean source · statement

theorem ord_eq_zero_of_not_mem_badOf {c : F} {v : Place K F} (hv : v ∉ badOf (K := K) c)
    (hc : c ≠ 0) : v.ord c = 0

def

badPoly

L65 ↗

JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal.AlgebraicCurve.HPDSepExt.badPoly

Documentation

Places at which some coefficient of a polynomial may have nonzero order.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HPDSepExt
open _root_.AlgebraicCurve
open Polynomial
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L]
  [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L] [HasPrincipalDivisors K F]
open Classical in

Lean source · statement

def badPoly (P : Polynomial F) : Finset (Place K F)

theorem

coeff_mem_of_not_mem_badPoly

L68 ↗

JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal.AlgebraicCurve.HPDSepExt.coeff_mem_of_not_mem_badPoly

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HPDSepExt
open _root_.AlgebraicCurve
open Polynomial
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L]
  [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L] [HasPrincipalDivisors K F]

Lean source · statement

theorem coeff_mem_of_not_mem_badPoly {P : Polynomial F} {v : Place K F}
    (hv : v ∉ badPoly (K := K) P) (i : ℕ) :
    P.coeff i ∈ v.toValuationSubring

theorem

mem_of_aeval_eq_zero

L80 ↗

JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal.AlgebraicCurve.HPDSepExt.mem_of_aeval_eq_zero

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HPDSepExt
open _root_.AlgebraicCurve
open Polynomial
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L]
  [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L] [HasPrincipalDivisors K F]
omit [FiniteDimensional F L] in

Lean source · statement

theorem mem_of_aeval_eq_zero {P : Polynomial F} (hP : P.Monic) {x : L} (hx : aeval x P = 0)
    (w : Place K L)
    (hw : w.restrict F ∉ badPoly (K := K) P) : x ∈ w.toValuationSubring

def

bad

L90 ↗

JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal.AlgebraicCurve.HPDSepExt.bad

Documentation

Exceptional places from the minimal polynomials of an element and its inverse.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HPDSepExt
open _root_.AlgebraicCurve
open Polynomial
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L]
  [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L] [HasPrincipalDivisors K F]
open Classical in

Lean source · statement

def bad (g : L) :
    Finset (Place K F)

theorem

ord_eq_zero_of_restrict_not_mem_bad

L93 ↗

JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal.AlgebraicCurve.HPDSepExt.ord_eq_zero_of_restrict_not_mem_bad

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HPDSepExt
open _root_.AlgebraicCurve
open Polynomial
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L]
  [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L] [HasPrincipalDivisors K F]

Lean source · statement

theorem ord_eq_zero_of_restrict_not_mem_bad {g : L} (_hg : g ≠ 0) (w : Place K L)
    (hw : w.restrict F ∉ bad (K := K) (F := F) g) :
    w.ord g = 0

def

suppOf

L112 ↗

JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal.AlgebraicCurve.HPDSepExt.suppOf

Documentation

Places above the finite exceptional set of the element and its inverse.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HPDSepExt
open _root_.AlgebraicCurve
open Polynomial
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L]
  [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L] [HasPrincipalDivisors K F]
open Classical in

Lean source · statement

def suppOf (g : L) : Finset (Place K L)

theorem

mem_suppOf_of_ord_ne_zero

L114 ↗

JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal.AlgebraicCurve.HPDSepExt.mem_suppOf_of_ord_ne_zero

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HPDSepExt
open _root_.AlgebraicCurve
open Polynomial
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L]
  [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L] [HasPrincipalDivisors K F]

Lean source · statement

theorem mem_suppOf_of_ord_ne_zero {g : L} (hg : g ≠ 0) {w : Place K L} (hw : w.ord g ≠ 0) :
    w ∈ suppOf (K := K) (F := F) g

def

divOf

L127 ↗

JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal.AlgebraicCurve.HPDSepExt.divOf

Documentation

The divisor with coefficients given by the orders of a nonzero element.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HPDSepExt
open _root_.AlgebraicCurve
open Polynomial
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L]
  [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L] [HasPrincipalDivisors K F]
open Classical in

Lean source · statement

def divOf {g : L} (hg : g ≠ 0) : Divisor K L

theorem

divOf_apply

L131 ↗

JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal.AlgebraicCurve.HPDSepExt.divOf_apply

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HPDSepExt
open _root_.AlgebraicCurve
open Polynomial
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L]
  [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L] [HasPrincipalDivisors K F]

Lean source · statement

theorem divOf_apply {g : L} (hg : g ≠ 0) (w : Place K L) :
    divOf (K := K) (F := F) hg w = w.ord g

theorem

pushforward_divOf_apply

L135 ↗

JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal.AlgebraicCurve.HPDSepExt.pushforward_divOf_apply

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HPDSepExt
open _root_.AlgebraicCurve
open Polynomial
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L]
  [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L] [HasPrincipalDivisors K F]

Lean source · statement

theorem pushforward_divOf_apply {g : L} (hg : g ≠ 0) (v : Place K F) :
    Divisor.pushforward F (divOf (K := K) (F := F) hg) v = v.ord (Algebra.norm F g)

theorem

degree_divOf

L155 ↗

JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal.AlgebraicCurve.HPDSepExt.degree_divOf

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.WeilPairing.Proofs.FiniteSeparablePrincipal
open _root_.AlgebraicCurve
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace HPDSepExt
open _root_.AlgebraicCurve
open Polynomial
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L]
  [Algebra F L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L] [HasPrincipalDivisors K F]

Lean source · statement

theorem degree_divOf {g : L} (hg : g ≠ 0) : Divisor.degree (divOf (K := K) (F := F) hg) = 0

theorem