The Picard group of a weighted two-component numerical type

For the numerical type with two components of multiplicity one and weight two, meeting twice, the weighted intersection relations are generated by (-1, 1). Thus its Picard group is infinite cyclic. The unweighted intersection relations are generated by (-2, 2), and their cokernel has nonzero two-torsion. This calculation distinguishes the weighted Picard group from the raw intersection cokernel in the numerical argument for stable reduction.

@[reducible, inline]

noncomputable abbrev TauCeti.NumericalType.twoComponentWeightTwoExample : NumericalType

Two components of multiplicity one, weight two and genus one, meeting doubly: a numerical type of signed genus three.

Equations

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

@[simp]

theorem TauCeti.NumericalType.twoComponentWeightTwoExample_multiplicity (i : Fin 2) : twoComponentWeightTwoExample.multiplicity i = 1

Each component of the two-component weight-two example has multiplicity one.

@[simp]

theorem TauCeti.NumericalType.twoComponentWeightTwoExample_weight (i : Fin 2) : twoComponentWeightTwoExample.weight i = 2

Each component of the two-component weight-two example has weight two.

@[simp]

theorem TauCeti.NumericalType.twoComponentWeightTwoExample_genus (i : Fin 2) : twoComponentWeightTwoExample.genus i = 1

Each component of the two-component weight-two example has genus one.

@[simp]

theorem TauCeti.NumericalType.twoComponentWeightTwoExample_arithmeticGenus : twoComponentWeightTwoExample.arithmeticGenus = 3

The two-component weight-two example has signed genus three.

@[simp]

theorem TauCeti.NumericalType.twoComponentWeightTwoExample_weightedIntersection : twoComponentWeightTwoExample.weightedIntersection = !![-1, 1; 1, -1]

The weighted intersection matrix of the two-component weight-two example.

@[simp]

theorem TauCeti.NumericalType.twoComponentWeightTwoExample_intersection : twoComponentWeightTwoExample.intersection = !![-2, 2; 2, -2]

The intersection matrix of the two-component weight-two example.

@[simp]

theorem TauCeti.NumericalType.twoComponentWeightTwoExample_mem_principalDivisors_iff (d : Fin 2 → ℤ) : d ∈ twoComponentWeightTwoExample.principalDivisors ↔ d 0 + d 1 = 0

The principal multidegrees in the weight-two example are exactly the pairs with sum zero.

noncomputable def TauCeti.NumericalType.twoComponentWeightTwoExamplePicLinearEquivInt : twoComponentWeightTwoExample.Pic ≃ₗ[ℤ] ℤ

The weighted Picard group of the two-component example is infinite cyclic, with a multidegree sent to the sum of its two coordinates.

Equations

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

@[simp]

theorem TauCeti.NumericalType.twoComponentWeightTwoExamplePicLinearEquivInt_mk (d : Fin 2 → ℤ) : twoComponentWeightTwoExamplePicLinearEquivInt (Submodule.Quotient.mk d) = d 0 + d 1

The Picard-class isomorphism is the sum of multidegrees.

instance TauCeti.NumericalType.twoComponentWeightTwoExample_isTorsionFree_pic : Module.IsTorsionFree ℤ twoComponentWeightTwoExample.Pic

The weighted Picard group of the two-component example is torsion-free.

theorem TauCeti.NumericalType.twoComponentWeightTwoExample_pic_eq_zero_of_two_smul_eq_zero (x : twoComponentWeightTwoExample.Pic) (hx : 2 • x = 0) : x = 0

The weighted Picard group has no nonzero two-torsion.

theorem TauCeti.NumericalType.twoComponentWeightTwoExample_coker_has_two_torsion : ∃ (x : twoComponentWeightTwoExample.Coker), x ≠ 0 ∧ 2 • x = 0

The raw intersection cokernel of the weight-two example contains nonzero two-torsion: the class of (1, -1) has order two.