Module

OpenDivisorCardinality.lean

Nyll.JacobianVarieties.Kummer.OpenDivisorCardinality

3 declarations indexed from sourceView source ↗

Module documentation

Cardinality of open divisorial Kummer classes

The actual quotient of functions unramified away from the boundary by actual powers has n^(2g+r-1) elements for a nonempty finite boundary. The proof uses its exact residue sequence, actual Pic⁰ torsion, and the proved geometric Picard cardinality calculation. Identification with derived H¹ of the open curve is not assumed or asserted here.

Imports5

Imported by3

def

openKummerResidueRangeEquiv

L33 ↗

AlgebraicCurve.CurveModel.openKummerResidueRangeEquiv

Documentation

The image of the actual quotient residue map consists exactly of the actual sum-zero boundary residue vectors.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open scoped BigOperators
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel

Lean source · full declaration

def openKummerResidueRangeEquiv
    {K F : Type} [Field K] [IsAlgClosed K]
    [Field F] [Algebra K F] [IsCurveOver K F]
    (M : CurveModel K F)
    (ε : SchemeHomOver (𝟙 (Spec (.of K))) M.toBase)
    (S : Set (Place K F)) [Fintype S] (v₀ : S)
    (n : ℕ+) (hchar : ((n : ℕ) : K) ≠ 0) :
    (Pic0.openKummerResidueQuotient S n).range ≃ boundaryResidueGroup S n where
  toFun x := ⟨Multiplicative.toAdd x.val, by
    obtain ⟨q, hq⟩ := x.property
    obtain ⟨u, rfl⟩ := QuotientGroup.mk_surjective q
    change (∑ v : S, Multiplicative.toAdd x.val v) = 0
    rw [← hq]
    exact M.sum_openKummerResidue_eq_zero_set S n u⟩
  invFun a := ⟨Multiplicative.ofAdd a.val, by
    obtain ⟨u, hu⟩ := M.exists_openKummerUnits_of_sum_eq_zero
      ε S v₀ n hchar a.val a.property
    exact ⟨QuotientGroup.mk u, hu⟩⟩
  left_inv _ := rfl
  right_inv _ := rfl

def

properKummerQuotientEquivResidueKernel

L56 ↗

AlgebraicCurve.CurveModel.properKummerQuotientEquivResidueKernel

Documentation

The kernel of the quotient residue map is the proper divisorial Kummer quotient, without adding identifications or abstract comparison data.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open scoped BigOperators
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel

Lean source · statement

def properKummerQuotientEquivResidueKernel
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (S : Set (Place K F)) (n : ℕ+) :
    Pic0.kummerUnits K F n ⧸ Pic0.kummerPowers K F n ≃
      (Pic0.openKummerResidueQuotient S n).ker

theorem

natCard_openKummerQuotient

L69 ↗

AlgebraicCurve.CurveModel.natCard_openKummerQuotient

Documentation

The cardinality formula for actual divisorial Kummer classes on the complement of a nonempty finite set of places, in characteristic zero.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open scoped BigOperators
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel

Lean source · statement

theorem natCard_openKummerQuotient
    {K F : Type} [Field K] [IsAlgClosed K] [CharZero K]
    [Field F] [Algebra K F] [IsCurveOver K F]
    (M : CurveModel K F)
    (ε : SchemeHomOver (𝟙 (Spec (.of K))) M.toBase)
    (S : Set (Place K F)) [Fintype S] (v₀ : S) (n : ℕ+) :
    Nat.card (Pic0.openKummerUnits K F S n ⧸ Pic0.openKummerPowers K F S n) =
      (n : ℕ) ^ (2 * genusFF K F + Fintype.card S - 1)

Module documentation

Cardinality of open divisorial Kummer classes

Declarations

openKummerResidueRangeEquiv

properKummerQuotientEquivResidueKernel

natCard_openKummerQuotient