Rank of the Picard group of a numerical type

The Picard group of a numerical type is a finitely generated abelian group of rank one. The key input is that the kernel of the intersection matrix has rank one: its positive-entry graph is connected and its strictly positive multiplicity vector lies in the kernel, so the weighted maximum principle shows that every rational kernel vector is proportional to that vector.

The weighted intersection matrix defining Pic(T) differs from the intersection matrix by the injective rescaling of each coordinate by its positive weight. Consequently it has the same kernel rank. Rank-nullity then computes the rank of its cokernel.

Main results

• TauCeti.NumericalType.vecMul_intersection_eq_zero_iff: an integral row vector is killed by the intersection matrix exactly when its cross-products with the multiplicity vector agree.
• TauCeti.NumericalType.finrank_ker_vecMulLinear_intersection: the kernel of the intersection matrix has rank one over ℤ.
• TauCeti.NumericalType.finrank_pic: the Picard group has rank one over ℤ.

The kernel argument is the weighted maximum principle in Matrix.eq_smul_of_mulVec_eq_zero. The rank-one conclusion is Stacks, Tag 0C7I.

theorem TauCeti.NumericalType.vecMul_intersection_eq_zero_iff (T : NumericalType) (v : T.Component → ℤ) : Matrix.vecMul v T.intersection = 0 ↔ ∀ (i j : T.Component), ↑↑(T.multiplicity j) * v i = ↑↑(T.multiplicity i) * v j

An integral row vector is killed by the intersection matrix of a numerical type exactly when its cross-products with the multiplicity vector agree. Thus, over the fraction field, every kernel vector is proportional to the multiplicity vector. The cross-product formulation remains exact over ℤ even when the multiplicities have a nontrivial common factor.

theorem TauCeti.NumericalType.ker_vecMulLinear_intersection_apply_injective (T : NumericalType) (i : T.Component) : Function.Injective ⇑((LinearMap.proj i).domRestrict T.intersection.vecMulLinear.ker)

Evaluation at any component is injective on the kernel of the intersection matrix.

theorem TauCeti.NumericalType.finrank_ker_vecMulLinear_intersection (T : NumericalType) : Module.finrank ℤ ↥T.intersection.vecMulLinear.ker = 1

The kernel of the intersection matrix of a numerical type has rank one over ℤ.

theorem TauCeti.NumericalType.finrank_pic (T : NumericalType) : Module.finrank ℤ T.Pic = 1

The Picard group of a numerical type has rank one over ℤ.