Documentation

LeanPool.BrillNoetherGraphs.Utilities.Gluing.CanonicalWedge

Canonical divisors on a vertex wedge #

If two graphs are identified at marked vertices x and y, the canonical divisor of the wedge is

K_(G ∨ H) = K_G + K_H + 2(x = y).

The extra two chips are the valence correction at the identified vertex. In particular the sum of the two factor canonical divisors is canonically dual to the doubled glue point. Riemann--Roch then gives a useful uniform estimate: on a connected wedge of total genus four, K_G + K_H has rank at least one.

This file is deliberately independent of genus two and of two-pole joins. It is the reusable one-pole calculation underlying the genus-two/genus-two seed.

source
theorem Utilities.vertex_degree_vertexWedge_inl (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (a : G.V) :
vertexDegree (vertexWedge G H x y) (Sum.inl a) = vertexDegree G a + if a = x then vertexDegree H y else 0

The degree of a left vertex in a wedge is its left-factor degree, with the right marked degree added at the common vertex.

source
theorem Utilities.vertex_degree_vertexWedge_inr (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (b : { b : H.V // b ≠ y }) :
vertexDegree (vertexWedge G H x y) (Sum.inr b) = vertexDegree H ↑b

A strictly-right vertex keeps its right-factor degree in a wedge.

source
def Utilities.wedgeCanonicalSum (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) :
CFDiv (vertexWedge G H x y)

The sum of the two factor canonical divisors on their vertex wedge.

Equations
Instances For
    source
    def Utilities.wedgeGlueDouble (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) :
    CFDiv (vertexWedge G H x y)

    The doubled common vertex of a wedge.

    Equations
    Instances For
      source
      theorem Utilities.canonical_divisor_vertexWedge (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) :
      canonicalDivisor (vertexWedge G H x y) = wedgeCanonicalSum G H x y + wedgeGlueDouble G H x y

      Canonical wedge formula. Identifying two vertices contributes two additional canonical chips at the common vertex.

      source
      theorem Utilities.canonical_sub_wedgeCanonicalSum (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) :
      canonicalDivisor (vertexWedge G H x y) - wedgeCanonicalSum G H x y = wedgeGlueDouble G H x y

      The doubled glue point is literally the canonical complement of the factor-canonical sum.

      source
      @[simp]
      theorem Utilities.deg_wedgeCanonicalSum (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) :
      CFDiv.degree (wedgeCanonicalSum G H x y) = 2 * G.genus + 2 * H.genus - 4
      source
      @[simp]
      theorem Utilities.deg_wedgeGlueDouble (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) :
      CFDiv.degree (wedgeGlueDouble G H x y) = 2
      source
      theorem Utilities.rank_wedgeCanonicalSum_sub_rank_wedgeGlueDouble (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (hG : graphConnected G) (hH : graphConnected H) :
      rank (vertexWedge G H x y) (wedgeCanonicalSum G H x y) - rank (vertexWedge G H x y) (wedgeGlueDouble G H x y) = G.genus + H.genus - 3

      Riemann--Roch compares the factor-canonical sum with the doubled glue point on a connected wedge.

      source
      theorem Utilities.rank_wedgeCanonicalSum_ge_one_of_genus_sum_four (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (hG : graphConnected G) (hH : graphConnected H) (hGenus : G.genus + H.genus = 4) :
      rank (vertexWedge G H x y) (wedgeCanonicalSum G H x y) ≥ 1

      On a connected wedge of total genus four, the sum of the two factor canonical divisors has rank at least one.