Module

OpenCurveResidueRanks.lean

Nyll.AnabelianGeometry.WeightFiltration.OpenCurveResidueRanks

3 declarations indexed from sourceView source ↗

Module documentation

Genus and boundary ranks in the actual residue sequence

The kernel has n^(2g) elements and the residue image has n^(r-1) elements. These counts apply to the actual cohomology maps constructed from Kummer covers. Intrinsic recognition of this filtration from arithmetic Galois action is not assumed here.

Imports2

Imported by2

def

properKummerEquivFiniteResidueKernel

L36 ↗

AnabelianGeometry.WeightFiltration.properKummerEquivFiniteResidueKernel

Documentation

The actual residue kernel is the proper divisorial Kummer quotient.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve NeronModelInfra
namespace AnabelianGeometry.WeightFiltration
variable {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)
  (n : ℕ+)
  {X : Scheme} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)

Lean source · statement

def properKummerEquivFiniteResidueKernel :
    Additive (Pic0.kummerUnits K F n ⧸ Pic0.kummerPowers K F n) ≃
      (finiteResidue M n j hj hn xi).ker

theorem

natCard_finiteResidue_ker

L48 ↗

AnabelianGeometry.WeightFiltration.natCard_finiteResidue_ker

Documentation

Genus appears as half the exponent in the cardinality of the actual finite-coefficient residue kernel.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve NeronModelInfra
namespace AnabelianGeometry.WeightFiltration
variable {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)
  (n : ℕ+)
  {X : Scheme} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)
include ε

Lean source · statement

theorem natCard_finiteResidue_ker :
    Nat.card (finiteResidue M n j hj hn xi).ker =
      (n : ℕ) ^ (2 * genusFF K F)

theorem

natCard_finiteResidue_range

L74 ↗

AnabelianGeometry.WeightFiltration.natCard_finiteResidue_range

Documentation

A nonempty boundary of size r contributes n^(r-1) actual residue classes.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory AlgebraicCurve NeronModelInfra
namespace AnabelianGeometry.WeightFiltration
variable {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)
  (n : ℕ+)
  {X : Scheme} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X)
include ε
variable [Fintype (M.openBoundaryPlaces j)]
omit [CharZero K] in

Lean source · statement

theorem natCard_finiteResidue_range (v₀ : M.openBoundaryPlaces j) :
    Nat.card (finiteResidue M n j hj hn xi).range =
      (n : ℕ) ^ (Fintype.card (M.openBoundaryPlaces j) - 1)

Module documentation

Genus and boundary ranks in the actual residue sequence

Declarations

properKummerEquivFiniteResidueKernel

natCard_finiteResidue_ker

natCard_finiteResidue_range