Dual graphs of nodal curves

The dual graph of a proper nodal curve X over an algebraically closed field records how the curve is assembled from smooth pieces. Its vertices are the irreducible components of the normalization of X, its edges are the nodes of X, and the two endpoints of an edge are the components carrying the two branches of the node; when both branches lie on one component the edge is a loop. Each vertex is labelled by the genus of its normalized component, and each marking of a pointed curve is attached to the component on which it lies.

This file introduces that combinatorial structure, TauCeti.DualGraph, together with the numerical invariants through which the geometry of the curve is read off from it:

• the valence of a vertex, the number of branches of nodes on the component, so that a loop counts twice;
• the first Betti number b₁ = #edges - #vertices + 1 of the connected graph and the arithmetic genus pₐ = ∑ᵥ gᵥ + b₁ encoded by the graph;
• the log-canonical degree 2gᵥ - 2 + val(v) + n(v) of a vertex carrying n(v) markings, which is the degree of ω_X(s₁ + ⋯ + sₙ) on the corresponding component.

A pointed nodal curve is stable exactly when every component has positive log-canonical degree, and semistable when none has negative degree; TauCeti.DualGraph.IsStable and TauCeti.DualGraph.IsSemistable are these conditions on the graph.

Main results

• TauCeti.DualGraph.sum_valence: the handshake identity ∑ᵥ val(v) = 2 · #edges.
• TauCeti.DualGraph.card_vertex_le_card_edge_add_one: a connected graph has at most one more vertex than it has edges, so the first Betti number is computed without truncation (TauCeti.DualGraph.firstBetti_add_card_vertex).
• TauCeti.DualGraph.sum_logCanonicalDegree: the log-canonical degrees add up to 2pₐ - 2 + n, the total degree of ω_X(s₁ + ⋯ + sₙ).
• TauCeti.DualGraph.IsStable.card_vertex_le and TauCeti.DualGraph.IsStable.card_edge_le: a stable graph of genus g with n markings has at most 2g - 2 + n vertices and at most 3g - 3 + n edges.
• TauCeti.DualGraph.isSemistable_iff_forall_not_isRationalTail: an unmarked graph of arithmetic genus at least one is semistable exactly when it has no rational tails, and TauCeti.DualGraph.isStable_iff_forall_not_isRationalTail_and_not_isRationalBridge: an unmarked graph of arithmetic genus at least two is stable exactly when it has neither rational tails nor rational bridges.
• TauCeti.DualGraph.isRationalTail_or_isRationalBridge_of_logCanonicalDegree_nonpos: a vertex of nonpositive log-canonical degree other than the only vertex is a rational tail with at most one marking or an unmarked rational bridge. In the stable range 2g - 2 + n > 0, a vertex of log-canonical degree zero is a rational tail with exactly one marking or an unmarked rational bridge (TauCeti.DualGraph.isRationalTail_or_isRationalBridge_of_logCanonicalDegree_eq_zero).

Reindexing

TauCeti.DualGraph.reindex reindexes the markings along a map e : κ → ι, keeping the curve and taking the e i-th marking as the new i-th marking. Along an equivalence it reorders the markings and preserves log-canonical degrees, stability and semistability; along some : ι → Option ι it forgets the marking none.

Implementation notes

An edge carries an ordered pair of endpoints, so the two branches of a node are always two distinct half-edges, even for a loop. Valence counts half-edges, which is what makes a loop contribute two, matching the two points of the normalization lying over a self-node.

Rational tails and rational bridges are defined without reference to markings, as in the unpointed theory of the Stacks Project; the characterizations of stability through them are stated for unmarked graphs.

References

• Stacks, Tag 0E6X (semistable curves) and Stacks, Tag 0E73 (stable curves).
• E. Arbarello, M. Cornalba and P. A. Griffiths, Geometry of Algebraic Curves, Volume II, Chapter X, for dual graphs of pointed nodal curves.

structure TauCeti.DualGraph (ι : Type v) : Type (max (u + 1) v)

The dual graph of a proper nodal curve over an algebraically closed field, with markings indexed by ι.

Vertex is the finite nonempty set of irreducible components of the normalization, Edge is the finite set of nodes, endpoint e 0 and endpoint e 1 are the components carrying the two branches of the node e, genus v is the genus of the normalized component v, and marking i is the component carrying the i-th marking. The curve is connected, so the graph is.

• Vertex : Type u

  The finite nonempty type of vertices: the components of the normalization.

• vertexFintype : Fintype self.Vertex

  The vertices form a finite type.

• vertexDecidableEq : DecidableEq self.Vertex

  Equality of vertices is decidable.

• vertexNonempty : Nonempty self.Vertex

  There is at least one vertex.

• Edge : Type u

  The finite type of edges: the nodes.

• edgeFintype : Fintype self.Edge

  The edges form a finite type.

• edgeDecidableEq : DecidableEq self.Edge

  Equality of edges is decidable.

• endpoint : self.Edge → Fin 2 → self.Vertex

  The components carrying the two branches of a node.

• genus : self.Vertex → ℕ

  The genus of a normalized component.

• marking : ι → self.Vertex

  The component carrying a marking.

• connected (v w : self.Vertex) : Relation.ReflTransGen (fun (v w : self.Vertex) => ∃ (e : self.Edge), self.endpoint e 0 = v ∧ self.endpoint e 1 = w ∨ self.endpoint e 0 = w ∧ self.endpoint e 1 = v) v w

  Any two vertices are joined by a chain of edges.

@[instance_reducible]

instance TauCeti.DualGraph.instFintypeVertex {ι : Type v} (G : DualGraph ι) : Fintype G.Vertex

@[instance_reducible]

instance TauCeti.DualGraph.instDecidableEqVertex {ι : Type v} (G : DualGraph ι) : DecidableEq G.Vertex

instance TauCeti.DualGraph.instNonemptyVertex {ι : Type v} (G : DualGraph ι) : Nonempty G.Vertex

@[instance_reducible]

instance TauCeti.DualGraph.instFintypeEdge {ι : Type v} (G : DualGraph ι) : Fintype G.Edge

@[instance_reducible]

instance TauCeti.DualGraph.instDecidableEqEdge {ι : Type v} (G : DualGraph ι) : DecidableEq G.Edge

Adjacency and connectedness

def TauCeti.DualGraph.Adj {ι : Type v} (G : DualGraph ι) (v w : G.Vertex) : Prop

Two vertices are adjacent when they are the two endpoints of some edge, in either order. A vertex carrying a loop is adjacent to itself.

theorem TauCeti.DualGraph.adj_iff {ι : Type v} {G : DualGraph ι} {v w : G.Vertex} : G.Adj v w ↔ ∃ (e : G.Edge), G.endpoint e 0 = v ∧ G.endpoint e 1 = w ∨ G.endpoint e 0 = w ∧ G.endpoint e 1 = v

theorem TauCeti.DualGraph.Adj.symm {ι : Type v} {G : DualGraph ι} {v w : G.Vertex} (h : G.Adj v w) : G.Adj w v

theorem TauCeti.DualGraph.reflTransGen_adj {ι : Type v} (G : DualGraph ι) (v w : G.Vertex) : Relation.ReflTransGen G.Adj v w

Any two vertices are joined by a chain of adjacencies.

def TauCeti.DualGraph.ends {ι : Type v} (G : DualGraph ι) (e : G.Edge) : Sym2 G.Vertex

The unordered pair of endpoints of an edge: the components carrying the two branches of the node, without distinguishing the branches.

theorem TauCeti.DualGraph.ends_def {ι : Type v} (G : DualGraph ι) (e : G.Edge) : G.ends e = s(G.endpoint e 0, G.endpoint e 1)

The ends of an edge are its two endpoints.

@[simp]

theorem TauCeti.DualGraph.mem_ends_iff {ι : Type v} {G : DualGraph ι} {v : G.Vertex} {e : G.Edge} : v ∈ G.ends e ↔ ∃ (i : Fin 2), G.endpoint e i = v

A vertex lies on an edge exactly when it carries one of its branches.

theorem TauCeti.DualGraph.forall_endpoint_ne_iff {ι : Type v} {G : DualGraph ι} {v : G.Vertex} {e : G.Edge} : (∀ (i : Fin 2), G.endpoint e i ≠ v) ↔ v ∉ G.ends e

An edge avoids a vertex exactly when neither of its branches lies there.

theorem TauCeti.DualGraph.forall_endpoint_ne_of_ne_of_rev_ne {ι : Type v} {G : DualGraph ι} {v : G.Vertex} {e : G.Edge} {i : Fin 2} (h : G.endpoint e i ≠ v) (h' : G.endpoint e i.rev ≠ v) (j : Fin 2) : G.endpoint e j ≠ v

An edge avoids v when neither of its branches lies there.

theorem TauCeti.DualGraph.forall_endpoint_one_ne_iff {ι : Type v} {G : DualGraph ι} {v : G.Vertex} : (∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v) ↔ ∀ (e : G.Edge), G.ends e ≠ s(v, v)

A vertex carries no loop exactly when no edge has both of its ends there.

def TauCeti.DualGraph.toSimpleGraph {ι : Type v} (G : DualGraph ι) : SimpleGraph G.Vertex

The simple graph on the vertices joining two distinct vertices when some edge does.

@[simp]

theorem TauCeti.DualGraph.toSimpleGraph_adj {ι : Type v} (G : DualGraph ι) {v w : G.Vertex} : G.toSimpleGraph.Adj v w ↔ v ≠ w ∧ G.Adj v w

theorem TauCeti.DualGraph.toSimpleGraph_connected {ι : Type v} (G : DualGraph ι) : G.toSimpleGraph.Connected

The simple graph underlying a dual graph is connected.

theorem TauCeti.DualGraph.connected_of_surjective {ι : Type v} {G : DualGraph ι} {V : Type u_1} {E : Type u_2} {f : E → Fin 2 → V} (φ : G.Vertex → V) (hφ : Function.Surjective φ) (h : ∀ (e : G.Edge), φ (G.endpoint e 0) = φ (G.endpoint e 1) ∨ ∃ (e' : E), f e' 0 = φ (G.endpoint e 0) ∧ f e' 1 = φ (G.endpoint e 1) ∨ f e' 0 = φ (G.endpoint e 1) ∧ f e' 1 = φ (G.endpoint e 0)) (x y : V) : Relation.ReflTransGen (fun (v w : V) => ∃ (e : E), f e 0 = v ∧ f e 1 = w ∨ f e 0 = w ∧ f e 1 = v) x y

A connectivity criterion for a graph built on the image of a surjection φ from the vertices of G: it suffices that each edge of G is either collapsed by φ or carried by φ to an edge of the new graph, in either orientation.

theorem TauCeti.DualGraph.eq_of_forall_endpoint_zero_eq_iff {ι : Type v} (G : DualGraph ι) {v : G.Vertex} (h : ∀ (e : G.Edge), G.endpoint e 0 = v ↔ G.endpoint e 1 = v) (w : G.Vertex) : w = v

If every edge at v is a loop, then v is the only vertex: no edge leaves it, and the graph is connected.

theorem TauCeti.DualGraph.card_vertex_le_card_edge_add_one {ι : Type v} (G : DualGraph ι) : Fintype.card G.Vertex ≤ Fintype.card G.Edge + 1

A connected graph has at most one more vertex than it has edges.

Valence and markings

def TauCeti.DualGraph.valence {ι : Type v} (G : DualGraph ι) (v : G.Vertex) : ℕ

The valence of a vertex: the number of branches of nodes lying on the component, that is, the number of half-edges at the vertex. A loop counts twice.

theorem TauCeti.DualGraph.valence_def {ι : Type v} (G : DualGraph ι) (v : G.Vertex) : G.valence v = {h : G.Edge × Fin 2 | G.endpoint h.1 h.2 = v}.card

theorem TauCeti.DualGraph.valence_eq_sum {ι : Type v} (G : DualGraph ι) (v : G.Vertex) : G.valence v = ∑ e : G.Edge, {i : Fin 2 | G.endpoint e i = v}.card

The valence of a vertex is the sum over the edges of the number of their branches at it.

theorem TauCeti.DualGraph.sum_valence {ι : Type v} (G : DualGraph ι) : ∑ v : G.Vertex, G.valence v = 2 * Fintype.card G.Edge

The handshake identity: the valences add up to twice the number of edges.

theorem TauCeti.DualGraph.valence_eq_zero_iff {ι : Type v} (G : DualGraph ι) {v : G.Vertex} : G.valence v = 0 ↔ ∀ (e : G.Edge) (i : Fin 2), G.endpoint e i ≠ v

def TauCeti.DualGraph.numMarkings {ι : Type v} (G : DualGraph ι) [Fintype ι] (v : G.Vertex) : ℕ

The number of markings carried by a vertex.

theorem TauCeti.DualGraph.numMarkings_def {ι : Type v} (G : DualGraph ι) [Fintype ι] (v : G.Vertex) : G.numMarkings v = {i : ι | G.marking i = v}.card

theorem TauCeti.DualGraph.numMarkings_eq_zero_iff {ι : Type v} (G : DualGraph ι) [Fintype ι] {v : G.Vertex} : G.numMarkings v = 0 ↔ ∀ (i : ι), G.marking i ≠ v

A vertex carries no markings exactly when every marking lies elsewhere.

theorem TauCeti.DualGraph.sum_numMarkings {ι : Type v} (G : DualGraph ι) [Fintype ι] : ∑ v : G.Vertex, G.numMarkings v = Fintype.card ι

Every marking lies on exactly one component.

@[simp]

theorem TauCeti.DualGraph.numMarkings_of_isEmpty {ι : Type v} (G : DualGraph ι) [Fintype ι] [IsEmpty ι] (v : G.Vertex) : G.numMarkings v = 0

Betti number and arithmetic genus

def TauCeti.DualGraph.firstBetti {ι : Type v} (G : DualGraph ι) : ℕ

The first Betti number #edges - #vertices + 1 of the connected graph.

theorem TauCeti.DualGraph.firstBetti_def {ι : Type v} (G : DualGraph ι) : G.firstBetti = Fintype.card G.Edge + 1 - Fintype.card G.Vertex

theorem TauCeti.DualGraph.firstBetti_add_card_vertex {ι : Type v} (G : DualGraph ι) : G.firstBetti + Fintype.card G.Vertex = Fintype.card G.Edge + 1

The first Betti number is computed without truncation.

def TauCeti.DualGraph.arithmeticGenus {ι : Type v} (G : DualGraph ι) : ℕ

The arithmetic genus encoded by the graph: the sum of the genera of the components and the first Betti number.

theorem TauCeti.DualGraph.arithmeticGenus_def {ι : Type v} (G : DualGraph ι) : G.arithmeticGenus = ∑ v : G.Vertex, G.genus v + G.firstBetti

theorem TauCeti.DualGraph.genus_le_arithmeticGenus {ι : Type v} (G : DualGraph ι) (v : G.Vertex) : G.genus v ≤ G.arithmeticGenus

A component's genus is at most the arithmetic genus of the whole graph.

theorem TauCeti.DualGraph.arithmeticGenus_add_card_vertex {ι : Type v} (G : DualGraph ι) : G.arithmeticGenus + Fintype.card G.Vertex = ∑ v : G.Vertex, G.genus v + Fintype.card G.Edge + 1

The arithmetic genus in terms of the numbers of vertices and edges.

theorem TauCeti.DualGraph.two_mul_arithmeticGenus_of_forall_endpoint_zero_eq_iff {ι : Type v} (G : DualGraph ι) {v : G.Vertex} (h : ∀ (e : G.Edge), G.endpoint e 0 = v ↔ G.endpoint e 1 = v) : 2 * G.arithmeticGenus = 2 * G.genus v + G.valence v

If every edge at v is a loop, the graph has the single vertex v, and twice its arithmetic genus is 2 g(v) + val(v).

Log-canonical degree and stability

def TauCeti.DualGraph.logCanonicalDegree {ι : Type v} (G : DualGraph ι) [Fintype ι] (v : G.Vertex) : ℤ

The log-canonical degree 2 g(v) - 2 + val(v) + n(v) of a vertex carrying n(v) markings. This is the numerical value that the degree of ω_X(s₁ + ⋯ + sₙ) takes on the corresponding component of a pointed nodal curve.

theorem TauCeti.DualGraph.logCanonicalDegree_def {ι : Type v} (G : DualGraph ι) [Fintype ι] (v : G.Vertex) : G.logCanonicalDegree v = 2 * ↑(G.genus v) - 2 + ↑(G.valence v) + ↑(G.numMarkings v)

theorem TauCeti.DualGraph.sum_logCanonicalDegree {ι : Type v} (G : DualGraph ι) [Fintype ι] : ∑ v : G.Vertex, G.logCanonicalDegree v = 2 * ↑G.arithmeticGenus - 2 + ↑(Fintype.card ι)

The log-canonical degrees add up to 2pₐ - 2 + n.

theorem TauCeti.DualGraph.logCanonicalDegree_eq_of_forall_eq {ι : Type v} (G : DualGraph ι) [Fintype ι] {v : G.Vertex} (h : ∀ (w : G.Vertex), w = v) : G.logCanonicalDegree v = 2 * ↑G.arithmeticGenus - 2 + ↑(Fintype.card ι)

The log-canonical degree of the only vertex of a graph is 2pₐ - 2 + n.

theorem TauCeti.DualGraph.logCanonicalDegree_nonpos_iff {ι : Type v} (G : DualGraph ι) [Fintype ι] {v : G.Vertex} : G.logCanonicalDegree v ≤ 0 ↔ G.genus v = 0 ∧ G.valence v + G.numMarkings v ≤ 2 ∨ G.genus v = 1 ∧ G.valence v = 0 ∧ G.numMarkings v = 0

A vertex has nonpositive log-canonical degree exactly when it is a rational component with at most two special points, or a component of genus one with none.

theorem TauCeti.DualGraph.logCanonicalDegree_neg_iff {ι : Type v} (G : DualGraph ι) [Fintype ι] {v : G.Vertex} : G.logCanonicalDegree v < 0 ↔ G.genus v = 0 ∧ G.valence v + G.numMarkings v ≤ 1

A vertex has negative log-canonical degree exactly when it is a rational component with at most one special point.

def TauCeti.DualGraph.IsStable {ι : Type v} (G : DualGraph ι) [Fintype ι] : Prop

A graph is stable when every vertex has positive log-canonical degree.

theorem TauCeti.DualGraph.isStable_iff {ι : Type v} (G : DualGraph ι) [Fintype ι] : G.IsStable ↔ ∀ (v : G.Vertex), 0 < G.logCanonicalDegree v

def TauCeti.DualGraph.IsSemistable {ι : Type v} (G : DualGraph ι) [Fintype ι] : Prop

A graph is semistable when no vertex has negative log-canonical degree.

theorem TauCeti.DualGraph.isSemistable_iff {ι : Type v} (G : DualGraph ι) [Fintype ι] : G.IsSemistable ↔ ∀ (v : G.Vertex), 0 ≤ G.logCanonicalDegree v

theorem TauCeti.DualGraph.IsStable.isSemistable {ι : Type v} {G : DualGraph ι} [Fintype ι] (hG : G.IsStable) : G.IsSemistable

theorem TauCeti.DualGraph.IsStable.card_vertex_le {ι : Type v} {G : DualGraph ι} [Fintype ι] (hG : G.IsStable) : ↑(Fintype.card G.Vertex) ≤ 2 * ↑G.arithmeticGenus - 2 + ↑(Fintype.card ι)

A stable graph of genus g with n markings has at most 2g - 2 + n vertices.

theorem TauCeti.DualGraph.IsStable.card_edge_le {ι : Type v} {G : DualGraph ι} [Fintype ι] (hG : G.IsStable) : ↑(Fintype.card G.Edge) ≤ 3 * ↑G.arithmeticGenus - 3 + ↑(Fintype.card ι)

A stable graph of genus g with n markings has at most 3g - 3 + n edges.

theorem TauCeti.DualGraph.IsStable.two_mul_arithmeticGenus_sub_two_add_card_pos {ι : Type v} {G : DualGraph ι} [Fintype ι] (hG : G.IsStable) : 0 < 2 * ↑G.arithmeticGenus - 2 + ↑(Fintype.card ι)

The stable range: a stable graph of genus g with n markings has 2g - 2 + n > 0.

Rational tails and rational bridges

def TauCeti.DualGraph.IsRationalTail {ι : Type v} (G : DualGraph ι) (v : G.Vertex) : Prop

A rational tail: a rational component meeting the rest of the curve in a single point.

theorem TauCeti.DualGraph.isRationalTail_iff {ι : Type v} (G : DualGraph ι) {v : G.Vertex} : G.IsRationalTail v ↔ G.genus v = 0 ∧ G.valence v = 1

def TauCeti.DualGraph.IsRationalBridge {ι : Type v} (G : DualGraph ι) (v : G.Vertex) : Prop

A rational bridge: a smooth rational component meeting the rest of the curve in exactly two points, so a rational component of valence two carrying no loop.

theorem TauCeti.DualGraph.isRationalBridge_iff {ι : Type v} (G : DualGraph ι) {v : G.Vertex} : G.IsRationalBridge v ↔ G.genus v = 0 ∧ G.valence v = 2 ∧ ∀ (e : G.Edge), G.endpoint e 0 = v → G.endpoint e 1 ≠ v

theorem TauCeti.DualGraph.IsRationalTail.logCanonicalDegree_eq {ι : Type v} {G : DualGraph ι} [Fintype ι] {v : G.Vertex} (hv : G.IsRationalTail v) : G.logCanonicalDegree v = -1 + ↑(G.numMarkings v)

A rational tail has log-canonical degree -1 + n(v).

theorem TauCeti.DualGraph.IsRationalBridge.logCanonicalDegree_eq {ι : Type v} {G : DualGraph ι} [Fintype ι] {v : G.Vertex} (hv : G.IsRationalBridge v) : G.logCanonicalDegree v = ↑(G.numMarkings v)

A rational bridge has log-canonical degree n(v).

theorem TauCeti.DualGraph.endpoint_eq_iff_eq_of_valence_eq_two {ι : Type v} {G : DualGraph ι} {v : G.Vertex} (hv : G.valence v = 2) {e : G.Edge} (he₀ : G.endpoint e 0 = v) (he₁ : G.endpoint e 1 = v) (e' : G.Edge) (i : Fin 2) : G.endpoint e' i = v ↔ e' = e

If a vertex of valence two carries a loop e, the loop accounts for both half-edges at the vertex: an edge has an endpoint there exactly when it is e.

theorem TauCeti.DualGraph.isRationalTail_or_isRationalBridge_of_logCanonicalDegree_nonpos {ι : Type v} {G : DualGraph ι} [Fintype ι] {v : G.Vertex} (hv : G.logCanonicalDegree v ≤ 0) (hw : ∃ (w : G.Vertex), w ≠ v) : G.IsRationalTail v ∧ G.numMarkings v ≤ 1 ∨ G.IsRationalBridge v ∧ ∀ (i : ι), G.marking i ≠ v

A vertex of nonpositive log-canonical degree in a graph with at least one other vertex is a rational tail with at most one marking or an unmarked rational bridge.

theorem TauCeti.DualGraph.isRationalTail_or_isRationalBridge_of_logCanonicalDegree_eq_zero {ι : Type v} {G : DualGraph ι} [Fintype ι] (hrange : 0 < 2 * ↑G.arithmeticGenus - 2 + ↑(Fintype.card ι)) {v : G.Vertex} (hv : G.logCanonicalDegree v = 0) : G.IsRationalTail v ∧ G.numMarkings v = 1 ∨ G.IsRationalBridge v ∧ ∀ (i : ι), G.marking i ≠ v

In the stable range 2g - 2 + n > 0, a vertex of log-canonical degree zero is a rational tail carrying exactly one marking or an unmarked rational bridge.

theorem TauCeti.DualGraph.isSemistable_iff_forall_not_isRationalTail {ι : Type v} {G : DualGraph ι} [Fintype ι] [IsEmpty ι] (hg : 1 ≤ G.arithmeticGenus) : G.IsSemistable ↔ ∀ (v : G.Vertex), ¬G.IsRationalTail v

An unmarked graph of arithmetic genus at least one is semistable exactly when it has no rational tails.

theorem TauCeti.DualGraph.isStable_iff_forall_not_isRationalTail_and_not_isRationalBridge {ι : Type v} {G : DualGraph ι} [Fintype ι] [IsEmpty ι] (hg : 2 ≤ G.arithmeticGenus) : G.IsStable ↔ ∀ (v : G.Vertex), ¬G.IsRationalTail v ∧ ¬G.IsRationalBridge v

An unmarked graph of arithmetic genus at least two is stable exactly when it has neither rational tails nor rational bridges.

Reindexing the markings

@[reducible, inline]

abbrev TauCeti.DualGraph.reindex {ι : Type v} (G : DualGraph ι) {κ : Type u_1} (e : κ → ι) : DualGraph κ

The dual graph with markings reindexed along e : κ → ι: the same curve, with the e i-th marking of G as its i-th marking. Along an equivalence this reorders the markings, and along some : ι → Option ι it forgets the marking none.

@[simp]

theorem TauCeti.DualGraph.reindex_id {ι : Type v} (G : DualGraph ι) : G.reindex id = G

@[simp]

theorem TauCeti.DualGraph.reindex_reindex {ι : Type v} (G : DualGraph ι) {κ : Type u_1} (e : κ → ι) {μ : Type u_2} (f : μ → κ) : (G.reindex e).reindex f = G.reindex (e ∘ f)

Reindexing twice is reindexing along the composite.

@[simp]

theorem TauCeti.DualGraph.endpoint_reindex {ι : Type v} (G : DualGraph ι) {κ : Type u_1} (e : κ → ι) (x : G.Edge) (i : Fin 2) : (G.reindex e).endpoint x i = G.endpoint x i

@[simp]

theorem TauCeti.DualGraph.genus_reindex {ι : Type v} (G : DualGraph ι) {κ : Type u_1} (e : κ → ι) (x : G.Vertex) : (G.reindex e).genus x = G.genus x

@[simp]

theorem TauCeti.DualGraph.marking_reindex {ι : Type v} (G : DualGraph ι) {κ : Type u_1} (e : κ → ι) (i : κ) : (G.reindex e).marking i = G.marking (e i)

@[simp]

theorem TauCeti.DualGraph.valence_reindex {ι : Type v} (G : DualGraph ι) {κ : Type u_1} (e : κ → ι) (x : G.Vertex) : (G.reindex e).valence x = G.valence x

Reindexing the markings does not change the valences.

@[simp]

theorem TauCeti.DualGraph.arithmeticGenus_reindex {ι : Type v} (G : DualGraph ι) {κ : Type u_1} (e : κ → ι) : (G.reindex e).arithmeticGenus = G.arithmeticGenus

Reindexing the markings does not change the arithmetic genus.

@[simp]

theorem TauCeti.DualGraph.numMarkings_reindex_equiv {ι : Type v} (G : DualGraph ι) {κ : Type u_1} [Fintype ι] [Fintype κ] (e : κ ≃ ι) (x : G.Vertex) : (G.reindex ⇑e).numMarkings x = G.numMarkings x

Reindexing along an equivalence does not change the number of markings on a vertex.

@[simp]

theorem TauCeti.DualGraph.logCanonicalDegree_reindex_equiv {ι : Type v} (G : DualGraph ι) {κ : Type u_1} [Fintype ι] [Fintype κ] (e : κ ≃ ι) (x : G.Vertex) : (G.reindex ⇑e).logCanonicalDegree x = G.logCanonicalDegree x

Reindexing along an equivalence does not change the log-canonical degrees.

@[simp]

theorem TauCeti.DualGraph.isStable_reindex_equiv_iff {ι : Type v} (G : DualGraph ι) {κ : Type u_1} [Fintype ι] [Fintype κ] (e : κ ≃ ι) : (G.reindex ⇑e).IsStable ↔ G.IsStable

Reindexing along an equivalence preserves stability.

@[simp]

theorem TauCeti.DualGraph.isSemistable_reindex_equiv_iff {ι : Type v} (G : DualGraph ι) {κ : Type u_1} [Fintype ι] [Fintype κ] (e : κ ≃ ι) : (G.reindex ⇑e).IsSemistable ↔ G.IsSemistable

Reindexing along an equivalence preserves semistability.