Contracting unstable rational components of dual graphs

A pointed nodal curve is made stable by repeatedly contracting rational components with at most two special points. There are three kinds of such components, and each contraction has a combinatorial shadow on the dual graph:

• an unmarked rational tail (a rational component meeting the rest of the curve in one point) is deleted;
• a rational tail carrying one marking is deleted, and the marking moves to the point where the tail met the rest of the curve, on the neighbouring component;
• an unmarked rational bridge (a smooth rational component meeting the rest of the curve in two points) is replaced by a node joining the two neighbouring branches.

This file constructs both graph operations, TauCeti.DualGraph.contractTail and TauCeti.DualGraph.contractBridge, and computes how they change the numerical invariants. They keep the markings and remove one vertex. They lower the arithmetic genus by the genus of the contracted vertex, so they preserve it when that vertex is rational, as in a stabilization step. Contracting a bridge changes no log-canonical degree. Contracting a tail changes only the log-canonical degree of the neighbouring component, which drops by one when the tail is unmarked. So a component of positive log-canonical degree can become unstable once its tails are removed, and stabilization has to be iterated, recomputing degrees after each step.

TauCeti.DualGraph.StabilizationStep G H says that H arises from G by one such contraction. In the stable range 2g - 2 + n > 0, a graph admits a stabilization step exactly when it is not stable, and iterating steps from any graph reaches a stable graph of the same genus with the same markings; the number of vertices decreases at every step.

TauCeti.DualGraph.LabelledStabilizationStep P is the variant for graphs whose vertices carry labels: it contracts only vertices whose label satisfies P, and the remaining vertices keep their labels. Labelling the components by the degree of a map and contracting only those of degree zero gives map-aware stabilization, which never contracts a component on which the map is not constant.

Main definitions

• TauCeti.DualGraph.attachment: the neighbour of a vertex of valence one.
• TauCeti.DualGraph.contractTail: the graph with a vertex of valence one deleted and its markings moved to its neighbour.
• TauCeti.DualGraph.contractBridge: the graph with an unmarked loopless vertex of valence two replaced by an edge joining its two neighbours.
• TauCeti.DualGraph.StabilizationStep: contraction of a rational tail with at most one marking or of an unmarked rational bridge.
• TauCeti.DualGraph.LabelledStabilizationStep: the same contractions on labelled graphs, restricted to vertices whose label satisfies a predicate.

Main results

• TauCeti.DualGraph.arithmeticGenus_contractTail and TauCeti.DualGraph.arithmeticGenus_contractBridge: the arithmetic genus drops by the genus of the contracted vertex.
• TauCeti.DualGraph.logCanonicalDegree_contractTail and TauCeti.DualGraph.logCanonicalDegree_contractBridge: the change of log-canonical degrees.
• TauCeti.DualGraph.IsSemistable.logCanonicalDegree_contractTail: in a semistable graph, contracting a rational tail with at most one marking leaves the other log-canonical degrees unchanged.
• TauCeti.DualGraph.isStable_iff_forall_not_stabilizationStep: in the stable range, a graph is stable exactly when it admits no stabilization step.
• TauCeti.DualGraph.exists_reflTransGen_stabilizationStep_isStable: in the stable range, iterated stabilization steps reach a stable graph.
• TauCeti.DualGraph.exists_reflTransGen_labelledStabilizationStep_forall_not: iterated labelled stabilization steps reach a labelled graph admitting no further step.

References

• Stacks, Tag 0E7N, contracting rational tails and rational bridges.
• F. F. Knudsen, The projectivity of the moduli space of stable curves, II: The stacks M_{g,n}, Math. Scand. 52 (1983), 161–199, §2, for stabilization of pointed curves.

Half-edges at a vertex

theorem TauCeti.DualGraph.endpoint_rev_ne {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) {e : G.Edge} {i : Fin 2} (he : G.endpoint e i = v) : G.endpoint e i.rev ≠ v

A loopless vertex: the other branch of a node at v lies on another component.

theorem TauCeti.DualGraph.exists_endpoint_eq_of_valence_pos {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : 0 < G.valence v) : ∃ (h : G.Edge × Fin 2), G.endpoint h.1 h.2 = v

A vertex of positive valence carries a half-edge.

theorem TauCeti.DualGraph.eq_of_valence_eq_one {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) (h h' : G.Edge × Fin 2) (hh : G.endpoint h.1 h.2 = v) (hh' : G.endpoint h'.1 h'.2 = v) : h = h'

At a vertex of valence one, any two half-edges coincide.

theorem TauCeti.DualGraph.endpoint_one_ne_of_valence_eq_one {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) (e : G.Edge) (he : G.endpoint e 0 = v) : G.endpoint e 1 ≠ v

A vertex of valence one carries no loop.

noncomputable def TauCeti.DualGraph.attachment {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) : G.Vertex

The attachment of a vertex of valence one: the other endpoint of its unique edge. For a rational tail, it is the component that the tail meets.

theorem TauCeti.DualGraph.endpoint_rev_eq_attachment {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) {e : G.Edge} {i : Fin 2} (he : G.endpoint e i = v) : G.endpoint e i.rev = attachment hv

The other branch of the unique node at a vertex of valence one lies on its attachment.

theorem TauCeti.DualGraph.attachment_ne {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) : attachment hv ≠ v

A vertex of valence one is not its own attachment.

theorem TauCeti.DualGraph.adj_attachment {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) : G.Adj v (attachment hv)

A vertex of valence one is adjacent to its attachment.

noncomputable def TauCeti.DualGraph.halfEdgeOfValenceEqTwo {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) : Fin 2 ≃ { h : G.Edge × Fin 2 // G.endpoint h.1 h.2 = v }

The two half-edges at a vertex of valence two, enumerated in some order.

theorem TauCeti.DualGraph.halfEdgeOfValenceEqTwo_zero_ne_one {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) : ↑((halfEdgeOfValenceEqTwo hv) 0) ≠ ↑((halfEdgeOfValenceEqTwo hv) 1)

The two enumerated half-edges at a vertex of valence two are distinct.

theorem TauCeti.DualGraph.halfEdgeOfValenceEqTwo_fst_ne {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) : (↑((halfEdgeOfValenceEqTwo hv) 0)).1 ≠ (↑((halfEdgeOfValenceEqTwo hv) 1)).1

At a loopless vertex of valence two, the two half-edges lie on distinct edges.

theorem TauCeti.DualGraph.exists_eq_halfEdgeOfValenceEqTwo {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) {h : G.Edge × Fin 2} (hh : G.endpoint h.1 h.2 = v) : ∃ (k : Fin 2), ↑((halfEdgeOfValenceEqTwo hv) k) = h

Every half-edge at a vertex of valence two is one of the two enumerated half-edges.

noncomputable def TauCeti.DualGraph.bridgeNeighbor {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (k : Fin 2) : G.Vertex

The neighbours of a loopless vertex of valence two: the components carrying the other branches of its two nodes. For a rational bridge, these are the two components that it joins.

theorem TauCeti.DualGraph.endpoint_halfEdgeOfValenceEqTwo_rev {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (k : Fin 2) : G.endpoint (↑((halfEdgeOfValenceEqTwo hv) k)).1 (↑((halfEdgeOfValenceEqTwo hv) k)).2.rev = bridgeNeighbor hv k

The kth neighbour carries the other branch of the kth half-edge.

theorem TauCeti.DualGraph.bridgeNeighbor_ne {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (k : Fin 2) : bridgeNeighbor hv k ≠ v

The neighbours of a loopless vertex are distinct from it.

theorem TauCeti.DualGraph.sym2_bridgeNeighbor_eq {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) {h h' : G.Edge × Fin 2} (hh : G.endpoint h.1 h.2 = v) (hh' : G.endpoint h'.1 h'.2 = v) (hne : h ≠ h') : s(bridgeNeighbor hv 0, bridgeNeighbor hv 1) = s(G.endpoint h.1 h.2.rev, G.endpoint h'.1 h'.2.rev)

The unordered pair of neighbours of a vertex of valence two does not depend on the enumeration of its half-edges: it is formed by the other branches of any two distinct half-edges there.

theorem TauCeti.DualGraph.attachment_eq_of_attachment_eq {ι : Type v} {G : DualGraph ι} {v₁ v₂ : G.Vertex} (hv₁ : G.valence v₁ = 1) (hv₂ : G.valence v₂ = 1) (h : attachment hv₁ = v₂) : attachment hv₂ = v₁

If a vertex of valence one is attached to another vertex of valence one, the latter is attached to the former.

theorem TauCeti.DualGraph.forall_endpoint_ne_of_valence_eq_one {ι : Type v} {G : DualGraph ι} {u v : G.Vertex} (hu : G.valence u = 1) (huv : u ≠ v) (hatt : attachment hu ≠ v) {e : G.Edge} {i : Fin 2} (he : G.endpoint e i = u) (j : Fin 2) : G.endpoint e j ≠ v

The node of a vertex u of valence one avoids every vertex other than u and its attachment.

theorem TauCeti.DualGraph.forall_endpoint_halfEdgeOfValenceEqTwo_ne {ι : Type v} {G : DualGraph ι} {u v : G.Vertex} (hu : G.valence u = 2) (huv : u ≠ v) {k : Fin 2} (hk : bridgeNeighbor hu k ≠ v) (i : Fin 2) : G.endpoint (↑((halfEdgeOfValenceEqTwo hu) k)).1 i ≠ v

The kth half-edge at a vertex u of valence two avoids every vertex other than u and its kth neighbour.

theorem TauCeti.DualGraph.exists_bridgeNeighbor_eq {ι : Type v} {G : DualGraph ι} {u v : G.Vertex} (hu : G.valence u = 2) (hv : G.valence v = 2) {k : Fin 2} (hk : bridgeNeighbor hu k = v) : ∃ (l : Fin 2), bridgeNeighbor hv l = u

If the kth neighbour of a vertex u of valence two is a vertex v of valence two, then u is a neighbour of v.

theorem TauCeti.DualGraph.bridgeNeighbor_rev_ne {ι : Type v} {G : DualGraph ι} {u v : G.Vertex} (hu : G.valence u = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = u → G.endpoint e 1 ≠ u) (hv : G.valence v = 1) {k : Fin 2} (hk : bridgeNeighbor hu k = v) : bridgeNeighbor hu k.rev ≠ v

A vertex of valence one is at most one of the two neighbours of a loopless vertex of valence two.

Edges and half-edges away from a vertex

Contracting a tail

@[reducible, inline]

noncomputable abbrev TauCeti.DualGraph.contractTail {ι : Type v} (G : DualGraph ι) {v : G.Vertex} (hv : G.valence v = 1) : DualGraph ι

The contraction of a vertex v of valence one: v and its unique edge are deleted, and the markings on v move to its attachment. When v is a rational tail, this is the dual graph of the curve obtained by contracting the tail.

@[simp]

theorem TauCeti.DualGraph.endpoint_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) (e : (G.contractTail hv).Edge) (i : Fin 2) : (G.contractTail hv).endpoint e i = ⟨G.endpoint (↑e) i, ⋯⟩

@[simp]

theorem TauCeti.DualGraph.genus_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) (w : (G.contractTail hv).Vertex) : (G.contractTail hv).genus w = G.genus ↑w

@[simp]

theorem TauCeti.DualGraph.marking_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) (i : ι) : (G.contractTail hv).marking i = if h : G.marking i = v then ⟨attachment hv, ⋯⟩ else ⟨G.marking i, h⟩

The markings on the tail move to its attachment; the other markings stay in place.

theorem TauCeti.DualGraph.card_vertex_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) : Fintype.card (G.contractTail hv).Vertex + 1 = Fintype.card G.Vertex

Contracting a tail removes one vertex.

theorem TauCeti.DualGraph.sum_vertex_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) {M : Type u_1} [AddCommMonoid M] (f : G.Vertex → M) : ∑ w : (G.contractTail hv).Vertex, f ↑w = ∑ w : { w : G.Vertex // w ≠ v }, f ↑w

A sum over the vertices of the contracted graph is the sum over the vertices other than v.

theorem TauCeti.DualGraph.card_edge_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) : Fintype.card (G.contractTail hv).Edge + 1 = Fintype.card G.Edge

Contracting a tail removes one edge.

@[simp]

theorem TauCeti.DualGraph.firstBetti_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) : (G.contractTail hv).firstBetti = G.firstBetti

Contracting a tail does not change the first Betti number.

theorem TauCeti.DualGraph.arithmeticGenus_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) : (G.contractTail hv).arithmeticGenus + G.genus v = G.arithmeticGenus

Contracting a tail lowers the arithmetic genus by the genus of the tail.

theorem TauCeti.DualGraph.valence_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) (u : G.Vertex) (hu : u ≠ v) : ((G.contractTail hv).valence ⟨u, hu⟩ + if attachment hv = u then 1 else 0) = G.valence u

Contracting a tail removes one branch at the attachment and leaves the other valences unchanged.

@[simp]

theorem TauCeti.DualGraph.map_val_ends_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) (e : (G.contractTail hv).Edge) : Sym2.map Subtype.val ((G.contractTail hv).ends e) = G.ends ↑e

Contracting a tail does not change the ends of the remaining edges.

theorem TauCeti.DualGraph.coe_attachment_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) {u : G.Vertex} (hu : G.valence u = 1) (huv : u ≠ v) (hatt : attachment hu ≠ v) (hu' : (G.contractTail hv).valence ⟨u, huv⟩ = 1) : ↑(attachment hu') = attachment hu

After contracting a tail v, a vertex of valence one whose node avoids v keeps its attachment.

theorem TauCeti.DualGraph.sym2_coe_bridgeNeighbor_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) {u : G.Vertex} (hu : G.valence u = 2) (huv : u ≠ v) (hnb : ∀ (k : Fin 2), bridgeNeighbor hu k ≠ v) (hu' : (G.contractTail hv).valence ⟨u, huv⟩ = 2) : s(↑(bridgeNeighbor hu' 0), ↑(bridgeNeighbor hu' 1)) = s(bridgeNeighbor hu 0, bridgeNeighbor hu 1)

After contracting a tail v, a vertex of valence two whose neighbours differ from v keeps its neighbours.

theorem TauCeti.DualGraph.valence_contractTail_of_attachment_ne {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) {u : G.Vertex} (hu : u ≠ v) (hatt : attachment hv ≠ u) : (G.contractTail hv).valence ⟨u, hu⟩ = G.valence u

Contracting a tail does not change the valence of a vertex other than its attachment.

theorem TauCeti.DualGraph.forall_endpoint_one_ne_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) {u : G.Vertex} (hu : u ≠ v) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = u → G.endpoint e 1 ≠ u) (e : (G.contractTail hv).Edge) : (G.contractTail hv).endpoint e 0 = ⟨u, hu⟩ → (G.contractTail hv).endpoint e 1 ≠ ⟨u, hu⟩

After contracting a tail, a loopless vertex is still loopless.

theorem TauCeti.DualGraph.marking_contractTail_ne {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) {u : G.Vertex} (hu : u ≠ v) (hm : ∀ (i : ι), G.marking i ≠ u) (hatt : attachment hv ≠ u) (i : ι) : (G.contractTail hv).marking i ≠ ⟨u, hu⟩

After contracting a tail, an unmarked vertex other than its attachment is still unmarked.

@[simp]

theorem TauCeti.DualGraph.numMarkings_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) [Fintype ι] (u : G.Vertex) (hu : u ≠ v) : (G.contractTail hv).numMarkings ⟨u, hu⟩ = G.numMarkings u + if attachment hv = u then G.numMarkings v else 0

Contracting a tail moves its markings to its attachment.

@[simp]

theorem TauCeti.DualGraph.logCanonicalDegree_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 1) [Fintype ι] (u : G.Vertex) (hu : u ≠ v) : (G.contractTail hv).logCanonicalDegree ⟨u, hu⟩ = G.logCanonicalDegree u + if attachment hv = u then ↑(G.numMarkings v) - 1 else 0

Contracting a tail changes only the log-canonical degree of its attachment, which changes by the number of markings on the tail minus one.

theorem TauCeti.DualGraph.IsSemistable.logCanonicalDegree_contractTail {ι : Type v} {G : DualGraph ι} {v : G.Vertex} [Fintype ι] (hG : G.IsSemistable) (ht : G.IsRationalTail v) (hm : G.numMarkings v ≤ 1) (u : G.Vertex) (hu : u ≠ v) : (G.contractTail ⋯).logCanonicalDegree ⟨u, hu⟩ = G.logCanonicalDegree u

In a semistable graph, contracting a rational tail carrying at most one marking does not change the log-canonical degrees of the other vertices: the tail carries exactly one marking, which moves to its attachment.

Contracting a bridge

@[reducible, inline]

noncomputable abbrev TauCeti.DualGraph.contractBridge {ι : Type v} (G : DualGraph ι) {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) : DualGraph ι

The contraction of an unmarked loopless vertex v of valence two: v and its two edges are deleted, and a new edge, the edge none, joins the two neighbours of v. When v is a rational bridge, this is the dual graph of the curve obtained by contracting the bridge.

@[simp]

theorem TauCeti.DualGraph.endpoint_contractBridge_none {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) (k : Fin 2) : (G.contractBridge hv hloop hm).endpoint none k = ⟨bridgeNeighbor hv k, ⋯⟩

The new edge joins the two neighbours of the contracted vertex.

@[simp]

theorem TauCeti.DualGraph.endpoint_contractBridge_some {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) (e : { e : G.Edge // ∀ (i : Fin 2), G.endpoint e i ≠ v }) (i : Fin 2) : (G.contractBridge hv hloop hm).endpoint (some e) i = ⟨G.endpoint (↑e) i, ⋯⟩

@[simp]

theorem TauCeti.DualGraph.genus_contractBridge {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) (w : (G.contractBridge hv hloop hm).Vertex) : (G.contractBridge hv hloop hm).genus w = G.genus ↑w

@[simp]

theorem TauCeti.DualGraph.marking_contractBridge {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) (i : ι) : (G.contractBridge hv hloop hm).marking i = ⟨G.marking i, ⋯⟩

theorem TauCeti.DualGraph.card_vertex_contractBridge {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) : Fintype.card (G.contractBridge hv hloop hm).Vertex + 1 = Fintype.card G.Vertex

Contracting a bridge removes one vertex.

theorem TauCeti.DualGraph.sum_vertex_contractBridge {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) {M : Type u_1} [AddCommMonoid M] (f : G.Vertex → M) : ∑ w : (G.contractBridge hv hloop hm).Vertex, f ↑w = ∑ w : { w : G.Vertex // w ≠ v }, f ↑w

A sum over the vertices of the contracted graph is the sum over the vertices other than v.

theorem TauCeti.DualGraph.card_edge_contractBridge {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) : Fintype.card (G.contractBridge hv hloop hm).Edge + 1 = Fintype.card G.Edge

Contracting a bridge replaces its two edges by one.

@[simp]

theorem TauCeti.DualGraph.firstBetti_contractBridge {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) : (G.contractBridge hv hloop hm).firstBetti = G.firstBetti

Contracting a bridge does not change the first Betti number.

theorem TauCeti.DualGraph.arithmeticGenus_contractBridge {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) : (G.contractBridge hv hloop hm).arithmeticGenus + G.genus v = G.arithmeticGenus

Contracting a bridge lowers the arithmetic genus by the genus of the bridge.

@[simp]

theorem TauCeti.DualGraph.valence_contractBridge {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) (u : G.Vertex) (hu : u ≠ v) : (G.contractBridge hv hloop hm).valence ⟨u, hu⟩ = G.valence u

Contracting a bridge does not change any valence: each neighbour trades a branch of an edge at the bridge for a branch of the new edge.

@[simp]

theorem TauCeti.DualGraph.numMarkings_contractBridge {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) [Fintype ι] (u : G.Vertex) (hu : u ≠ v) : (G.contractBridge hv hloop hm).numMarkings ⟨u, hu⟩ = G.numMarkings u

Contracting a bridge does not move any marking.

@[simp]

theorem TauCeti.DualGraph.logCanonicalDegree_contractBridge {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) [Fintype ι] (u : G.Vertex) (hu : u ≠ v) : (G.contractBridge hv hloop hm).logCanonicalDegree ⟨u, hu⟩ = G.logCanonicalDegree u

Contracting a bridge does not change any log-canonical degree.

theorem TauCeti.DualGraph.forall_endpoint_one_ne_contractBridge {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) {u : G.Vertex} (hu : u ≠ v) (hloopu : ∀ (e : G.Edge), G.endpoint e 0 = u → G.endpoint e 1 ≠ u) {k : Fin 2} (hk : bridgeNeighbor hv k ≠ u) (e : (G.contractBridge hv hloop hm).Edge) : (G.contractBridge hv hloop hm).endpoint e 0 = ⟨u, hu⟩ → (G.contractBridge hv hloop hm).endpoint e 1 ≠ ⟨u, hu⟩

After contracting a bridge, a loopless vertex which is not both neighbours of the bridge is still loopless.

theorem TauCeti.DualGraph.marking_contractBridge_ne {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) {u : G.Vertex} (hu : u ≠ v) (hmu : ∀ (i : ι), G.marking i ≠ u) (i : ι) : (G.contractBridge hv hloop hm).marking i ≠ ⟨u, hu⟩

After contracting a bridge, an unmarked vertex is still unmarked.

@[simp]

theorem TauCeti.DualGraph.map_val_ends_contractBridge_none {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) : Sym2.map Subtype.val ((G.contractBridge hv hloop hm).ends none) = s(bridgeNeighbor hv 0, bridgeNeighbor hv 1)

Contracting a bridge replaces it by a new edge joining its two neighbours.

@[simp]

theorem TauCeti.DualGraph.map_val_ends_contractBridge_some {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) (e : { e : G.Edge // ∀ (i : Fin 2), G.endpoint e i ≠ v }) : Sym2.map Subtype.val ((G.contractBridge hv hloop hm).ends (some e)) = G.ends ↑e

Contracting a bridge does not change the ends of the old edges away from it.

theorem TauCeti.DualGraph.coe_attachment_contractBridge {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) {u : G.Vertex} (hu : G.valence u = 1) (huv : u ≠ v) (hatt : attachment hu ≠ v) (hu' : (G.contractBridge hv hloop hm).valence ⟨u, huv⟩ = 1) : ↑(attachment hu') = attachment hu

After contracting a bridge v, a vertex of valence one whose node avoids v keeps its attachment.

theorem TauCeti.DualGraph.sym2_coe_bridgeNeighbor_contractBridge {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) {u : G.Vertex} (hu : G.valence u = 2) (huv : u ≠ v) (hnb : ∀ (k : Fin 2), bridgeNeighbor hu k ≠ v) (hu' : (G.contractBridge hv hloop hm).valence ⟨u, huv⟩ = 2) : s(↑(bridgeNeighbor hu' 0), ↑(bridgeNeighbor hu' 1)) = s(bridgeNeighbor hu 0, bridgeNeighbor hu 1)

After contracting a bridge v, a vertex of valence two whose neighbours differ from v keeps its neighbours.

theorem TauCeti.DualGraph.sym2_coe_bridgeNeighbor_contractBridge_of_bridgeNeighbor_eq {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) (hloop : ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) (hm : ∀ (i : ι), G.marking i ≠ v) {u : G.Vertex} (hu : G.valence u = 2) (hne : v ≠ u) {k l : Fin 2} (hk : bridgeNeighbor hv k = u) (hl : bridgeNeighbor hu l.rev ≠ v) (hval : (G.contractBridge hv hloop hm).valence ⟨u, ⋯⟩ = 2) : s(↑(bridgeNeighbor hval 0), ↑(bridgeNeighbor hval 1)) = s(bridgeNeighbor hv k.rev, bridgeNeighbor hu l.rev)

After contracting a bridge v adjacent to a vertex u of valence two along a single node, the neighbours of u are the other neighbours of v and of u.

Stabilization

inductive TauCeti.DualGraph.StabilizationStep {ι : Type v} [Fintype ι] : DualGraph ι → DualGraph ι → Prop

A stabilization step: H is obtained from G by contracting a rational tail carrying at most one marking or an unmarked rational bridge. These are the contractions of a component of nonpositive log-canonical degree that again give the dual graph of a pointed nodal curve.

• contractTail {ι : Type v} [Fintype ι] (G : DualGraph ι) {v : G.Vertex} (hv : G.IsRationalTail v) (hm : G.numMarkings v ≤ 1) : G.StabilizationStep (G.contractTail ⋯)

  Contract a rational tail carrying at most one marking.

• contractBridge {ι : Type v} [Fintype ι] (G : DualGraph ι) {v : G.Vertex} (hv : G.IsRationalBridge v) (hm : ∀ (i : ι), G.marking i ≠ v) : G.StabilizationStep (G.contractBridge ⋯ ⋯ hm)

  Contract an unmarked rational bridge.

theorem TauCeti.DualGraph.StabilizationStep.arithmeticGenus_eq {ι : Type v} {G : DualGraph ι} [Fintype ι] {H : DualGraph ι} (h : G.StabilizationStep H) : H.arithmeticGenus = G.arithmeticGenus

A stabilization step preserves the arithmetic genus.

theorem TauCeti.DualGraph.StabilizationStep.card_vertex_lt {ι : Type v} {G : DualGraph ι} [Fintype ι] {H : DualGraph ι} (h : G.StabilizationStep H) : Fintype.card H.Vertex < Fintype.card G.Vertex

A stabilization step removes a vertex.

theorem TauCeti.DualGraph.StabilizationStep.exists_logCanonicalDegree_nonpos {ι : Type v} {G : DualGraph ι} [Fintype ι] {H : DualGraph ι} (h : G.StabilizationStep H) : ∃ (v : G.Vertex), G.logCanonicalDegree v ≤ 0

A stabilization step contracts a vertex of nonpositive log-canonical degree.

theorem TauCeti.DualGraph.IsStable.not_stabilizationStep {ι : Type v} {G : DualGraph ι} [Fintype ι] {H : DualGraph ι} (hG : G.IsStable) : ¬G.StabilizationStep H

A stable graph admits no stabilization step.

theorem TauCeti.DualGraph.arithmeticGenus_eq_of_reflTransGen {ι : Type v} {G : DualGraph ι} [Fintype ι] {H : DualGraph ι} (h : Relation.ReflTransGen StabilizationStep G H) : H.arithmeticGenus = G.arithmeticGenus

Iterated stabilization steps preserve the arithmetic genus.

Labelled stabilization

inductive TauCeti.DualGraph.LabelledStabilizationStep {ι : Type v} [Fintype ι] {α : Type w} (P : α → Prop) : (G : DualGraph ι) × (G.Vertex → α) → (G : DualGraph ι) × (G.Vertex → α) → Prop

A labelled stabilization step. The vertices of the dual graphs carry labels in α; the step contracts a rational tail carrying at most one marking or an unmarked rational bridge whose label satisfies P, and the remaining vertices keep their labels. Thus only vertices whose label satisfies P are ever contracted. With the degree of a map on each component as label and P saying that the degree is zero, these are the steps of map-aware stabilization; with labels in Unit and P always true, they are the stabilization steps (TauCeti.DualGraph.StabilizationStep.labelledStabilizationStep).

• contractTail {ι : Type v} [Fintype ι] {α : Type w} {P : α → Prop} {G : DualGraph ι} (c : G.Vertex → α) {v : G.Vertex} (hv : G.IsRationalTail v) (hm : G.numMarkings v ≤ 1) (hc : P (c v)) : LabelledStabilizationStep P ⟨G, c⟩ ⟨G.contractTail ⋯, fun (w : (G.contractTail ⋯).Vertex) => c ↑w⟩

  Contract a rational tail carrying at most one marking, whose label satisfies P.

• contractBridge {ι : Type v} [Fintype ι] {α : Type w} {P : α → Prop} {G : DualGraph ι} (c : G.Vertex → α) {v : G.Vertex} (hv : G.IsRationalBridge v) (hm : ∀ (i : ι), G.marking i ≠ v) (hc : P (c v)) : LabelledStabilizationStep P ⟨G, c⟩ ⟨G.contractBridge ⋯ ⋯ hm, fun (w : (G.contractBridge ⋯ ⋯ hm).Vertex) => c ↑w⟩

  Contract an unmarked rational bridge whose label satisfies P.

theorem TauCeti.DualGraph.LabelledStabilizationStep.fst {ι : Type v} [Fintype ι] {α : Type w} {P : α → Prop} {x y : (G : DualGraph ι) × (G.Vertex → α)} (h : LabelledStabilizationStep P x y) : x.fst.StabilizationStep y.fst

A labelled stabilization step is a stabilization step of the underlying graphs.

theorem TauCeti.DualGraph.LabelledStabilizationStep.exists_logCanonicalDegree_nonpos {ι : Type v} [Fintype ι] {α : Type w} {P : α → Prop} {x y : (G : DualGraph ι) × (G.Vertex → α)} (h : LabelledStabilizationStep P x y) : ∃ (v : x.fst.Vertex), P (x.snd v) ∧ x.fst.logCanonicalDegree v ≤ 0

A labelled stabilization step contracts a vertex whose label satisfies P and whose log-canonical degree is nonpositive.

theorem TauCeti.DualGraph.LabelledStabilizationStep.forall_snd_iff {ι : Type v} [Fintype ι] {α : Type w} {P : α → Prop} {x y : (G : DualGraph ι) × (G.Vertex → α)} (h : LabelledStabilizationStep P x y) : (∀ (w : y.fst.Vertex), P (y.snd w)) ↔ ∀ (v : x.fst.Vertex), P (x.snd v)

Since the contracted vertex has a label satisfying P and the other vertices keep their labels, all labels satisfy P after a labelled stabilization step exactly when they did before.

theorem TauCeti.DualGraph.LabelledStabilizationStep.two_mul_arithmeticGenus_sub_two_add_card_pos {ι : Type v} [Fintype ι] {α : Type w} {P : α → Prop} {x y : (G : DualGraph ι) × (G.Vertex → α)} (h : LabelledStabilizationStep P x y) (hrange : (∀ (v : x.fst.Vertex), P (x.snd v)) → 0 < 2 * ↑x.fst.arithmeticGenus - 2 + ↑(Fintype.card ι)) : (∀ (w : y.fst.Vertex), P (y.snd w)) → 0 < 2 * ↑y.fst.arithmeticGenus - 2 + ↑(Fintype.card ι)

The stable range condition 2g - 2 + n > 0, required only when all labels satisfy P, persists along a labelled stabilization step.

theorem TauCeti.DualGraph.StabilizationStep.labelledStabilizationStep {ι : Type v} {G : DualGraph ι} [Fintype ι] {H : DualGraph ι} (h : G.StabilizationStep H) : LabelledStabilizationStep (fun (x : Unit) => True) ⟨G, fun (x : G.Vertex) => ()⟩ ⟨H, fun (x : H.Vertex) => ()⟩

A stabilization step is a labelled stabilization step for the constant labelling by Unit, in which every vertex may be contracted.

theorem TauCeti.DualGraph.reflTransGen_labelledStabilizationStep_of_reflTransGen {ι : Type v} {G : DualGraph ι} [Fintype ι] {H : DualGraph ι} (h : Relation.ReflTransGen StabilizationStep G H) : Relation.ReflTransGen (LabelledStabilizationStep fun (x : Unit) => True) ⟨G, fun (x : G.Vertex) => ()⟩ ⟨H, fun (x : H.Vertex) => ()⟩

Iterated stabilization steps are iterated labelled stabilization steps for the constant labelling by Unit.

theorem TauCeti.DualGraph.exists_reflTransGen_labelledStabilizationStep_forall_not {ι : Type v} [Fintype ι] {α : Type w} {P : α → Prop} (x : (G : DualGraph ι) × (G.Vertex → α)) : ∃ (y : (G : DualGraph ι) × (G.Vertex → α)), Relation.ReflTransGen (LabelledStabilizationStep P) x y ∧ ∀ (z : (G : DualGraph ι) × (G.Vertex → α)), ¬LabelledStabilizationStep P y z

Labelled stabilization terminates. Iterating labelled stabilization steps from any labelled graph reaches one admitting no further step, since every step removes a vertex.

theorem TauCeti.DualGraph.exists_stabilizationStep_of_not_isStable {ι : Type v} (G : DualGraph ι) [Fintype ι] (hrange : 0 < 2 * ↑G.arithmeticGenus - 2 + ↑(Fintype.card ι)) (hG : ¬G.IsStable) : ∃ (H : DualGraph ι), G.StabilizationStep H

In the stable range 2g - 2 + n > 0, a graph that is not stable admits a stabilization step. A vertex of nonpositive log-canonical degree is a rational tail with at most one marking, a rational bridge without markings, or the only vertex; in the last case its log-canonical degree is 2g - 2 + n.

theorem TauCeti.DualGraph.isStable_iff_forall_not_stabilizationStep {ι : Type v} (G : DualGraph ι) [Fintype ι] (hrange : 0 < 2 * ↑G.arithmeticGenus - 2 + ↑(Fintype.card ι)) : G.IsStable ↔ ∀ (H : DualGraph ι), ¬G.StabilizationStep H

In the stable range 2g - 2 + n > 0, a graph is stable exactly when it admits no stabilization step.

theorem TauCeti.DualGraph.exists_reflTransGen_stabilizationStep_isStable {ι : Type v} (G : DualGraph ι) [Fintype ι] (hrange : 0 < 2 * ↑G.arithmeticGenus - 2 + ↑(Fintype.card ι)) : ∃ (H : DualGraph ι), Relation.ReflTransGen StabilizationStep G H ∧ H.IsStable

Stabilization terminates. In the stable range 2g - 2 + n > 0, iterating stabilization steps from any graph reaches a stable graph, of the same arithmetic genus by TauCeti.DualGraph.arithmeticGenus_eq_of_reflTransGen. Termination holds because every step removes a vertex.