Module

OpenLocalUnits.lean

Nyll.JacobianVarieties.Kummer.OpenLocalUnits

4 declarations indexed from sourceView source ↗

Module documentation

Local Kummer equations away from a boundary

Only the valuation at the point in question is used to remove an nth power and obtain a unit. For an actual open immersion, the canonical function-field map transports these two local-ring membership statements. No comparison with the cohomology of the open curve is postulated.

Imports6

Imported by2

theorem

ord_pow

L33 ↗

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

L37 ↗

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_of_ord_dvd

L49 ↗

AlgebraicCurve.CurveModel.exists_stalk_kummer_unit_of_ord_dvd

Documentation

Divisibility at a single closed point supplies a unit after dividing by an actual nth power in the function field.

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_of_ord_dvd (M : CurveModel K F) (n : ℕ+)
    (u : Fˣ) (x : M.C)
    (hdiv : ∀ xc : closedPoints M.C, xc.val = x →
      (n : ℤ) ∣ (M.placeOfPoint xc).ord (u : F)) :
    ∃ h : M.C.functionField, h ≠ 0 ∧
      M.ffEquiv (u : F) / h ^ (n : ℕ) ∈
        (algebraMap (M.C.presheaf.stalk x) M.C.functionField).range ∧
      h ^ (n : ℕ) / M.ffEquiv (u : F) ∈
        (algebraMap (M.C.presheaf.stalk x) M.C.functionField).range

theorem

exists_open_stalk_kummer_unit

L105 ↗

AlgebraicCurve.CurveModel.exists_open_stalk_kummer_unit

Documentation

A divisorial Kummer class with orders divisible away from the boundary has actual local unit equations at every point of an open subscheme that avoids that boundary.

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_kummer_unit
    (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
    (a : Pic0.openKummerUnits K F S n)
    {U : Scheme} [IsIntegral 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)
    (y : U) :
    ∃ h : U.functionField, h ≠ 0 ∧
      j.functionFieldMap hj (M.ffEquiv (a.val : F)) / h ^ (n : ℕ) ∈
        (algebraMap (U.presheaf.stalk y) U.functionField).range ∧
      h ^ (n : ℕ) / j.functionFieldMap hj (M.ffEquiv (a.val : F)) ∈
        (algebraMap (U.presheaf.stalk y) U.functionField).range

Module documentation

Local Kummer equations away from a boundary

Declarations

ord_pow

ffEquiv_mem_stalk_range

exists_stalk_kummer_unit_of_ord_dvd

exists_open_stalk_kummer_unit