Comparing the arithmetic and topological genera of a numerical type

For a component i of a numerical type, put

qᵢ = mᵢwᵢ and rᵢ = ∑_{j ≠ i} aᵢⱼ / wᵢ.

The local genus defect

qᵢ (-1 + gᵢ + rᵢ / 2) - (-1 + degree(i) / 2)

compares the contribution of i to the arithmetic genus with its contribution to the first Betti number of the intersection graph. Summing these defects gives exactly arithmeticGenus - topologicalGenus.

The divisibility axiom for a numerical type implies that rᵢ is at least the ordinary valence of i. Consequently the local defect is nonnegative whenever gᵢ is positive, i has at least two neighbours, or qᵢ = 1. This proves the arithmetic/topological genus comparison whenever every component satisfies one of those conditions, in particular when the intersection graph has minimum valence at least two.

For a minimal numerical type with more than one component the comparison holds without further hypotheses: g_top ≤ g (Stacks, Lemma 55.3.14). The proof here differs from the chain argument of the Stacks Project. For a set S of components, put

E(S) = ∑_{i ∈ S} (Φᵢ + 1 - vᵢ(S) / 2),

where Φᵢ is the genus contribution of i and vᵢ(S) is the number of components of S meeting i, so that E of the set of all components is g - g_top. Deleting i from S lowers E(S) by Φᵢ + 1 - vᵢ(S), which is nonnegative when vᵢ(S) ≤ 1 because minimality makes Φᵢ nonnegative. Once every remaining component meets at least two others, the fibre relation bounds E(S) below by a sum of nonnegative terms.

Main results

• TauCeti.NumericalType.sum_genusDefect: the local defects sum to g - g_top.
• TauCeti.NumericalType.topologicalGenus_le_arithmeticGenus_of_two_le_valence: g_top ≤ g when every component has at least two neighbours.
• TauCeti.NumericalType.IsMinimal.topologicalGenus_le_arithmeticGenus: g_top ≤ g for a minimal numerical type with more than one component.

noncomputable def TauCeti.NumericalType.normalizedValence (T : NumericalType) (i : T.Component) : ℚ

The sum ∑_{j ≠ i} aᵢⱼ / wᵢ of the normalized intersections of a component with all other components. Each summand is a nonnegative integer by the axioms of a numerical type.

Equations

• T.normalizedValence i = ∑ j ∈ Finset.univ.erase i, ↑(T.intersection i j) / ↑↑(T.weight i)

theorem TauCeti.NumericalType.normalizedValence_def (T : NumericalType) (i : T.Component) : T.normalizedValence i = ∑ j ∈ Finset.univ.erase i, ↑(T.intersection i j) / ↑↑(T.weight i)

The defining sum for the normalized valence.

noncomputable def TauCeti.NumericalType.genusDefect (T : NumericalType) (i : T.Component) : ℚ

The local difference between the arithmetic-genus and graph-genus contributions of a component of a numerical type.

Equations

• T.genusDefect i = ↑↑(T.multiplicity i) * ↑↑(T.weight i) * (-1 + ↑(T.genus i) + T.normalizedValence i / 2) - (-1 + ↑(T.intersectionGraph.neighborSet i).ncard / 2)

theorem TauCeti.NumericalType.genusDefect_def (T : NumericalType) (i : T.Component) : T.genusDefect i = ↑↑(T.multiplicity i) * ↑↑(T.weight i) * (-1 + ↑(T.genus i) + T.normalizedValence i / 2) - (-1 + ↑(T.intersectionGraph.neighborSet i).ncard / 2)

The defining formula for the local genus defect.

theorem TauCeti.NumericalType.normalizedValence_nonneg (T : NumericalType) (i : T.Component) : 0 ≤ T.normalizedValence i

The normalized valence is nonnegative.

theorem TauCeti.NumericalType.valence_le_normalizedValence (T : NumericalType) (i : T.Component) : ↑(T.intersectionGraph.neighborSet i).ncard ≤ T.normalizedValence i

The normalized intersection valence is at least the valence of the intersection graph.

theorem TauCeti.NumericalType.sum_genusDefect (T : NumericalType) : ∑ i : T.Component, T.genusDefect i = ↑T.arithmeticGenus - ↑T.topologicalGenus

The sum of the local genus defects is the arithmetic genus minus the topological genus.

theorem TauCeti.NumericalType.genusDefect_nonneg_of_genus_pos_or_two_le_valence_or_mul_eq_one (T : NumericalType) (i : T.Component) (h : 0 < T.genus i ∨ 2 ≤ (T.intersectionGraph.neighborSet i).ncard ∨ T.multiplicity i * T.weight i = 1) : 0 ≤ T.genusDefect i

A component has nonnegative genus defect if it has positive genus, at least two neighbours, or multiplicity times weight equal to one.

theorem TauCeti.NumericalType.topologicalGenus_le_arithmeticGenus_of_genus_pos_or_two_le_valence_or_mul_eq_one (T : NumericalType) (h : ∀ (i : T.Component), 0 < T.genus i ∨ 2 ≤ (T.intersectionGraph.neighborSet i).ncard ∨ T.multiplicity i * T.weight i = 1) : T.topologicalGenus ≤ T.arithmeticGenus

If every component has positive genus, at least two neighbours, or unit weighted multiplicity, then the topological genus is at most the arithmetic genus.

theorem TauCeti.NumericalType.topologicalGenus_le_arithmeticGenus_of_two_le_valence (T : NumericalType) (h : ∀ (i : T.Component), 2 ≤ (T.intersectionGraph.neighborSet i).ncard) : T.topologicalGenus ≤ T.arithmeticGenus

If the intersection graph has minimum degree at least two, then the topological genus is at most the arithmetic genus.

Minimal numerical types

theorem TauCeti.NumericalType.IsMinimal.topologicalGenus_le_arithmeticGenus {T : NumericalType} (hT : T.IsMinimal) (h : 1 < Fintype.card T.Component) : T.topologicalGenus ≤ T.arithmeticGenus

A minimal numerical type with more than one component has topological genus at most its arithmetic genus (Stacks, Tag 0C7C).