Documentation

TauCeti.AlgebraicGeometry.Curves.StableReduction.Picard.DegreeZero

The degree-zero numerical Picard group #

The weighted Picard group of a numerical type is a finitely generated abelian group of rank one. Its total-degree map is nonzero, so its kernel has rank zero and is finite. Thus the numerical degree-zero classes are precisely the torsion classes. This is the finite group to which the degree-zero part of the Picard group of a special fibre is compared in stable reduction.

The rank-one input is NumericalType.finrank_pic; the degree map and its value on a unit multidegree are in Picard.Basic.

The numerical Picard construction follows Stacks, Tag 0C7H, and its finite generation and rank follow Stacks, Tag 0C7I.

source
def TauCeti.NumericalType.degreeZeroSubgroup (T : NumericalType) :
Submodule ℤ T.Pic

The numerical Picard classes of total degree zero.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.NumericalType.mem_degreeZeroSubgroup (T : NumericalType) {x : T.Pic} :
    x ∈ T.degreeZeroSubgroup ↔ T.degree x = 0

    A numerical Picard class belongs to the degree-zero subgroup exactly when it has total degree zero.

    source
    @[simp]
    theorem TauCeti.NumericalType.degree_coe_degreeZeroSubgroup (T : NumericalType) (x : ↥T.degreeZeroSubgroup) :
    T.degree ↑x = 0

    A degree-zero numerical Picard class has total degree zero.

    source
    theorem TauCeti.NumericalType.finrank_range_degree (T : NumericalType) :
    Module.finrank ℤ ↥T.degree.range = 1

    The total-degree map of a numerical type has rank one: the class supported at any component has nonzero degree.

    source
    theorem TauCeti.NumericalType.finrank_degreeZeroSubgroup (T : NumericalType) :
    Module.finrank ℤ ↥T.degreeZeroSubgroup = 0

    The kernel of total degree has rank zero.

    source
    theorem TauCeti.NumericalType.finite_degreeZeroSubgroup (T : NumericalType) :
    Finite ↥T.degreeZeroSubgroup

    The degree-zero subgroup of the numerical Picard group is finite.

    source
    theorem TauCeti.NumericalType.degree_eq_zero_iff_exists_smul_eq_zero (T : NumericalType) (x : T.Pic) :
    T.degree x = 0 ↔ ∃ (n : ℤ), n ≠ 0 ∧ n • x = 0

    A numerical Picard class has degree zero if and only if it is torsion. In particular, the degree-zero condition can be checked by an integral multiple of the class.