Prime torsion for a numerical type

For a numerical type T, this file equips the subgroups Pic(T)[ℓ] and Coker(A)[ℓ] killed by a natural number ℓ with their canonical ZMod ℓ-module structures. When ℓ is prime, Pic(T)[ℓ] is a finite-dimensional vector space. Its cardinality is therefore ℓ raised to its dimension, which is the form of the torsion invariant used when comparing a numerical type with torsion line bundles on a regular model.

The total degree of every nonzero-order torsion class vanishes. Equivalences of numerical types carry torsion classes to torsion classes and induce linear equivalences on the corresponding prime-torsion spaces, so both their dimension and cardinality are independent of the indexing of the components.

The Picard group follows Stacks, Tag 0C7H, and its finite generation and rank are Stacks, Tag 0C7I.

@[reducible, inline]

abbrev TauCeti.NumericalType.torsion (T : NumericalType) (ℓ : ℕ) : AddSubgroup T.Pic

The subgroup Pic(T)[ℓ] of Picard classes killed by ℓ.

Although the main application takes ℓ prime, the subgroup is useful for every natural number. For prime ℓ, it carries the canonical vector-space structure over ZMod ℓ.

Equations

• T.torsion ℓ = AddSubgroup.torsionBy T.Pic ↑ℓ

@[instance_reducible]

noncomputable instance TauCeti.NumericalType.torsionModule (T : NumericalType) (ℓ : ℕ) : Module (ZMod ℓ) ↥(T.torsion ℓ)

The canonical ZMod ℓ-module structure on the ℓ-torsion of Pic(T).

Equations

• T.torsionModule ℓ = AddSubgroup.torsionBy.zmodModule

@[reducible, inline]

abbrev TauCeti.NumericalType.cokerTorsion (T : NumericalType) (ℓ : ℕ) : AddSubgroup T.Coker

The subgroup Coker(A)[ℓ] of classes in the cokernel of the intersection matrix killed by ℓ.

Equations

• T.cokerTorsion ℓ = AddSubgroup.torsionBy T.Coker ↑ℓ

@[instance_reducible]

noncomputable instance TauCeti.NumericalType.cokerTorsionModule (T : NumericalType) (ℓ : ℕ) : Module (ZMod ℓ) ↥(T.cokerTorsion ℓ)

The canonical ZMod ℓ-module structure on the ℓ-torsion of Coker(A).

Equations

• T.cokerTorsionModule ℓ = AddSubgroup.torsionBy.zmodModule

theorem TauCeti.NumericalType.finite_torsion (T : NumericalType) {ℓ : ℕ} (hℓ : ℓ ≠ 0) : Finite ↥(T.torsion ℓ)

If ℓ is nonzero, then the ℓ-torsion subgroup of Pic(T) is finite.

The ambient Picard group is finitely generated because it is a quotient of the finite free module of multidegrees. Its ℓ-torsion subgroup is therefore a finitely generated torsion abelian group.

instance TauCeti.NumericalType.torsionModuleFinite (T : NumericalType) (ℓ : ℕ) [NeZero ℓ] : Module.Finite (ZMod ℓ) ↥(T.torsion ℓ)

For nonzero ℓ, the ℓ-torsion subgroup of Pic(T) is finitely generated over ZMod ℓ.

theorem TauCeti.NumericalType.natCard_torsion (T : NumericalType) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : Nat.card ↥(T.torsion ℓ) = ℓ ^ Module.finrank (ZMod ℓ) ↥(T.torsion ℓ)

The cardinality of prime torsion is the prime raised to its vector-space dimension.

@[simp]

theorem TauCeti.NumericalType.degree_coe_torsion (T : NumericalType) {ℓ : ℕ} (hℓ : ℓ ≠ 0) (x : ↥(T.torsion ℓ)) : T.degree ↑x = 0

Every Picard torsion class killed by a nonzero natural number has total degree zero.

theorem TauCeti.NumericalType.isTorsionFree_pic_of_card_eq_one (T : NumericalType) (h : Fintype.card T.Component = 1) : Module.IsTorsionFree ℤ T.Pic

The Picard group of a numerical type with a single component is torsion-free: its intersection matrix vanishes, so zero is the only principal multidegree.

@[simp]

theorem TauCeti.NumericalType.finrank_torsion_eq_zero_of_card_eq_one (T : NumericalType) (h : Fintype.card T.Component = 1) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : Module.finrank (ZMod ℓ) ↥(T.torsion ℓ) = 0

A numerical type with a single component has no nonzero prime torsion in its Picard group.

noncomputable def TauCeti.NumericalType.Equiv.torsionCongr {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') (ℓ : ℕ) : ↥(T.torsion ℓ) ≃ₗ[ZMod ℓ] ↥(T'.torsion ℓ)

An equivalence of numerical types induces a ZMod ℓ-linear equivalence on their ℓ-torsion Picard subgroups.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.NumericalType.Equiv.coe_torsionCongr {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') (ℓ : ℕ) (x : ↥(T.torsion ℓ)) : ↑((f.torsionCongr ℓ) x) = f.picCongr ↑x

The underlying Picard class of a transported torsion class is transported by picCongr.

@[simp]

theorem TauCeti.NumericalType.Equiv.torsionCongr_refl {T : NumericalType} (ℓ : ℕ) : refl.torsionCongr ℓ = LinearEquiv.refl (ZMod ℓ) ↥(T.torsion ℓ)

The identity equivalence induces the identity on torsion Picard classes.

@[simp]

theorem TauCeti.NumericalType.Equiv.torsionCongr_trans {T : NumericalType} {T' : NumericalType} {T'' : NumericalType} (f : T.Equiv T') (g : T'.Equiv T'') (ℓ : ℕ) : (f.trans g).torsionCongr ℓ = f.torsionCongr ℓ ≪≫ₗ g.torsionCongr ℓ

Torsion transport respects composition of equivalences of numerical types.

@[simp]

theorem TauCeti.NumericalType.Equiv.torsionCongr_symm {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') (ℓ : ℕ) : (f.torsionCongr ℓ).symm = f.symm.torsionCongr ℓ

Torsion transport along an inverse equivalence is the inverse linear equivalence.

theorem TauCeti.NumericalType.Equiv.finrank_torsion_eq {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : Module.finrank (ZMod ℓ) ↥(T.torsion ℓ) = Module.finrank (ZMod ℓ) ↥(T'.torsion ℓ)

Prime-torsion dimension is invariant under equivalence of numerical types.

theorem TauCeti.NumericalType.Equiv.natCard_torsion_eq {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') (ℓ : ℕ) : Nat.card ↥(T.torsion ℓ) = Nat.card ↥(T'.torsion ℓ)

Torsion cardinality is invariant under equivalence of numerical types.