Smoothing nodes of dual graphs

Smoothing a node of a nodal curve replaces the local equation xy = 0 by xy = t with t ≠ 0. The two branches of the node then become one annulus, so the components carrying them merge into one component. Smoothing a set S of nodes therefore glues together the components joined by the nodes in S; the remaining nodes stay nodes, and the markings stay on the component they lay on.

This file describes the effect on dual graphs. For a finite set S of edges of a dual graph G:

• TauCeti.DualGraph.SmoothingRel G S relates the two endpoints of every edge in S, and TauCeti.DualGraph.smoothingVertex G S sends a vertex of G to its class in the quotient by the equivalence relation it generates.
• TauCeti.DualGraph.smoothingComponent G S x is the part of G that is smoothed into the class x: the vertices in x, the edges of S joining them and the markings on them. It is connected, so it is a dual graph.
• TauCeti.DualGraph.smoothing G S is the dual graph of the smoothed curve. Its vertices are the classes, its edges are the edges of G outside S, and the genus of the class x is the arithmetic genus of smoothingComponent G S x: a smoothed component is a smoothing of that subcurve, and smoothing preserves arithmetic genus.

Main results

• TauCeti.DualGraph.genus_smoothing_add_card: the genus of a smoothed component is ∑ g(v) + #(S-edges in x) + 1 - #(vertices in x), summing over the vertices v in x.
• TauCeti.DualGraph.arithmeticGenus_smoothing: smoothing preserves the arithmetic genus ∑ g(v) + b₁ of the graph.
• TauCeti.DualGraph.genus_smoothing_singleton_of_ne and TauCeti.DualGraph.genus_smoothing_singleton_of_eq: smoothing one node joining two different components gives a component whose genus is the sum of theirs, and smoothing a self-node raises the genus of its component by one.
• TauCeti.DualGraph.genus_smoothing_of_forall_endpoint_ne: components meeting no node of S are untouched.
• TauCeti.DualGraph.genus_smoothing_univ: smoothing every node gives a smooth curve whose genus is the arithmetic genus of G.
• TauCeti.DualGraph.logCanonicalDegree_smoothing: the log-canonical degree of a smoothed component is the sum of the log-canonical degrees of the components it is made of. Hence smoothing preserves stability and semistability (TauCeti.DualGraph.IsStable.smoothing, TauCeti.DualGraph.IsSemistable.smoothing).

A different way to remove a node is to cut it open into two markings, which undoes clutching; its effect on the invariants is computed in TauCeti.AlgebraicGeometry.Curves.DualGraph.Clutching.

Implementation notes

The quotient is Quot (SmoothingRel G S). It is finite because G.Vertex is, and it is given the classical decidable equality. The edges of the smoothing are the subtype {e // e ∉ S}.

References

• E. Arbarello, M. Cornalba and P. A. Griffiths, Geometry of Algebraic Curves, Volume II, Chapter X, for nodal curves and their dual graphs.
• J. W. Robbin and D. A. Salamon, A construction of the Deligne–Mumford orbifold, J. Eur. Math. Soc. 8 (2006), 611–699, for nodal Riemann surfaces and the smoothing xy = t of their nodes.

The components of a smoothing

def TauCeti.DualGraph.SmoothingRel {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) (v w : G.Vertex) : Prop

The relation joining the two endpoints of each edge in S. When the nodes in S are smoothed, the components related by its equivalence closure merge into one component.

def TauCeti.DualGraph.smoothingVertex {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) (v : G.Vertex) : Quot (G.SmoothingRel S)

The component of the curve smoothed along S that contains the component v of G: the class of v for the equivalence relation generated by SmoothingRel G S.

@[instance_reducible]

noncomputable instance TauCeti.DualGraph.instFintypeQuotVertexSmoothingRel {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) : Fintype (Quot (G.SmoothingRel S))

@[instance_reducible]

noncomputable instance TauCeti.DualGraph.instDecidableEqQuotVertexSmoothingRel {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) : DecidableEq (Quot (G.SmoothingRel S))

theorem TauCeti.DualGraph.smoothingRel_iff {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) {v w : G.Vertex} : G.SmoothingRel S v w ↔ ∃ e ∈ S, G.endpoint e 0 = v ∧ G.endpoint e 1 = w

theorem TauCeti.DualGraph.smoothingVertex_surjective {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) : Function.Surjective (G.smoothingVertex S)

theorem TauCeti.DualGraph.smoothingVertex_eq_smoothingVertex_iff {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) {v w : G.Vertex} : G.smoothingVertex S v = G.smoothingVertex S w ↔ Relation.EqvGen (G.SmoothingRel S) v w

Two components of G end up on the same component of the smoothing exactly when they are related by the equivalence relation generated by the nodes in S.

theorem TauCeti.DualGraph.smoothingVertex_endpoint {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) {e : G.Edge} (he : e ∈ S) (i j : Fin 2) : G.smoothingVertex S (G.endpoint e i) = G.smoothingVertex S (G.endpoint e j)

The two branches of a smoothed node lie on the same component of the smoothing.

def TauCeti.DualGraph.smoothingVertexLift {ι : Type v} {G : DualGraph ι} {S : Finset G.Edge} {α : Sort u_1} (f : G.Vertex → α) (hf : ∀ e ∈ S, f (G.endpoint e 0) = f (G.endpoint e 1)) : Quot (G.SmoothingRel S) → α

A function on the components of G that agrees on the two branches of every node in S descends to the components of the curve smoothed along S.

@[simp]

theorem TauCeti.DualGraph.smoothingVertexLift_smoothingVertex {ι : Type v} {G : DualGraph ι} {S : Finset G.Edge} {α : Sort u_1} (f : G.Vertex → α) (hf : ∀ e ∈ S, f (G.endpoint e 0) = f (G.endpoint e 1)) (v : G.Vertex) : smoothingVertexLift f hf (G.smoothingVertex S v) = f v

theorem TauCeti.DualGraph.apply_eq_apply_of_smoothingVertex_eq {ι : Type v} {G : DualGraph ι} {S : Finset G.Edge} {α : Sort u_1} (f : G.Vertex → α) (hf : ∀ e ∈ S, f (G.endpoint e 0) = f (G.endpoint e 1)) {v w : G.Vertex} (h : G.smoothingVertex S v = G.smoothingVertex S w) : f v = f w

A function on the components of G that agrees on the two branches of every node in S takes the same value on components of G lying on the same component of the smoothing.

theorem TauCeti.DualGraph.smoothingVertex_induction_on {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) {p : Quot (G.SmoothingRel S) → Prop} (x : Quot (G.SmoothingRel S)) (h : ∀ (v : G.Vertex), p (G.smoothingVertex S v)) : p x

To prove a property of every component of the smoothing, it suffices to prove it for the component containing each component of G.

@[reducible, inline]

noncomputable abbrev TauCeti.DualGraph.smoothingComponent {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) (x : Quot (G.SmoothingRel S)) : DualGraph { i : ι // G.smoothingVertex S (G.marking i) = x }

The part of G that is smoothed into the component x: the components of G in the class x, the nodes of S joining them and the markings on them. It is connected, since x is a class of the equivalence relation generated by these nodes.

@[simp]

theorem TauCeti.DualGraph.endpoint_smoothingComponent {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) (x : Quot (G.SmoothingRel S)) (e : (G.smoothingComponent S x).Edge) (i : Fin 2) : (G.smoothingComponent S x).endpoint e i = ⟨G.endpoint (↑e) i, ⋯⟩

@[simp]

theorem TauCeti.DualGraph.genus_smoothingComponent {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) (x : Quot (G.SmoothingRel S)) (v : (G.smoothingComponent S x).Vertex) : (G.smoothingComponent S x).genus v = G.genus ↑v

@[simp]

theorem TauCeti.DualGraph.marking_smoothingComponent {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) (x : Quot (G.SmoothingRel S)) (i : { i : ι // G.smoothingVertex S (G.marking i) = x }) : (G.smoothingComponent S x).marking i = ⟨G.marking ↑i, ⋯⟩

The smoothed graph

@[reducible, inline]

noncomputable abbrev TauCeti.DualGraph.smoothing {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) : DualGraph ι

The dual graph of the curve obtained from a curve with dual graph G by smoothing the nodes in S. Its vertices are the classes of the vertices of G under the equivalence relation generated by the edges in S, its edges are the edges of G outside S, and the genus of a class x is the arithmetic genus of the part smoothingComponent G S x smoothed into it.

@[simp]

theorem TauCeti.DualGraph.endpoint_smoothing {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) (e : (G.smoothing S).Edge) (i : Fin 2) : (G.smoothing S).endpoint e i = G.smoothingVertex S (G.endpoint (↑e) i)

theorem TauCeti.DualGraph.genus_smoothing {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) (x : (G.smoothing S).Vertex) : (G.smoothing S).genus x = (G.smoothingComponent S x).arithmeticGenus

@[simp]

theorem TauCeti.DualGraph.marking_smoothing {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) (i : ι) : (G.smoothing S).marking i = G.smoothingVertex S (G.marking i)

theorem TauCeti.DualGraph.card_edge_smoothing {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) : Fintype.card (G.smoothing S).Edge + S.card = Fintype.card G.Edge

Smoothing removes exactly the smoothed nodes.

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

The number of smoothed components is at most one more than the number of remaining nodes.

theorem TauCeti.DualGraph.genus_smoothing_add_card {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) (x : (G.smoothing S).Vertex) : (G.smoothing S).genus x + {v : G.Vertex | G.smoothingVertex S v = x}.card = ∑ v : G.Vertex with G.smoothingVertex S v = x, G.genus v + {e ∈ S | G.smoothingVertex S (G.endpoint e 0) = x}.card + 1

Genus of a smoothed component. The genus of the component x of the smoothing, plus the number of components of G in x, is the sum of their genera plus the number of nodes of S in x plus one. That is, it is ∑ g(v) + b₁ of the part of G smoothed into x.

@[simp]

theorem TauCeti.DualGraph.arithmeticGenus_smoothing {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) : (G.smoothing S).arithmeticGenus = G.arithmeticGenus

Smoothing preserves the arithmetic genus. The first Betti number lost by smoothing the nodes in S reappears in the genera of the smoothed components.

theorem TauCeti.DualGraph.valence_smoothing_add {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) (x : (G.smoothing S).Vertex) : (G.smoothing S).valence x + 2 * {e ∈ S | G.smoothingVertex S (G.endpoint e 0) = x}.card = ∑ v : G.Vertex with G.smoothingVertex S v = x, G.valence v

The valence of a smoothed component is the total valence of the components of G in it, minus the two branches of each smoothed node joining them.

theorem TauCeti.DualGraph.numMarkings_smoothing {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) [Fintype ι] (x : (G.smoothing S).Vertex) : (G.smoothing S).numMarkings x = ∑ v : G.Vertex with G.smoothingVertex S v = x, G.numMarkings v

The markings on a smoothed component are those on the components of G in it.

theorem TauCeti.DualGraph.logCanonicalDegree_smoothing {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) [Fintype ι] (x : (G.smoothing S).Vertex) : (G.smoothing S).logCanonicalDegree x = ∑ v : G.Vertex with G.smoothingVertex S v = x, G.logCanonicalDegree v

The log-canonical degree of a smoothed component is the sum of the log-canonical degrees of the components of G in it.

theorem TauCeti.DualGraph.IsStable.smoothing {ι : Type v} {G : DualGraph ι} (S : Finset G.Edge) [Fintype ι] (hG : G.IsStable) : (G.smoothing S).IsStable

Smoothing nodes of a stable graph gives a stable graph.

theorem TauCeti.DualGraph.IsSemistable.smoothing {ι : Type v} {G : DualGraph ι} (S : Finset G.Edge) [Fintype ι] (hG : G.IsSemistable) : (G.smoothing S).IsSemistable

Smoothing nodes of a semistable graph gives a semistable graph.

Components away from the smoothed nodes

theorem TauCeti.DualGraph.smoothingVertex_eq_iff_of_forall_endpoint_ne {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) {v w : G.Vertex} (hv : ∀ e ∈ S, ∀ (i : Fin 2), G.endpoint e i ≠ v) : G.smoothingVertex S w = G.smoothingVertex S v ↔ w = v

A component of G carrying no branch of a node of S is alone in its class.

theorem TauCeti.DualGraph.genus_smoothing_of_forall_endpoint_ne {ι : Type v} (G : DualGraph ι) (S : Finset G.Edge) {v : G.Vertex} (hv : ∀ e ∈ S, ∀ (i : Fin 2), G.endpoint e i ≠ v) : (G.smoothing S).genus (G.smoothingVertex S v) = G.genus v

Smoothing does not change the genus of a component carrying no branch of a smoothed node.

Smoothing one node

theorem TauCeti.DualGraph.smoothingVertex_singleton_eq_iff {ι : Type v} {G : DualGraph ι} {e : G.Edge} {w : G.Vertex} : G.smoothingVertex {e} w = G.smoothingVertex {e} (G.endpoint e 0) ↔ w = G.endpoint e 0 ∨ w = G.endpoint e 1

Smoothing the single node e merges exactly the components carrying its two branches.

theorem TauCeti.DualGraph.genus_smoothing_singleton_of_ne {ι : Type v} {G : DualGraph ι} {e : G.Edge} (he : G.endpoint e 0 ≠ G.endpoint e 1) : (G.smoothing {e}).genus (G.smoothingVertex {e} (G.endpoint e 0)) = G.genus (G.endpoint e 0) + G.genus (G.endpoint e 1)

Smoothing a node joining two different components merges them into one component whose genus is the sum of their genera.

theorem TauCeti.DualGraph.genus_smoothing_singleton_of_eq {ι : Type v} {G : DualGraph ι} {e : G.Edge} (he : G.endpoint e 0 = G.endpoint e 1) : (G.smoothing {e}).genus (G.smoothingVertex {e} (G.endpoint e 0)) = G.genus (G.endpoint e 0) + 1

Smoothing a self-node raises the genus of its component by one.

Smoothing every node

theorem TauCeti.DualGraph.smoothingVertex_univ_eq {ι : Type v} (G : DualGraph ι) (v w : G.Vertex) : G.smoothingVertex Finset.univ v = G.smoothingVertex Finset.univ w

Smoothing every node leaves a single component, since the graph is connected.

theorem TauCeti.DualGraph.card_vertex_smoothing_univ {ι : Type v} (G : DualGraph ι) : Fintype.card (G.smoothing Finset.univ).Vertex = 1

Smoothing every node gives a graph with a single vertex.

theorem TauCeti.DualGraph.genus_smoothing_univ {ι : Type v} (G : DualGraph ι) (x : (G.smoothing Finset.univ).Vertex) : (G.smoothing Finset.univ).genus x = G.arithmeticGenus

Smoothing every node gives a smooth curve whose genus is the arithmetic genus of G.