Module

OpenCurveCover.lean

Nyll.JacobianVarieties.Kummer.OpenCurveCover

5 declarations indexed from sourceView source ↗

Module documentation

Actual Kummer covers of open curves

The normalization construction is applied to the actual open curve, using local unit equations proved from its interior valuation orders. The cover is not required to extend étale across the removed boundary.

Imports5

Imported by4

theorem

exists_open_stalk_ranges

L31 ↗

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_finite_kummer_unit_cover

L56 ↗

AlgebraicCurve.CurveModel.exists_finite_kummer_unit_cover

Documentation

Pointwise unit equations admit a finite open cover on a compact integral scheme.

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_finite_kummer_unit_cover
    {X : Scheme.{u}} [IsIntegral X] [CompactSpace X]
    (n : ℕ+) (a : X.functionField)
    (hlocal : ∀ x : X, ∃ h : X.functionField, h ≠ 0 ∧
      a / h ^ (n : ℕ) ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range ∧
      h ^ (n : ℕ) / a ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range) :
    ∃ (r : ℕ) (V : Fin r → X.Opens) (h : Fin r → X.functionField),
      (⨆ i, V i) = ⊤ ∧ (∀ i, h i ≠ 0) ∧ ∀ i (x : X), x ∈ V i →
        a / h i ^ (n : ℕ) ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range ∧
        h i ^ (n : ℕ) / a ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range

def

openKummerGenericMap

L93 ↗

AlgebraicCurve.CurveModel.openKummerGenericMap

Documentation

The actual generic Kummer equation over an open subscheme of a proper curve model.

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 openKummerGenericMap
    (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
    (a : Pic0.openKummerUnits K F S n)
    {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) (hj : DenseRange j) :
    Spec (.of (AdjoinRoot (Polynomial.X ^ (n : ℕ) -
      Polynomial.C (j.functionFieldMap hj (M.ffEquiv (a.val : F))) :
        Polynomial U.functionField))) ⟶ U

theorem

isFiniteEtale_openKummer

L106 ↗

AlgebraicCurve.CurveModel.isFiniteEtale_openKummer

Documentation

Normalizing the actual open curve in its Kummer root algebra gives a finite étale cover when the valuation orders are divisible at all interior points. Compactness here is quasi-compactness of the open curve.

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_openKummer
    (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
    (hn : IsUnit ((n : ℕ) : K)) (a : Pic0.openKummerUnits K F S n)
    {U : Scheme.{u}} [IsIntegral U] [CompactSpace U]
    (j : U ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
    (hinterior : ∀ (y : U) (x : closedPoints M.C),
      x.val = j y → M.placeOfPoint x ∉ S) :
    IsFiniteEtale (M.openKummerGenericMap S n a j hj).fromNormalization

def

openKummerCover

L134 ↗

AlgebraicCurve.CurveModel.openKummerCover

Documentation

The actual finite étale Kummer cover of the open curve.

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 openKummerCover
    (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
    (hn : IsUnit ((n : ℕ) : K)) (a : Pic0.openKummerUnits K F S n)
    {U : Scheme.{u}} [IsIntegral U] [CompactSpace U]
    (j : U ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
    (hinterior : ∀ (y : U) (x : closedPoints M.C),
      x.val = j y → M.placeOfPoint x ∉ S) : FiniteEtale U

Module documentation

Actual Kummer covers of open curves

Declarations

exists_open_stalk_ranges

exists_finite_kummer_unit_cover

openKummerGenericMap

isFiniteEtale_openKummer

openKummerCover