Numerical types and their signed genus

A numerical type is the combinatorial shadow of the special fibre of a proper regular model of a curve over a discrete valuation ring: a finite nonempty set of components carrying multiplicities mᵢ, weights wᵢ (the degrees of the constant fields of the components over the residue field) and genera gᵢ, together with a symmetric matrix of intersection numbers A = (aᵢⱼ) whose off-diagonal entries are nonnegative, whose associated graph is connected, which is killed by the multiplicity vector, and whose i-th row is divisible by wᵢ.

This file introduces that structure, its positivity and connectedness API, its reindexing along an equivalence of component sets, equivalences of numerical types, and its signed genus

g(T) = 1 + ∑ᵢ mᵢ (wᵢ (gᵢ - 1) - aᵢᵢ / 2).

The arithmetic subtlety in the genus formula is that the individual half-diagonals aᵢᵢ / 2 need not be integers, so the halving may only be performed once, on the whole sum. That this is legitimate is TauCeti.NumericalType.even_sum_multiplicity_mul_diagonal: pairing the fibre relation against the multiplicity vector gives ∑ᵢⱼ mᵢ mⱼ aᵢⱼ = 0, and for a symmetric integer matrix that forces ∑ᵢ mᵢ aᵢᵢ to be even (Matrix.IsSymm.even_sum_mul_diag_of_dotProduct_mulVec_eq_zero).

Main definitions

• TauCeti.NumericalType: the structure described above, following Stacks, Tag 0C6Z.
• TauCeti.NumericalType.Adj: the adjacency relation i ≠ j ∧ 0 < aᵢⱼ whose reflexive transitive closure the connectedness axiom requires to be total.
• TauCeti.NumericalType.reindex: the numerical type obtained by transporting the component set along an equivalence.
• TauCeti.NumericalType.Equiv: an equivalence of numerical types, a bijection of component sets matching all of their data, with its identity, inverse and composite.
• TauCeti.NumericalType.arithmeticGenus: the signed genus, valued in ℤ.

Main results

• TauCeti.NumericalType.even_sum_multiplicity_mul_diagonal: ∑ᵢ mᵢ aᵢᵢ is even, which is what makes the halving in the genus formula exact, and TauCeti.NumericalType.two_mul_arithmeticGenus, the resulting division-free form of that formula.
• TauCeti.NumericalType.intersection_self_nonpos and TauCeti.NumericalType.intersection_self_neg: self-intersections are nonpositive, and are negative as soon as there is more than one component.
• TauCeti.NumericalType.multiplicity_mul_intersection_le and TauCeti.NumericalType.multiplicity_mul_weight_le_of_pos: the data at a neighbour of a component are bounded by its weighted self-intersection (Stacks, Tag 0C9U).
• TauCeti.NumericalType.intersection_eq_zero_of_card_eq_one and TauCeti.NumericalType.arithmeticGenus_of_card_eq_one: a numerical type with a single component has zero intersection matrix and signed genus 1 + mᵢwᵢ(gᵢ - 1) (Stacks, Tag 0C73).
• TauCeti.NumericalType.exists_mem_notMem_adj: every nonempty proper set of components meets its complement, the no-disconnected-cut form in which Stacks, Tag 0C6Z states the connectedness condition.
• TauCeti.NumericalType.arithmeticGenus_reindex: the signed genus does not depend on the chosen indexing of the components.
• TauCeti.NumericalType.nonempty_equiv_iff: two numerical types are equivalent exactly when one is a reindexing of the other, and TauCeti.NumericalType.Equiv.arithmeticGenus_eq: equivalent numerical types have the same signed genus.

Implementation notes

Abstract numerical types can have negative genus, so arithmeticGenus lands in ℤ rather than ℕ; the genus-zero variant of twoComponentWeightTwoExample in Picard/WeightedExample.lean has genus -1. Nor may the halving be distributed over the sum: oddDiagonalExample has odd diagonal entries.

Symmetry of the intersection matrix is recorded through Mathlib's Matrix.IsSymm rather than as a bare pointwise equation, so that a reindexed matrix inherits it from Matrix.IsSymm.submatrix.

The no-disconnected-cut criterion in the other direction, which is what discharges the connected field when a numerical type is built, has to be available before the type exists, so it is stated for a bare matrix: Matrix.forall_reflTransGen_ne_and_pos_iff in TauCeti.LinearAlgebra.Matrix.Connected, which this file re-exports.

structure TauCeti.NumericalType : Type (u + 1)

A numerical type, in the sense of Stacks, Tag 0C6Z.

multiplicity i and weight i are the multiplicity of the i-th component of the special fibre of a proper regular model and the degree of its constant field over the residue field, and genus i is its arithmetic genus over that constant field, not the genus of its normalization. The matrix intersection records the intersection numbers of the components.

• Component : Type u

  The finite nonempty index set of components.

• componentFintype : Fintype self.Component
• componentDecidableEq : DecidableEq self.Component
• componentNonempty : Nonempty self.Component
• multiplicity : self.Component → ℕ+

  The multiplicity of a component in the special fibre.

• weight : self.Component → ℕ+

  The degree of the constant field of a component over the residue field.

• intersection : Matrix self.Component self.Component ℤ

  The matrix of intersection numbers of the components.

• intersection_isSymm : self.intersection.IsSymm

  Intersection numbers are symmetric.

• offDiagonal_nonneg (i j : self.Component) : i ≠ j → 0 ≤ self.intersection i j

  Distinct components meet nonnegatively.

• connected (i j : self.Component) : Relation.ReflTransGen (fun (i j : self.Component) => i ≠ j ∧ 0 < self.intersection i j) i j

  The graph joining components that meet is connected.

• fiber_relation (i : self.Component) : ∑ j : self.Component, ↑↑(self.multiplicity j) * self.intersection i j = 0

  The whole special fibre meets every component in degree zero.

• weight_dvd (i j : self.Component) : ↑↑(self.weight i) ∣ self.intersection i j

  The i-th row of the intersection matrix is divisible by the weight of the i-th component.

• genus : self.Component → ℕ

  The arithmetic genus of a component over its own constant field.

theorem TauCeti.NumericalType.intersection_comm (T : NumericalType) (i j : T.Component) : T.intersection i j = T.intersection j i

Intersection numbers of a numerical type commute.

Connectedness of the intersection graph

def TauCeti.NumericalType.Adj (T : NumericalType) (i j : T.Component) : Prop

Two components of a numerical type are adjacent when they are distinct and meet.

Equations

• T.Adj i j = (i ≠ j ∧ 0 < T.intersection i j)

@[simp]

theorem TauCeti.NumericalType.adj_iff (T : NumericalType) {i j : T.Component} : T.Adj i j ↔ i ≠ j ∧ 0 < T.intersection i j

Unfolding of TauCeti.NumericalType.Adj.

theorem TauCeti.NumericalType.reflTransGen_adj (T : NumericalType) (i j : T.Component) : Relation.ReflTransGen T.Adj i j

The connectedness axiom, phrased with TauCeti.NumericalType.Adj.

theorem TauCeti.NumericalType.Adj.symm {T : NumericalType} {i j : T.Component} (h : T.Adj i j) : T.Adj j i

Adjacency is a symmetric relation.

theorem TauCeti.NumericalType.exists_mem_notMem_adj (T : NumericalType) (s : Set T.Component) (hne : s.Nonempty) (hs : s ≠ Set.univ) : ∃ i ∈ s, ∃ j ∉ s, T.Adj i j

Every nonempty proper set of components of a numerical type meets its complement: this is the no-disconnected-cut form of the connectedness axiom.

@[simp]

theorem TauCeti.NumericalType.intersection_mulVec_multiplicity (T : NumericalType) : (T.intersection.mulVec fun (i : T.Component) => ↑↑(T.multiplicity i)) = 0

The fibre relation in matrix form: the multiplicity vector lies in the kernel of the intersection matrix.

@[simp]

theorem TauCeti.NumericalType.multiplicity_vecMul_intersection (T : NumericalType) : Matrix.vecMul (fun (i : T.Component) => ↑↑(T.multiplicity i)) T.intersection = 0

The fibre relation in row-vector form: the multiplicity vector lies in the kernel of the intersection matrix.

Self-intersections

theorem TauCeti.NumericalType.multiplicity_mul_intersection_nonneg (T : NumericalType) {i j : T.Component} (h : i ≠ j) : 0 ≤ ↑↑(T.multiplicity j) * T.intersection i j

Off the diagonal, multiplicity-weighted intersection numbers are nonnegative.

theorem TauCeti.NumericalType.multiplicity_mul_intersection_self (T : NumericalType) (i : T.Component) : ↑↑(T.multiplicity i) * T.intersection i i = -∑ j ∈ Finset.univ.erase i, ↑↑(T.multiplicity j) * T.intersection i j

The fibre relation with the diagonal term isolated.

theorem TauCeti.NumericalType.intersection_self_nonpos (T : NumericalType) (i : T.Component) : T.intersection i i ≤ 0

Self-intersections in a numerical type are nonpositive.

theorem TauCeti.NumericalType.exists_adj (T : NumericalType) (h : 1 < Fintype.card T.Component) (i : T.Component) : ∃ (j : T.Component), T.Adj i j

In a numerical type with more than one component, every component meets some other one.

theorem TauCeti.NumericalType.intersection_self_neg (T : NumericalType) (h : 1 < Fintype.card T.Component) (i : T.Component) : T.intersection i i < 0

In a numerical type with more than one component, self-intersections are negative.

theorem TauCeti.NumericalType.exists_intersection_self_eq (T : NumericalType) (h : 1 < Fintype.card T.Component) (i : T.Component) : ∃ (k : ℕ), 1 ≤ k ∧ T.intersection i i = -(↑k * ↑↑(T.weight i))

With more than one component, every self-intersection is a negative multiple of the weight.

Bounds at the neighbours of a component

theorem TauCeti.NumericalType.multiplicity_mul_intersection_le (T : NumericalType) (i j : T.Component) : ↑↑(T.multiplicity i) * T.intersection i j ≤ ↑↑(T.multiplicity j) * |T.intersection j j|

The multiplicity-weighted intersection number mᵢaᵢⱼ is bounded by the weighted self-intersection mⱼ|aⱼⱼ| of the second component (Stacks, Tag 0C9U).

theorem TauCeti.NumericalType.multiplicity_mul_weight_le_of_pos (T : NumericalType) {i j : T.Component} (hij : 0 < T.intersection i j) : ↑↑(T.multiplicity i) * ↑↑(T.weight i) ≤ ↑↑(T.multiplicity j) * |T.intersection j j|

If two components meet, the multiplicity times the weight of the first is bounded by the weighted self-intersection of the second (Stacks, Tag 0C9U).

Numerical types with one component

theorem TauCeti.NumericalType.intersection_eq_zero_of_card_eq_one (T : NumericalType) (h : Fintype.card T.Component = 1) (i j : T.Component) : T.intersection i j = 0

A numerical type with a single component has zero intersection matrix (Stacks, Tag 0C73).

theorem TauCeti.NumericalType.one_lt_card_of_intersection_self_ne_zero (T : NumericalType) {i : T.Component} (h : T.intersection i i ≠ 0) : 1 < Fintype.card T.Component

A numerical type with a component of nonzero self-intersection has more than one component.

Integrality of the signed genus

theorem TauCeti.NumericalType.even_sum_multiplicity_mul_diagonal (T : NumericalType) : Even (∑ i : T.Component, ↑↑(T.multiplicity i) * T.intersection i i)

The multiplicity-weighted sum of the self-intersections of a numerical type is even.

This is what makes the halving in the genus formula exact; the individual terms mᵢ aᵢᵢ need not be even, as oddDiagonalExample shows. The fibre relation says that the intersection matrix kills the multiplicity vector, so this is an instance of Matrix.IsSymm.even_sum_mul_diag_of_dotProduct_mulVec_eq_zero.

The signed genus

def TauCeti.NumericalType.arithmeticGenus (T : NumericalType) : ℤ

The signed genus of a numerical type, g(T) = 1 + ∑ᵢ mᵢ (wᵢ (gᵢ - 1) - aᵢᵢ / 2) (compare Stacks, Tag 0C71).

The halving is performed once, on the whole sum ∑ᵢ mᵢ aᵢᵢ, which is even by even_sum_multiplicity_mul_diagonal; the individual half-diagonals need not be integers. Abstract numerical types can have negative genus, so the value is an integer, not a natural number.

Equations

• T.arithmeticGenus = 1 + ∑ i : T.Component, ↑↑(T.multiplicity i) * ↑↑(T.weight i) * (↑(T.genus i) - 1) - (∑ i : T.Component, ↑↑(T.multiplicity i) * T.intersection i i) / 2

theorem TauCeti.NumericalType.arithmeticGenus_def (T : NumericalType) : T.arithmeticGenus = 1 + ∑ i : T.Component, ↑↑(T.multiplicity i) * ↑↑(T.weight i) * (↑(T.genus i) - 1) - (∑ i : T.Component, ↑↑(T.multiplicity i) * T.intersection i i) / 2

The defining formula of the signed genus, with the halving performed once on the whole sum ∑ᵢ mᵢ aᵢᵢ.

theorem TauCeti.NumericalType.two_mul_arithmeticGenus (T : NumericalType) : 2 * T.arithmeticGenus = 2 + 2 * ∑ i : T.Component, ↑↑(T.multiplicity i) * ↑↑(T.weight i) * (↑(T.genus i) - 1) - ∑ i : T.Component, ↑↑(T.multiplicity i) * T.intersection i i

The genus formula with the halving cleared, which is the shape in which it is used.

theorem TauCeti.NumericalType.arithmeticGenus_of_card_eq_one (T : NumericalType) (h : Fintype.card T.Component = 1) (i : T.Component) : T.arithmeticGenus = 1 + ↑↑(T.multiplicity i) * ↑↑(T.weight i) * (↑(T.genus i) - 1)

The signed genus of a numerical type with a single component i is 1 + mᵢwᵢ(gᵢ - 1) (Stacks, Tag 0C73).

Reindexing

def TauCeti.NumericalType.reindex (T : NumericalType) {C : Type v} (e : T.Component ≃ C) : NumericalType

The numerical type obtained by transporting the component set along an equivalence.

The finiteness and decidable equality of the new component set are transported along the equivalence, so the target needs no instances of its own and may live in any universe.

Equations

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

theorem TauCeti.NumericalType.reindex_eq (T : NumericalType) {T' : NumericalType} (e : T.Component ≃ T'.Component) (hm : ∀ (i : T.Component), T'.multiplicity (e i) = T.multiplicity i) (hw : ∀ (i : T.Component), T'.weight (e i) = T.weight i) (hA : ∀ (i j : T.Component), T'.intersection (e i) (e j) = T.intersection i j) (hg : ∀ (i : T.Component), T'.genus (e i) = T.genus i) : T.reindex e = T'

Numerical types are determined by their multiplicity, weight, intersection and genus data: an equivalence of component sets matching all four identifies the two types. As the component set is a field rather than a parameter, this is the extensionality principle for numerical types; the instance fields are subsingletons and the remaining fields are proofs.

@[simp]

theorem TauCeti.NumericalType.reindex_multiplicity (T : NumericalType) {C : Type v} (e : T.Component ≃ C) (c : C) : (T.reindex e).multiplicity c = T.multiplicity (e.symm c)

Multiplicities of a reindexed numerical type.

@[simp]

theorem TauCeti.NumericalType.reindex_weight (T : NumericalType) {C : Type v} (e : T.Component ≃ C) (c : C) : (T.reindex e).weight c = T.weight (e.symm c)

Weights of a reindexed numerical type.

@[simp]

theorem TauCeti.NumericalType.reindex_genus (T : NumericalType) {C : Type v} (e : T.Component ≃ C) (c : C) : (T.reindex e).genus c = T.genus (e.symm c)

Component genera of a reindexed numerical type.

@[simp]

theorem TauCeti.NumericalType.reindex_intersection (T : NumericalType) {C : Type v} (e : T.Component ≃ C) (c d : C) : (T.reindex e).intersection c d = T.intersection (e.symm c) (e.symm d)

Intersection numbers of a reindexed numerical type.

@[simp]

theorem TauCeti.NumericalType.reindex_refl (T : NumericalType) : T.reindex (_root_.Equiv.refl T.Component) = T

Reindexing along the identity equivalence changes nothing.

@[simp]

theorem TauCeti.NumericalType.reindex_reindex (T : NumericalType) {C : Type v} (e : T.Component ≃ C) {D : Type w} (f : C ≃ D) : (T.reindex e).reindex f = T.reindex (e.trans f)

Reindexing twice is reindexing along the composite equivalence.

@[simp]

theorem TauCeti.NumericalType.arithmeticGenus_reindex (T : NumericalType) {C : Type v} (e : T.Component ≃ C) : (T.reindex e).arithmeticGenus = T.arithmeticGenus

The signed genus does not depend on the chosen indexing of the components.

Equivalence of numerical types

structure TauCeti.NumericalType.Equiv (T : NumericalType) (T' : NumericalType) : Type (max u v)

An equivalence of numerical types, in the sense of Stacks, Tag 0C6Z: a bijection of component sets matching multiplicities, weights, intersection numbers and genera. Two numerical types are equivalent when Nonempty (T.Equiv T').

• toEquiv : T.Component ≃ T'.Component

  The underlying bijection of component sets.

• multiplicity_apply (i : T.Component) : T'.multiplicity (self.toEquiv i) = T.multiplicity i

  The bijection preserves multiplicities.

• weight_apply (i : T.Component) : T'.weight (self.toEquiv i) = T.weight i

  The bijection preserves weights.

• intersection_apply (i j : T.Component) : T'.intersection (self.toEquiv i) (self.toEquiv j) = T.intersection i j

  The bijection preserves intersection numbers.

• genus_apply (i : T.Component) : T'.genus (self.toEquiv i) = T.genus i

  The bijection preserves the genera of the components.

theorem TauCeti.NumericalType.Equiv.ext {T : NumericalType} {T' : NumericalType} {x y : T.Equiv T'} (toEquiv : x.toEquiv = y.toEquiv) : x = y

theorem TauCeti.NumericalType.Equiv.ext_iff {T : NumericalType} {T' : NumericalType} {x y : T.Equiv T'} : x = y ↔ x.toEquiv = y.toEquiv

def TauCeti.NumericalType.Equiv.refl {T : NumericalType} : T.Equiv T

The identity equivalence of a numerical type.

Equations

• TauCeti.NumericalType.Equiv.refl = { toEquiv := Equiv.refl T.Component, multiplicity_apply := ⋯, weight_apply := ⋯, intersection_apply := ⋯, genus_apply := ⋯ }

@[simp]

theorem TauCeti.NumericalType.Equiv.refl_toEquiv {T : NumericalType} : refl.toEquiv = _root_.Equiv.refl T.Component

The bijection underlying TauCeti.NumericalType.Equiv.refl is the identity.

def TauCeti.NumericalType.Equiv.symm {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') : T'.Equiv T

The inverse of an equivalence of numerical types.

Equations

• f.symm = { toEquiv := f.toEquiv.symm, multiplicity_apply := ⋯, weight_apply := ⋯, intersection_apply := ⋯, genus_apply := ⋯ }

@[simp]

theorem TauCeti.NumericalType.Equiv.symm_toEquiv {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') : f.symm.toEquiv = f.toEquiv.symm

The bijection underlying the inverse is the inverse bijection.

def TauCeti.NumericalType.Equiv.trans {T : NumericalType} {T' : NumericalType} {T'' : NumericalType} (f : T.Equiv T') (g : T'.Equiv T'') : T.Equiv T''

The composite of two equivalences of numerical types.

Equations

• f.trans g = { toEquiv := f.toEquiv.trans g.toEquiv, multiplicity_apply := ⋯, weight_apply := ⋯, intersection_apply := ⋯, genus_apply := ⋯ }

@[simp]

theorem TauCeti.NumericalType.Equiv.trans_toEquiv {T : NumericalType} {T' : NumericalType} {T'' : NumericalType} (f : T.Equiv T') (g : T'.Equiv T'') : (f.trans g).toEquiv = f.toEquiv.trans g.toEquiv

The bijection underlying a composite is the composite bijection.

@[simp]

theorem TauCeti.NumericalType.Equiv.refl_symm {T : NumericalType} : refl.symm = refl

The inverse of the identity equivalence is the identity.

@[simp]

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

Inverting an equivalence of numerical types twice returns it.

@[simp]

theorem TauCeti.NumericalType.Equiv.refl_trans {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') : refl.trans f = f

The identity equivalence is a left unit for composition.

@[simp]

theorem TauCeti.NumericalType.Equiv.trans_refl {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') : f.trans refl = f

The identity equivalence is a right unit for composition.

@[simp]

theorem TauCeti.NumericalType.Equiv.self_trans_symm {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') : f.trans f.symm = refl

An equivalence of numerical types composed with its inverse is the identity.

@[simp]

theorem TauCeti.NumericalType.Equiv.symm_trans_self {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') : f.symm.trans f = refl

The inverse of an equivalence of numerical types composed with it is the identity.

@[simp]

theorem TauCeti.NumericalType.Equiv.trans_assoc {T : NumericalType} {T' : NumericalType} {T'' : NumericalType} {T''' : NumericalType} (f : T.Equiv T') (g : T'.Equiv T'') (h : T''.Equiv T''') : (f.trans g).trans h = f.trans (g.trans h)

Composition of equivalences of numerical types is associative.

theorem TauCeti.NumericalType.Equiv.reindex_eq {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') : T.reindex f.toEquiv = T'

An equivalence of numerical types identifies the target with the reindexed source.

theorem TauCeti.NumericalType.Equiv.arithmeticGenus_eq {T : NumericalType} {T' : NumericalType} (f : T.Equiv T') : T'.arithmeticGenus = T.arithmeticGenus

Equivalent numerical types have the same signed genus.

def TauCeti.NumericalType.equivReindex (T : NumericalType) {C : Type v} (e : T.Component ≃ C) : T.Equiv (T.reindex e)

A numerical type is equivalent to each of its reindexings, along the reindexing equivalence.

Equations

• T.equivReindex e = { toEquiv := e, multiplicity_apply := ⋯, weight_apply := ⋯, intersection_apply := ⋯, genus_apply := ⋯ }

@[simp]

theorem TauCeti.NumericalType.equivReindex_toEquiv (T : NumericalType) {C : Type v} (e : T.Component ≃ C) : (T.equivReindex e).toEquiv = e

The bijection underlying TauCeti.NumericalType.equivReindex is the reindexing equivalence.

theorem TauCeti.NumericalType.nonempty_equiv_iff (T : NumericalType) {T' : NumericalType} : Nonempty (T.Equiv T') ↔ ∃ (e : T.Component ≃ T'.Component), T.reindex e = T'

Two numerical types are equivalent exactly when one is a reindexing of the other.

Worked examples