Module

OpenBoundaryRelation.lean

Nyll.JacobianVarieties.Kummer.OpenBoundaryRelation

2 declarations indexed from sourceView source ↗

Module documentation

The boundary residue relation

The degree of an actual principal divisor is zero. Orders away from the boundary vanish modulo the exponent, so the sum of its boundary residues is zero. Together with boundary realization this identifies the residue image; it does not assert the still separate open-curve H¹ comparison.

Imports2

Imported by3

theorem

sum_openKummerResidue_eq_zero

L27 ↗

AlgebraicCurve.CurveModel.sum_openKummerResidue_eq_zero

Documentation

Boundary residues of an actual function unramified off a finite set satisfy the degree-zero relation.

Source context 3 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicCurve.CurveModel

Lean source · statement

theorem sum_openKummerResidue_eq_zero
    {K F : Type} [Field K] [IsAlgClosed K]
    [Field F] [Algebra K F] [IsCurveOver K F]
    (M : CurveModel K F) (S : Finset (Place K F)) (n : ℕ+)
    (u : Pic0.openKummerUnits K F (S : Set (Place K F)) n) :
    ∑ v ∈ S, (v.ord (u.val : F) : ZMod (n : ℕ)) = 0

theorem

sum_openKummerResidue_eq_zero_set

L77 ↗

AlgebraicCurve.CurveModel.sum_openKummerResidue_eq_zero_set