NYLL
Module

CurveCover.lean

Nyll.JacobianVarieties.Kummer.CurveCover
9 declarations indexed from sourceView source ↗

Module documentation

Finite etale Kummer covers of actual curve models

Divisibility of every valuation order supplies local expressions as a unit times an nth power. Compactness supplies the finite cover required by the concrete normalization theorem. The result is the actual normalization in the Kummer root algebra, with no irreducibility or connectedness assumption on that algebra.

Imports13
Imported by5

Declarations

theorem

ord_pow

L40 ↗
AlgebraicCurve.CurveModel.ord_pow
Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
universe u v
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
Lean source · statement
theorem ord_pow (v : Place K F) (a : F) (n : ℕ) :
    v.ord (a ^ n) = (n : ℤ) * v.ord a
theorem

ffEquiv_mem_stalk_range

L44 ↗
AlgebraicCurve.CurveModel.ffEquiv_mem_stalk_range
Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
universe u v
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
Lean source · statement
theorem ffEquiv_mem_stalk_range (M : CurveModel K F) (x : closedPoints M.C)
    (a : F) (ha : a ∈ (M.placeOfPoint x).toValuationSubring) :
    M.ffEquiv a ∈ (algebraMap (M.C.presheaf.stalk x.val) M.C.functionField).range
theorem

exists_stalk_kummer_unit

L54 ↗
AlgebraicCurve.CurveModel.exists_stalk_kummer_unit
Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
universe u v
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
Lean source · statement
theorem exists_stalk_kummer_unit (M : CurveModel K F) (n : ℕ+)
    (u : Pic0.kummerUnits K F n) (x : M.C) :
    ∃ h : M.C.functionField, h ≠ 0 ∧
      M.ffEquiv (u.val : F) / h ^ (n : ℕ) ∈
        (algebraMap (M.C.presheaf.stalk x) M.C.functionField).range ∧
      h ^ (n : ℕ) / M.ffEquiv (u.val : F) ∈
        (algebraMap (M.C.presheaf.stalk x) M.C.functionField).range
theorem

exists_open_stalk_ranges

L105 ↗
AlgebraicCurve.CurveModel.exists_open_stalk_ranges
Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
universe u v
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
Lean source · statement
theorem exists_open_stalk_ranges {X : Scheme.{u}} [IsIntegral X]
    (x : X) (a b : X.functionField)
    (ha : a ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range)
    (hb : b ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range) :
    ∃ U : X.Opens, x ∈ U ∧ ∀ y ∈ U,
      a ∈ (algebraMap (X.presheaf.stalk y) X.functionField).range ∧
      b ∈ (algebraMap (X.presheaf.stalk y) X.functionField).range
theorem

exists_kummer_unit_cover

L129 ↗
AlgebraicCurve.CurveModel.exists_kummer_unit_cover
Documentation

Divisible valuation orders give a finite open cover with actual unit local equations.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
universe u v
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
Lean source · statement
theorem exists_kummer_unit_cover (M : CurveModel K F) (n : ℕ+)
    (u : Pic0.kummerUnits K F n) :
    ∃ (r : ℕ) (U : Fin r → M.C.Opens) (h : Fin r → M.C.functionField),
      (⨆ i, U i) = ⊤ ∧ (∀ i, h i ≠ 0) ∧ ∀ i (x : M.C), x ∈ U i →
        M.ffEquiv (u.val : F) / h i ^ (n : ℕ) ∈
          (algebraMap (M.C.presheaf.stalk x) M.C.functionField).range ∧
        h i ^ (n : ℕ) / M.ffEquiv (u.val : F) ∈
          (algebraMap (M.C.presheaf.stalk x) M.C.functionField).range
def

kummerGenericMap

L166 ↗
AlgebraicCurve.CurveModel.kummerGenericMap
Documentation

The generic Kummer algebra map whose normalization is the cover.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
universe u v
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
Lean source · statement
def kummerGenericMap (M : CurveModel K F) (n : ℕ+) (u : Pic0.kummerUnits K F n) :
    Spec (.of (AdjoinRoot (Polynomial.X ^ (n : ℕ) -
      Polynomial.C (M.ffEquiv (u.val : F)) : Polynomial M.C.functionField))) ⟶ M.C
theorem

isFiniteEtale_kummer

L173 ↗
AlgebraicCurve.CurveModel.isFiniteEtale_kummer
Documentation

Normalization in the actual Kummer algebra is finite etale when n is a unit.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
universe u v
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
Lean source · statement
theorem isFiniteEtale_kummer (M : CurveModel K F) (n : ℕ+)
    (hn : IsUnit ((n : ℕ) : K)) (u : Pic0.kummerUnits K F n) :
    IsFiniteEtale (M.kummerGenericMap n u).fromNormalization
def

kummerCover

L189 ↗
AlgebraicCurve.CurveModel.kummerCover
Documentation

The actual finite etale Kummer cover, which may be disconnected.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
universe u v
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
Lean source · statement
def kummerCover (M : CurveModel K F) (n : ℕ+) (hn : IsUnit ((n : ℕ) : K))
    (u : Pic0.kummerUnits K F n) : FiniteEtale M.C
theorem

kummerClass_eq_one_of_section

L196 ↗
AlgebraicCurve.CurveModel.kummerClass_eq_one_of_section
Documentation

A section of the actual Kummer cover forces its divisor class to vanish.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel
universe u v
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
Lean source · statement
theorem kummerClass_eq_one_of_section [HasPrincipalDivisors K F]
    (M : CurveModel K F) (n : ℕ+) (hn : IsUnit ((n : ℕ) : K))
    (u : Pic0.kummerUnits K F n) (s : M.C ⟶ (M.kummerCover n hn u).left)
    (hs : s ≫ (M.kummerCover n hn u).hom = 𝟙 M.C) : Pic0.kummerClass n u = 1

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