Module

BoundaryResidueCardinality.lean

Nyll.JacobianVarieties.Kummer.BoundaryResidueCardinality

4 declarations indexed from sourceView source ↗

Module documentation

Cardinality of the degree-zero boundary residue group

A nonempty finite boundary has one independent sum relation. This counts the actual kernel of the sum homomorphism, not a group postulated to model étale cohomology.

Imports5

Mathlib.Data.ZMod.Basic
Mathlib.Data.PNat.Defs
Mathlib.GroupTheory.QuotientGroup.Basic
Mathlib.GroupTheory.Coset.Card
Mathlib.Data.Fintype.Pi

Imported by3

def

boundaryResidueSum

L28 ↗

JacobianVarieties.Kummer.boundaryResidueSum

Documentation

Sum the residues at the finitely many boundary points.

Source context 3 commands

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

noncomputable section
open scoped BigOperators
namespace JacobianVarieties.Kummer

Lean source · full declaration

def boundaryResidueSum (ι : Type*) [Fintype ι] (n : ℕ+) :
    (ι → ZMod (n : ℕ)) →+ ZMod (n : ℕ) where
  toFun a := ∑ i, a i
  map_zero' := Finset.sum_const_zero
  map_add' _ _ := Finset.sum_add_distrib

def

boundaryResidueGroup

L35 ↗

JacobianVarieties.Kummer.boundaryResidueGroup

Documentation

Residue vectors satisfying the degree-zero relation.

Source context 3 commands

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

noncomputable section
open scoped BigOperators
namespace JacobianVarieties.Kummer

Lean source · statement

def boundaryResidueGroup (ι : Type*) [Fintype ι] (n : ℕ+) :
    AddSubgroup (ι → ZMod (n : ℕ))

theorem

boundaryResidueSum_surjective

L40 ↗

JacobianVarieties.Kummer.boundaryResidueSum_surjective

Documentation

Any residue can occur as the total, using one chosen boundary point.

Source context 3 commands

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

noncomputable section
open scoped BigOperators
namespace JacobianVarieties.Kummer

Lean source · statement

theorem boundaryResidueSum_surjective
    {ι : Type*} [Fintype ι] (i₀ : ι) (n : ℕ+) :
    Function.Surjective (boundaryResidueSum ι n)

theorem

natCard_boundaryResidueGroup

L56 ↗

JacobianVarieties.Kummer.natCard_boundaryResidueGroup

Documentation

A boundary of cardinality r greater than zero contributes n^(r-1) possible degree-zero residue vectors.

Source context 3 commands

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

noncomputable section
open scoped BigOperators
namespace JacobianVarieties.Kummer

Lean source · statement

theorem natCard_boundaryResidueGroup
    {ι : Type*} [Fintype ι] (i₀ : ι) (n : ℕ+) :
    Nat.card (boundaryResidueGroup ι n) =
      (n : ℕ) ^ (Fintype.card ι - 1)

Module documentation

Cardinality of the degree-zero boundary residue group

Declarations

boundaryResidueSum

boundaryResidueGroup

boundaryResidueSum_surjective

natCard_boundaryResidueGroup