Clutching dual graphs

Pointed nodal curves are glued along markings by the two clutching operations of Knudsen. In external clutching, two pointed curves with marking sets I ⊔ {a} and J ⊔ {b} are glued by identifying the points a and b, which become a new node; the result carries the markings I ⊔ J. In self-clutching, one pointed curve with marking set I ⊔ {a, b} is glued to itself by identifying a with b; the result carries the markings I.

This file describes the effect of both operations on dual graphs.

• TauCeti.DualGraph.clutch G₁ G₂: for dual graphs G₁ and G₂ with markings indexed by Option ι and Option κ, the extra marking being none, the disjoint union of G₁ and G₂ with one new edge joining the components carrying the two none markings; its markings are indexed by ι ⊕ κ.
• TauCeti.DualGraph.selfClutch G: for a dual graph G with markings indexed by ι ⊕ Fin 2, the graph G with one new edge joining the components carrying the two markings Sum.inr 0 and Sum.inr 1, a loop when both lie on the same component; its markings are indexed by ι.

Main results

• TauCeti.DualGraph.arithmeticGenus_clutch and TauCeti.DualGraph.firstBetti_clutch: external clutching adds the arithmetic genera and the first Betti numbers.
• TauCeti.DualGraph.arithmeticGenus_selfClutch and TauCeti.DualGraph.firstBetti_selfClutch: self-clutching raises the arithmetic genus and the first Betti number by one.
• TauCeti.DualGraph.logCanonicalDegree_clutch_inl, TauCeti.DualGraph.logCanonicalDegree_clutch_inr and TauCeti.DualGraph.logCanonicalDegree_selfClutch: clutching preserves every log-canonical degree, since each glued marking is replaced by a branch of the new node.
• TauCeti.DualGraph.isStable_clutch_iff and TauCeti.DualGraph.isStable_selfClutch_iff, with their semistable counterparts: a clutched graph is stable exactly when its inputs are.

Implementation notes

The glued markings are singled out by the shape of the marking type, Option ι for external clutching and ι ⊕ Fin 2 for self-clutching, so that the new edge none is determined by them. Both constructions are abbreviations, so that their vertex and edge types reduce to G₁.Vertex ⊕ G₂.Vertex and Option (G₁.Edge ⊕ G₂.Edge), respectively G.Vertex and Option G.Edge, and vertices of an externally clutched graph can be written as Sum.inl v and Sum.inr v.

References

• F. F. Knudsen, The projectivity of the moduli space of stable curves, II: The stacks M_{g,n}, Math. Scand. 52 (1983), 161–199, §3, for the clutching morphisms.

External clutching

@[reducible, inline]

abbrev TauCeti.DualGraph.clutch {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) : DualGraph (ι ⊕ κ)

External clutching: the dual graph obtained by gluing a curve with dual graph G₁ to a curve with dual graph G₂ along their markings none. It is the disjoint union of G₁ and G₂ with a new edge, the edge none, joining the components carrying those two markings.

@[simp]

theorem TauCeti.DualGraph.endpoint_clutch_none {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) : (G₁.clutch G₂).endpoint none = ![Sum.inl (G₁.marking none), Sum.inr (G₂.marking none)]

@[simp]

theorem TauCeti.DualGraph.endpoint_clutch_some_inl {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) (e : G₁.Edge) (i : Fin 2) : (G₁.clutch G₂).endpoint (some (Sum.inl e)) i = Sum.inl (G₁.endpoint e i)

@[simp]

theorem TauCeti.DualGraph.endpoint_clutch_some_inr {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) (e : G₂.Edge) (i : Fin 2) : (G₁.clutch G₂).endpoint (some (Sum.inr e)) i = Sum.inr (G₂.endpoint e i)

@[simp]

theorem TauCeti.DualGraph.genus_clutch_inl {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) (v : G₁.Vertex) : (G₁.clutch G₂).genus (Sum.inl v) = G₁.genus v

@[simp]

theorem TauCeti.DualGraph.genus_clutch_inr {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) (v : G₂.Vertex) : (G₁.clutch G₂).genus (Sum.inr v) = G₂.genus v

@[simp]

theorem TauCeti.DualGraph.marking_clutch_inl {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) (i : ι) : (G₁.clutch G₂).marking (Sum.inl i) = Sum.inl (G₁.marking (some i))

@[simp]

theorem TauCeti.DualGraph.marking_clutch_inr {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) (j : κ) : (G₁.clutch G₂).marking (Sum.inr j) = Sum.inr (G₂.marking (some j))

theorem TauCeti.DualGraph.card_vertex_clutch {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) : Fintype.card (G₁.clutch G₂).Vertex = Fintype.card G₁.Vertex + Fintype.card G₂.Vertex

theorem TauCeti.DualGraph.card_edge_clutch {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) : Fintype.card (G₁.clutch G₂).Edge = Fintype.card G₁.Edge + Fintype.card G₂.Edge + 1

External clutching adds exactly one edge, the new node.

@[simp]

theorem TauCeti.DualGraph.firstBetti_clutch {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) : (G₁.clutch G₂).firstBetti = G₁.firstBetti + G₂.firstBetti

External clutching adds the first Betti numbers: the new edge joins two components that were not connected before, so it creates no cycle.

@[simp]

theorem TauCeti.DualGraph.arithmeticGenus_clutch {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) : (G₁.clutch G₂).arithmeticGenus = G₁.arithmeticGenus + G₂.arithmeticGenus

External clutching adds the arithmetic genera.

theorem TauCeti.DualGraph.valence_clutch_inl {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) (v : G₁.Vertex) : (G₁.clutch G₂).valence (Sum.inl v) = G₁.valence v + if G₁.marking none = v then 1 else 0

A component of G₁ gains one branch of the new node exactly when it carries the glued marking.

theorem TauCeti.DualGraph.valence_clutch_inr {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) (v : G₂.Vertex) : (G₁.clutch G₂).valence (Sum.inr v) = G₂.valence v + if G₂.marking none = v then 1 else 0

A component of G₂ gains one branch of the new node exactly when it carries the glued marking.

theorem TauCeti.DualGraph.numMarkings_clutch_inl {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) [Fintype ι] [Fintype κ] (v : G₁.Vertex) : ((G₁.clutch G₂).numMarkings (Sum.inl v) + if G₁.marking none = v then 1 else 0) = G₁.numMarkings v

A component of G₁ loses the glued marking exactly when it carries it.

theorem TauCeti.DualGraph.numMarkings_clutch_inr {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) [Fintype ι] [Fintype κ] (v : G₂.Vertex) : ((G₁.clutch G₂).numMarkings (Sum.inr v) + if G₂.marking none = v then 1 else 0) = G₂.numMarkings v

A component of G₂ loses the glued marking exactly when it carries it.

@[simp]

theorem TauCeti.DualGraph.logCanonicalDegree_clutch_inl {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) [Fintype ι] [Fintype κ] (v : G₁.Vertex) : (G₁.clutch G₂).logCanonicalDegree (Sum.inl v) = G₁.logCanonicalDegree v

External clutching preserves the log-canonical degree of every component of G₁: the glued marking becomes a branch of the new node.

@[simp]

theorem TauCeti.DualGraph.logCanonicalDegree_clutch_inr {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) [Fintype ι] [Fintype κ] (v : G₂.Vertex) : (G₁.clutch G₂).logCanonicalDegree (Sum.inr v) = G₂.logCanonicalDegree v

External clutching preserves the log-canonical degree of every component of G₂: the glued marking becomes a branch of the new node.

@[simp]

theorem TauCeti.DualGraph.isStable_clutch_iff {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) [Fintype ι] [Fintype κ] : (G₁.clutch G₂).IsStable ↔ G₁.IsStable ∧ G₂.IsStable

An externally clutched graph is stable exactly when both of its inputs are.

@[simp]

theorem TauCeti.DualGraph.isSemistable_clutch_iff {ι : Type v} {κ : Type w} (G₁ : DualGraph (Option ι)) (G₂ : DualGraph (Option κ)) [Fintype ι] [Fintype κ] : (G₁.clutch G₂).IsSemistable ↔ G₁.IsSemistable ∧ G₂.IsSemistable

An externally clutched graph is semistable exactly when both of its inputs are.

Self-clutching

@[reducible, inline]

abbrev TauCeti.DualGraph.selfClutch {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) : DualGraph ι

Self-clutching: the dual graph obtained from a curve with dual graph G by gluing its markings Sum.inr 0 and Sum.inr 1. It is G with a new edge, the edge none, joining the components carrying those two markings; the edge is a loop when they lie on one component.

@[simp]

theorem TauCeti.DualGraph.endpoint_selfClutch_none {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) (i : Fin 2) : G.selfClutch.endpoint none i = G.marking (Sum.inr i)

@[simp]

theorem TauCeti.DualGraph.endpoint_selfClutch_some {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) (e : G.Edge) (i : Fin 2) : G.selfClutch.endpoint (some e) i = G.endpoint e i

@[simp]

theorem TauCeti.DualGraph.genus_selfClutch {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) (v : G.Vertex) : G.selfClutch.genus v = G.genus v

@[simp]

theorem TauCeti.DualGraph.marking_selfClutch {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) (i : ι) : G.selfClutch.marking i = G.marking (Sum.inl i)

theorem TauCeti.DualGraph.card_vertex_selfClutch {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) : Fintype.card G.selfClutch.Vertex = Fintype.card G.Vertex

theorem TauCeti.DualGraph.card_edge_selfClutch {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) : Fintype.card G.selfClutch.Edge = Fintype.card G.Edge + 1

Self-clutching adds exactly one edge, the new node.

@[simp]

theorem TauCeti.DualGraph.firstBetti_selfClutch {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) : G.selfClutch.firstBetti = G.firstBetti + 1

Self-clutching raises the first Betti number by one: the new edge closes a cycle.

@[simp]

theorem TauCeti.DualGraph.arithmeticGenus_selfClutch {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) : G.selfClutch.arithmeticGenus = G.arithmeticGenus + 1

Self-clutching raises the arithmetic genus by one.

theorem TauCeti.DualGraph.valence_selfClutch {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) (v : G.Vertex) : G.selfClutch.valence v = G.valence v + {i : Fin 2 | G.marking (Sum.inr i) = v}.card

A component gains one branch of the new node for each glued marking it carries.

theorem TauCeti.DualGraph.numMarkings_selfClutch {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) [Fintype ι] (v : G.Vertex) : G.selfClutch.numMarkings v + {i : Fin 2 | G.marking (Sum.inr i) = v}.card = G.numMarkings v

A component loses each glued marking it carries.

@[simp]

theorem TauCeti.DualGraph.logCanonicalDegree_selfClutch {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) [Fintype ι] (v : G.Vertex) : G.selfClutch.logCanonicalDegree v = G.logCanonicalDegree v

Self-clutching preserves every log-canonical degree: the two glued markings become the two branches of the new node.

@[simp]

theorem TauCeti.DualGraph.isStable_selfClutch_iff {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) [Fintype ι] : G.selfClutch.IsStable ↔ G.IsStable

A self-clutched graph is stable exactly when its input is.

@[simp]

theorem TauCeti.DualGraph.isSemistable_selfClutch_iff {ι : Type v} (G : DualGraph (ι ⊕ Fin 2)) [Fintype ι] : G.selfClutch.IsSemistable ↔ G.IsSemistable

A self-clutched graph is semistable exactly when its input is.