NYLL
Module

CurveCoverSplitting.lean

Nyll.JacobianVarieties.Kummer.CurveCoverSplitting
2 declarations indexed from sourceView source ↗

Module documentation

Splitting of the actual Kummer cover

An actual root of a Kummer function constructs a section of its normalized finite etale cover. Use a single open set with local denominator equal to that root: the normalized equation is then the unit equation, so the existing local root universal property constructs the section on the original curve.

Over algebraically closed constants, the actual divisorial Kummer comparison therefore identifies vanishing of the torsion divisor class with existence of a section of the actual cover. The integer must be invertible in the base field; the statement includes positive characteristic only away from it.

Imports7
Imported by3

Declarations

theorem

exists_section_kummerCover_of_pow

L41 ↗
AlgebraicCurve.CurveModel.exists_section_kummerCover_of_pow
Documentation

An actual root supplies a section of the actual normalized Kummer cover.

Source context 5 commands

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

noncomputable section
universe u v
open CategoryTheory AlgebraicGeometry
namespace AlgebraicCurve.CurveModel
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
Lean source · statement
theorem exists_section_kummerCover_of_pow (M : CurveModel K F) (n : ℕ+)
    (hn : IsUnit ((n : ℕ) : K)) (u : Pic0.kummerUnits K F n)
    (w : F) (hw : w ^ (n : ℕ) = (u.val : F)) :
    ∃ s : M.C ⟶ (M.kummerCover n hn u).left,
      s ≫ (M.kummerCover n hn u).hom = 𝟙 M.C
theorem

kummerClass_eq_one_iff_exists_section

L84 ↗
AlgebraicCurve.CurveModel.kummerClass_eq_one_iff_exists_section
Documentation

A Kummer cover of a curve over algebraically closed constants has a section exactly when the actual divided principal-divisor class vanishes.

Source context 5 commands

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

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

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