The topological genus of a numerical type #

The intersection matrix of a numerical type determines a finite simple graph: its vertices are the components, and two distinct vertices are joined when the corresponding components meet. This file records the first Betti number of that connected graph,

g_top = 1 - #components + #edges,

and proves the elementary graph-theoretic facts needed when comparing it with the arithmetic genus. The graph is connected by the defining connectedness condition of a numerical type, so its topological genus is nonnegative; it vanishes exactly when the intersection graph is a tree.

The definition uses Nat.card for the finite edge type. This avoids making the combinatorial invariant depend on a chosen finite-type instance for the unordered pairs of components.

The terminology is that of the Stacks Project, Section 55.3, especially Lemma 55.3.10. The result here supplies the graph-theoretic input for the comparison with arithmetic genus in Lemma 55.3.14.

The intersection graph #

source

def TauCeti.NumericalType.intersectionGraph (T : NumericalType) :

SimpleGraph T.Component

The simple graph joining distinct components with positive intersection number.

Equations

T.intersectionGraph = SimpleGraph.fromRel T.Adj

Instances For

source

@[simp]

theorem TauCeti.NumericalType.intersectionGraph_adj_iff (T : NumericalType) {i j : T.Component} :

T.intersectionGraph.Adj i j ↔ T.Adj i j

source

theorem TauCeti.NumericalType.intersectionGraph_connected (T : NumericalType) :

T.intersectionGraph.Connected

The intersection graph of a numerical type is connected.

Topological genus #

source

noncomputable def TauCeti.NumericalType.topologicalGenus (T : NumericalType) :

ℤ

The topological genus of the intersection graph of a numerical type.

For a connected dual graph this is its first Betti number. The edge type is the finite type of unordered pairs of distinct components that are adjacent in intersectionGraph.

Equations