NYLL
Module

DivisorClasses.lean

Nyll.JacobianVarieties.Kummer.DivisorClasses
14 declarations indexed from sourceView source ↗

Module documentation

Divisorial Kummer classes

Functions whose orders are divisible by a positive integer, modulo powers of that integer, identify with the actual torsion subgroup of the degree-zero divisor class group. The map sends a function to its principal divisor divided by the integer. This is the divisor-theoretic part of the Kummer comparison; no identification with etale cohomology is assumed here.

Imports12
Imported by7

Declarations

def

kummerUnits

L37 ↗
AlgebraicCurve.Pic0.kummerUnits
Documentation

Nonzero functions whose orders at every place are divisible by n.

Source context 3 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · full declaration
def kummerUnits (n : ℕ+) : Subgroup Fˣ where
  carrier := {u | ∀ v : Place K F, (n : ℤ) ∣ v.ord (u : F)}
  one_mem' := by
    intro v
    rw [Units.val_one, v.ord_one]
    exact dvd_zero _
  mul_mem' := by
    intro u w hu hw v
    rw [Units.val_mul, v.ord_mul (Units.ne_zero u) (Units.ne_zero w)]
    exact dvd_add (hu v) (hw v)
  inv_mem' := by
    intro u hu v
    rw [Units.val_inv_eq_inv_val, v.ord_inv]
    exact dvd_neg.mpr (hu v)
def

kummerPowers

L53 ↗
AlgebraicCurve.Pic0.kummerPowers
Documentation

The subgroup consisting of actual nth powers of functions.

Source context 3 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · statement
def kummerPowers (n : ℕ+) : Subgroup (kummerUnits K F n)
def

kummerDivisor

L60 ↗
AlgebraicCurve.Pic0.kummerDivisor
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
section PrincipalDivisors
variable {K F} [HasPrincipalDivisors K F]
Lean source · statement
def kummerDivisor (n : ℕ+) (u : kummerUnits K F n) :
    Divisor.degZero (K := K) (F := F)
theorem

kummerDivisor_spec

L65 ↗
AlgebraicCurve.Pic0.kummerDivisor_spec
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
section PrincipalDivisors
variable {K F} [HasPrincipalDivisors K F]
Lean source · statement
theorem kummerDivisor_spec (n : ℕ+) (u : kummerUnits K F n)
    (v : Place K F) :
    v.ord (u.val : F) = (n : ℤ) * (kummerDivisor n u : Divisor K F) v
theorem

kummerDivisor_eq

L71 ↗
AlgebraicCurve.Pic0.kummerDivisor_eq
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
section PrincipalDivisors
variable {K F} [HasPrincipalDivisors K F]
Lean source · statement
theorem kummerDivisor_eq (n : ℕ+) (u : kummerUnits K F n)
    (D : Divisor.degZero (K := K) (F := F))
    (hD : ∀ v : Place K F, v.ord (u.val : F) = (n : ℤ) * (D : Divisor K F) v) :
    kummerDivisor n u = D
theorem

kummerDivisor_one

L81 ↗
AlgebraicCurve.Pic0.kummerDivisor_one
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
section PrincipalDivisors
variable {K F} [HasPrincipalDivisors K F]
Lean source · statement
theorem kummerDivisor_one (n : ℕ+) :
    kummerDivisor n (1 : kummerUnits K F n) = 0
theorem

kummerDivisor_mul

L88 ↗
AlgebraicCurve.Pic0.kummerDivisor_mul
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
section PrincipalDivisors
variable {K F} [HasPrincipalDivisors K F]
Lean source · statement
theorem kummerDivisor_mul (n : ℕ+) (u w : kummerUnits K F n) :
    kummerDivisor n (u * w) = kummerDivisor n u + kummerDivisor n w
theorem

kummerDivisor_class_mem

L98 ↗
AlgebraicCurve.Pic0.kummerDivisor_class_mem
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
section PrincipalDivisors
variable {K F} [HasPrincipalDivisors K F]
Lean source · statement
theorem kummerDivisor_class_mem (n : ℕ+) (u : kummerUnits K F n) :
    mk (kummerDivisor n u) ∈ torsion K F n
def

kummerClass

L109 ↗
AlgebraicCurve.Pic0.kummerClass
Documentation

Divide the actual principal divisor by n and take its torsion class.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
section PrincipalDivisors
variable {K F} [HasPrincipalDivisors K F]
Lean source · full declaration
def kummerClass (n : ℕ+) : kummerUnits K F n →* Multiplicative (torsion K F n) where
  toFun u := Multiplicative.ofAdd ⟨mk (kummerDivisor n u), kummerDivisor_class_mem n u⟩
  map_one' := by
    apply congrArg Multiplicative.ofAdd
    apply Subtype.ext
    change mk (kummerDivisor n (1 : kummerUnits K F n)) = 0
    rw [kummerDivisor_one, mk_zero]
  map_mul' u w := by
    apply congrArg Multiplicative.ofAdd
    apply Subtype.ext
    change mk (kummerDivisor n (u * w)) =
      mk (kummerDivisor n u) + mk (kummerDivisor n w)
    rw [kummerDivisor_mul, mk_add]
theorem

kummerClass_eq

L124 ↗
AlgebraicCurve.Pic0.kummerClass_eq
Documentation

The Kummer class is computed by any divisor with the required orders.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
section PrincipalDivisors
variable {K F} [HasPrincipalDivisors K F]
Lean source · statement
theorem kummerClass_eq (n : ℕ+) (u : kummerUnits K F n)
    (D : Divisor.degZero (K := K) (F := F))
    (hD : ∀ v : Place K F, v.ord (u.val : F) = (n : ℤ) * (D : Divisor K F) v) :
    (Multiplicative.toAdd (kummerClass n u)).val = mk D
theorem

kummerClass_surjective

L132 ↗
AlgebraicCurve.Pic0.kummerClass_surjective
Documentation

Every actual torsion class is represented by a function with divisible orders.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
section PrincipalDivisors
variable {K F} [HasPrincipalDivisors K F]
Lean source · statement
theorem kummerClass_surjective (n : ℕ+) :
    Function.Surjective (kummerClass (K := K) (F := F) n)
theorem

kummerClass_ker

L148 ↗
AlgebraicCurve.Pic0.kummerClass_ker
Documentation

Over algebraically closed constants, the kernel consists of actual powers.

Source context 4 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F} [IsAlgClosed K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
Lean source · statement
theorem kummerClass_ker (n : ℕ+) :
    (kummerClass (K := K) (F := F) n).ker = kummerPowers K F n
def

kummerDivisorEquiv

L177 ↗
AlgebraicCurve.Pic0.kummerDivisorEquiv
Documentation

Divisorial Kummer classes are exactly the actual n-torsion in Pic⁰.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F} [IsAlgClosed K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
variable (K F)
Lean source · statement
def kummerDivisorEquiv (n : ℕ+) :
    kummerUnits K F n ⧸ kummerPowers K F n ≃* Multiplicative (torsion K F n)
theorem

kummerDivisorEquiv_mk

L184 ↗
AlgebraicCurve.Pic0.kummerDivisorEquiv_mk
Documentation

The quotient comparison sends a represented function to its divided divisor class.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve.Pic0
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F} [IsAlgClosed K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
variable (K F)
Lean source · statement
theorem kummerDivisorEquiv_mk (n : ℕ+) (u : kummerUnits K F n) :
    kummerDivisorEquiv K F n (QuotientGroup.mk u) = kummerClass n u

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