The Picard group of a numerical type

Let T be a numerical type, with components i, multiplicities mᵢ, weights wᵢ and intersection matrix A = (aᵢⱼ). A multidegree of T is a tuple d : T.Component → ℤ, and the Picard group of T is the cokernel of

eᵢ ↦ ∑ⱼ (aᵢⱼ / wⱼ) eⱼ,

as in Stacks, Tag 0C7H. Everything in this file is purely numerical: it is a construction on the combinatorial datum T alone, and no model, line bundle or realisation statement occurs in any definition or proof below.

The geometry the construction abstracts, and from which the terminology is borrowed, is the following. On the special fibre of a regular model realising T, a line bundle has a multidegree: the tuple of the degrees of its restrictions to the components, each taken over the constant field κᵢ of its own component. The degree over κⱼ of the restriction to Cⱼ of the line bundle attached to Cᵢ is aᵢⱼ / wⱼ, so the bundles coming from the components themselves have multidegrees spanning the image of the map above.

The divisions aᵢⱼ / wⱼ are exact: the defining axiom of a numerical type gives wⱼ ∣ aⱼᵢ, and the intersection matrix is symmetric. Performing them is not cosmetic. The cokernel Coker(A) of the intersection matrix itself is a different group, and the comparison map Pic(T) → Coker(A) induced by eⱼ ↦ wⱼeⱼ is injective but, as soon as one weight exceeds one, not surjective. Both halves of that statement are proved below.

Main definitions

• TauCeti.NumericalType.weightedIntersection: the matrix a'ᵢⱼ = aᵢⱼ / wⱼ.
• TauCeti.NumericalType.principalDivisors: the subgroup of multidegrees spanned by the rows of A', and TauCeti.NumericalType.intersectionRelations, the subgroup spanned by the rows of A itself.
• TauCeti.NumericalType.Pic: the Picard group of a numerical type, the cokernel of A', and TauCeti.NumericalType.Coker, the cokernel of A.
• TauCeti.NumericalType.picToCoker: the comparison map Pic(T) → Coker(A) induced by eⱼ ↦ wⱼeⱼ.
• TauCeti.NumericalType.degree: the total degree ∑ⱼ mⱼwⱼdⱼ of a multidegree, as a homomorphism on Pic(T).
• TauCeti.NumericalType.Equiv.picCongr: the isomorphism of Picard groups induced by an equivalence of numerical types.

Main results

• TauCeti.NumericalType.picToCoker_injective: the comparison map is injective, which is the assertion of Stacks, Tag 0CE7.
• TauCeti.NumericalType.picToCoker_surjective_iff: it is surjective exactly when every weight is one, so Pic(T) is a strictly finer invariant than Coker(A).
• TauCeti.NumericalType.smul_ne_zero_of_degree_ne_zero: a class of nonzero total degree has infinite order, and TauCeti.NumericalType.smul_mk_single_ne_zero, its special case for the class of the unit multidegree supported at a component, whose total degree is mᵢwᵢ ≠ 0. With the finite generation that Pic(T) inherits from ℤ^Component this is half of the assertion that Pic(T) is finitely generated of rank one.
• TauCeti.NumericalType.Equiv.picCongr and TauCeti.NumericalType.Equiv.degree_picCongr: the Picard group and the total degree do not depend on the chosen indexing of the components.

Implementation notes

Multidegrees are plain functions T.Component → ℤ, and the two relation subgroups are ranges of Matrix.vecMulLinear, so Pic(T) and Coker(A) are literally cokernels of ℤ-linear maps and inherit their module structure from Submodule.Quotient. Invariance under reindexing of the component set, in the sense of TauCeti.NumericalType.reindex, is the special case of TauCeti.NumericalType.Equiv.picCongr at TauCeti.NumericalType.equivReindex; it is transport along LinearEquiv.funCongrLeft.

The weighted intersection matrix

theorem TauCeti.NumericalType.weight_dvd_intersection (T : NumericalType) (i j : T.Component) : ↑↑(T.weight j) ∣ T.intersection i j

The weight of the j-th component divides every intersection number aᵢⱼ.

The axiom weight_dvd of a numerical type says that wⱼ divides every entry of the j-th row; symmetry of the intersection matrix turns that into divisibility of the j-th column.

def TauCeti.NumericalType.weightedIntersection (T : NumericalType) : Matrix T.Component T.Component ℤ

The weighted intersection matrix a'ᵢⱼ = aᵢⱼ / wⱼ of a numerical type. Its i-th row is the multidegree attached to the i-th component: geometrically, the j-th entry is the degree, over the constant field κⱼ of the j-th component, of the restriction to Cⱼ of the line bundle attached to Cᵢ.

The division is exact by TauCeti.NumericalType.weight_dvd_intersection; see TauCeti.NumericalType.weightedIntersection_mul_weight.

Equations

• T.weightedIntersection = Matrix.of fun (i j : T.Component) => T.intersection i j / ↑↑(T.weight j)

@[simp]

theorem TauCeti.NumericalType.weightedIntersection_apply (T : NumericalType) (i j : T.Component) : T.weightedIntersection i j = T.intersection i j / ↑↑(T.weight j)

The entries of the weighted intersection matrix.

theorem TauCeti.NumericalType.weightedIntersection_mul_weight (T : NumericalType) (i j : T.Component) : T.weightedIntersection i j * ↑↑(T.weight j) = T.intersection i j

The division defining the weighted intersection matrix is exact.

This is not a simp lemma: TauCeti.NumericalType.weightedIntersection_apply rewrites the left-hand side to aᵢⱼ / wⱼ * wⱼ, so the statement is not in simp-normal form.

theorem TauCeti.NumericalType.weightedIntersection_mul_diagonal (T : NumericalType) : (T.weightedIntersection * Matrix.diagonal fun (i : T.Component) => ↑↑(T.weight i)) = T.intersection

Rescaling the columns of the weighted intersection matrix by the weights returns the intersection matrix.

Multidegrees and the two relation subgroups

def TauCeti.NumericalType.weightScaling (T : NumericalType) : (T.Component → ℤ) →ₗ[ℤ] T.Component → ℤ

Rescaling the j-th coordinate of a multidegree by the weight wⱼ, that is, the map eⱼ ↦ wⱼeⱼ. Geometrically it converts a degree measured over the constant field κⱼ into a degree measured over the residue field.

Equations

• T.weightScaling = (Matrix.diagonal fun (i : T.Component) => ↑↑(T.weight i)).vecMulLinear

@[simp]

theorem TauCeti.NumericalType.weightScaling_apply (T : NumericalType) (d : T.Component → ℤ) (j : T.Component) : T.weightScaling d j = d j * ↑↑(T.weight j)

The coordinates of a weight-rescaled multidegree.

theorem TauCeti.NumericalType.weightScaling_injective (T : NumericalType) : Function.Injective ⇑T.weightScaling

Rescaling by the weights is injective, the weights being positive.

theorem TauCeti.NumericalType.weightScaling_comp_weightedIntersection (T : NumericalType) : T.weightScaling ∘ₗ T.weightedIntersection.vecMulLinear = T.intersection.vecMulLinear

Rescaling by the weights carries the rows of the weighted intersection matrix to the rows of the intersection matrix, at the level of the linear maps they induce.

def TauCeti.NumericalType.principalDivisors (T : NumericalType) : Submodule ℤ (T.Component → ℤ)

The principal multidegrees of a numerical type: the subgroup spanned by the rows j ↦ aᵢⱼ / wⱼ of the weighted intersection matrix, that is, by the multidegrees attached to the components.

Equations

• T.principalDivisors = T.weightedIntersection.vecMulLinear.range

def TauCeti.NumericalType.intersectionRelations (T : NumericalType) : Submodule ℤ (T.Component → ℤ)

The subgroup spanned by the rows of the intersection matrix itself, the unweighted analogue of TauCeti.NumericalType.principalDivisors.

Equations

• T.intersectionRelations = T.intersection.vecMulLinear.range

theorem TauCeti.NumericalType.mem_principalDivisors_iff (T : NumericalType) {d : T.Component → ℤ} : d ∈ T.principalDivisors ↔ ∃ (v : T.Component → ℤ), Matrix.vecMul v T.weightedIntersection = d

Membership in the principal multidegrees, spelled out.

theorem TauCeti.NumericalType.mem_intersectionRelations_iff (T : NumericalType) {d : T.Component → ℤ} : d ∈ T.intersectionRelations ↔ ∃ (v : T.Component → ℤ), Matrix.vecMul v T.intersection = d

Membership in the span of the rows of the intersection matrix, spelled out.

theorem TauCeti.NumericalType.map_weightScaling_principalDivisors (T : NumericalType) : Submodule.map T.weightScaling T.principalDivisors = T.intersectionRelations

Rescaling by the weights carries the principal multidegrees exactly onto the span of the rows of the intersection matrix.

theorem TauCeti.NumericalType.intersectionRelations_le_range_weightScaling (T : NumericalType) : T.intersectionRelations ≤ T.weightScaling.range

Every row of the intersection matrix is divisible by the weights, so the relations it spans are themselves weight-rescaled multidegrees.

theorem TauCeti.NumericalType.principalDivisors_le_comap_intersectionRelations (T : NumericalType) : T.principalDivisors ≤ Submodule.comap T.weightScaling T.intersectionRelations

Rescaling by the weights descends to the quotients defining Pic(T) and Coker(A).

The Picard group and the cokernel of the intersection matrix

@[reducible, inline]

abbrev TauCeti.NumericalType.Pic (T : NumericalType) : Type u

The Picard group of a numerical type: the cokernel of eᵢ ↦ ∑ⱼ (aᵢⱼ/wⱼ)eⱼ, as in Stacks, Tag 0C7H. Its elements are multidegrees T.Component → ℤ modulo the principal ones, the rows of the weighted intersection matrix.

Equations

• T.Pic = ((T.Component → ℤ) ⧸ T.principalDivisors)

@[reducible, inline]

abbrev TauCeti.NumericalType.Coker (T : NumericalType) : Type u

The cokernel of the intersection matrix of a numerical type. It is a coarser invariant than TauCeti.NumericalType.Pic; see TauCeti.NumericalType.picToCoker_surjective_iff.

Equations

• T.Coker = ((T.Component → ℤ) ⧸ T.intersectionRelations)

def TauCeti.NumericalType.picToCoker (T : NumericalType) : T.Pic →ₗ[ℤ] T.Coker

The comparison map Pic(T) → Coker(A) induced by eⱼ ↦ wⱼeⱼ, from Stacks, Tag 0CE7.

Equations

• T.picToCoker = T.principalDivisors.mapQ T.intersectionRelations T.weightScaling ⋯

@[simp]

theorem TauCeti.NumericalType.picToCoker_mk (T : NumericalType) (d : T.Component → ℤ) : T.picToCoker (Submodule.Quotient.mk d) = Submodule.Quotient.mk (T.weightScaling d)

The comparison map on the class of a multidegree.

theorem TauCeti.NumericalType.picToCoker_injective (T : NumericalType) : Function.Injective ⇑T.picToCoker

The comparison map of Stacks, Tag 0CE7 is injective: a multidegree whose weight rescaling is a combination of the rows of A is itself the same combination of the rows of A'.

theorem TauCeti.NumericalType.range_picToCoker (T : NumericalType) : T.picToCoker.range = Submodule.map T.intersectionRelations.mkQ T.weightScaling.range

The image of the comparison map consists of the classes of the weight-rescaled multidegrees.

theorem TauCeti.NumericalType.picToCoker_surjective_iff (T : NumericalType) : Function.Surjective ⇑T.picToCoker ↔ ∀ (i : T.Component), T.weight i = 1

The comparison map Pic(T) → Coker(A) is surjective exactly when every component has weight one, that is, exactly when no division by a weight took place. So the weighted cokernel is a strictly finer invariant than the cokernel of the intersection matrix.

The total degree

def TauCeti.NumericalType.totalDegree (T : NumericalType) : (T.Component → ℤ) →ₗ[ℤ] ℤ

The total degree ∑ⱼ mⱼwⱼdⱼ of a multidegree d, before passing to the Picard group.

The j-th component contributes its multiplicity times its coordinate, rescaled by wⱼ so as to be measured over the residue field rather than over the constant field κⱼ. This is the numerical counterpart of the degree over the residue field of a line bundle on the whole special fibre ∑ⱼ mⱼCⱼ.

Equations

• T.totalDegree = Fintype.linearCombination ℤ fun (j : T.Component) => ↑↑(T.multiplicity j) * ↑↑(T.weight j)

theorem TauCeti.NumericalType.totalDegree_apply (T : NumericalType) (d : T.Component → ℤ) : T.totalDegree d = ∑ j : T.Component, d j * (↑↑(T.multiplicity j) * ↑↑(T.weight j))

The total degree, written out as a sum over the components.

theorem TauCeti.NumericalType.totalDegree_comp_weightedIntersection (T : NumericalType) : T.totalDegree ∘ₗ T.weightedIntersection.vecMulLinear = 0

The total degree kills the multidegrees coming from the components: this is exactly the fibre relation ∑ⱼ mⱼaᵢⱼ = 0 of a numerical type.

def TauCeti.NumericalType.degree (T : NumericalType) : T.Pic →ₗ[ℤ] ℤ

The total degree of a class in the Picard group of a numerical type. The fibre relation makes TauCeti.NumericalType.totalDegree vanish on the principal multidegrees, so it descends to Pic(T).

Equations

• T.degree = T.principalDivisors.liftQ T.totalDegree ⋯

@[simp]

theorem TauCeti.NumericalType.degree_mk (T : NumericalType) (d : T.Component → ℤ) : T.degree (Submodule.Quotient.mk d) = T.totalDegree d

The degree of the class of a multidegree is its total degree.

theorem TauCeti.NumericalType.degree_mk_single (T : NumericalType) (i : T.Component) : T.degree (Submodule.Quotient.mk (Pi.single i 1)) = ↑↑(T.multiplicity i) * ↑↑(T.weight i)

The degree of the unit multidegree supported at a component.

theorem TauCeti.NumericalType.smul_ne_zero_of_degree_ne_zero (T : NumericalType) {x : T.Pic} (hx : T.degree x ≠ 0) {n : ℤ} (hn : n ≠ 0) : n • x ≠ 0

A class of nonzero total degree has infinite order in Pic(T): no nonzero multiple of it vanishes.

theorem TauCeti.NumericalType.smul_mk_single_ne_zero (T : NumericalType) (i : T.Component) {n : ℤ} (hn : n ≠ 0) : n • Submodule.Quotient.mk (Pi.single i 1) ≠ 0

No nonzero multiple of the class of the unit multidegree supported at the i-th component vanishes in Pic(T), because its total degree is mᵢwᵢ ≠ 0. This class is not the class of the i-th component itself: that is the i-th row of the weighted intersection matrix, hence principal and zero in Pic(T).

Together with the finite generation that Pic(T) inherits from ℤ^Component, this is half of the assertion that Pic(T) is a finitely generated abelian group of rank one.

Invariance under equivalences of numerical types

theorem TauCeti.NumericalType.Equiv.weightedIntersection_eq {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') : T'.weightedIntersection = T.weightedIntersection.submatrix ⇑f.toEquiv.symm ⇑f.toEquiv.symm

An equivalence of numerical types matches the weighted intersection matrices.

theorem TauCeti.NumericalType.Equiv.vecMulLinear_weightedIntersection {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') : T'.weightedIntersection.vecMulLinear = ↑(LinearEquiv.funCongrLeft ℤ ℤ f.toEquiv.symm) ∘ₗ T.weightedIntersection.vecMulLinear ∘ₗ ↑(LinearEquiv.funCongrLeft ℤ ℤ f.toEquiv)

Transporting multidegrees along an equivalence of numerical types intertwines the two maps whose cokernels are the Picard groups.

theorem TauCeti.NumericalType.Equiv.map_principalDivisors {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') : Submodule.map (↑(LinearEquiv.funCongrLeft ℤ ℤ f.toEquiv.symm)) T.principalDivisors = T'.principalDivisors

An equivalence of numerical types matches the principal multidegrees.

def TauCeti.NumericalType.Equiv.picCongr {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') : T.Pic ≃ₗ[ℤ] T'.Pic

Equivalent numerical types have isomorphic Picard groups.

Equations

• f.picCongr = Submodule.Quotient.equiv T.principalDivisors T'.principalDivisors (LinearEquiv.funCongrLeft ℤ ℤ f.toEquiv.symm) ⋯

@[simp]

theorem TauCeti.NumericalType.Equiv.picCongr_mk {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') (d : T.Component → ℤ) : f.picCongr (Submodule.Quotient.mk d) = Submodule.Quotient.mk fun (b : T'.Component) => d (f.toEquiv.symm b)

The transported Picard class of a multidegree is the class of the transported multidegree.

@[simp]

theorem TauCeti.NumericalType.Equiv.picCongr_refl {T : NumericalType} : refl.picCongr = LinearEquiv.refl ℤ T.Pic

The identity equivalence induces the identity of Picard groups.

@[simp]

theorem TauCeti.NumericalType.Equiv.picCongr_trans {T : NumericalType} {T' : NumericalType} {T'' : NumericalType} (f : T.Equiv T') (g : T'.Equiv T'') : (f.trans g).picCongr = f.picCongr ≪≫ₗ g.picCongr

A composite of equivalences induces the composite isomorphism of Picard groups.

@[simp]

theorem TauCeti.NumericalType.Equiv.picCongr_symm {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') : f.picCongr.symm = f.symm.picCongr

The inverse of an equivalence induces the inverse isomorphism of Picard groups.

@[simp]

theorem TauCeti.NumericalType.Equiv.degree_picCongr {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') (x : T.Pic) : T'.degree (f.picCongr x) = T.degree x

The total degree of a class in Pic(T) does not change under transport along an equivalence of numerical types.