Documentation

LeanPool.BrillNoetherGraphs.Utilities.Gluing.BridgeGraph

Joining two graphs by a bridge #

This module forms the disjoint union of two chip-firing graphs on a sum vertex type and adds one edge between specified vertices in the two factors. The construction is useful for reducing divisor questions across separating edges.

source
@[reducible, inline]
abbrev Utilities.bridgeGraph (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) :
CFGraph

The graph obtained from G and H by joining x to y with one edge. The factor vertex types are kept as the two summands of the new vertex type.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Utilities.bridgeGraph_edges (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) :
    (bridgeGraph G H x y).edges = (Sum.inl x, Sum.inr y) ::ₘ (Multiset.map (fun (e : G.V × G.V) => (Sum.inl e.1, Sum.inl e.2)) G.edges + Multiset.map (fun (e : H.V × H.V) => (Sum.inr e.1, Sum.inr e.2)) H.edges)
    source
    theorem Utilities.bridgeGraph_edge_card (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) :
    (bridgeGraph G H x y).edges.card = G.edges.card + H.edges.card + 1

    Joining two factors by one bridge adds their edge counts and one.

    source
    theorem Utilities.bridgeGraph_vertex_card (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) :
    Fintype.card (bridgeGraph G H x y).V = Fintype.card G.V + Fintype.card H.V

    The sum vertex type has the sum of the two factor vertex counts.

    source
    @[simp]
    theorem Utilities.genus_bridgeGraph (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) :
    (bridgeGraph G H x y).genus = G.genus + H.genus

    A bridge joining two components creates no new cycle.

    source
    @[simp]
    theorem Utilities.num_edges_bridgeGraph_inl (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (a b : G.V) :
    numEdges (bridgeGraph G H x y) (Sum.inl a) (Sum.inl b) = numEdges G a b

    Edge multiplicities within the left factor are unchanged.

    source
    @[simp]
    theorem Utilities.num_edges_bridgeGraph_inr (G : CFGraph) (H : CFGraph) (x : G.V) (y a b : H.V) :
    numEdges (bridgeGraph G H x y) (Sum.inr a) (Sum.inr b) = numEdges H a b

    Edge multiplicities within the right factor are unchanged.

    source
    @[simp]
    theorem Utilities.num_edges_bridgeGraph_inl_inr (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (a : G.V) (b : H.V) :
    numEdges (bridgeGraph G H x y) (Sum.inl a) (Sum.inr b) = if a = x ∧ b = y then 1 else 0

    The bridge is the only edge between the two factors.

    source
    theorem Utilities.num_edges_bridgeGraph_endpoints (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) :
    numEdges (bridgeGraph G H x y) (Sum.inl x) (Sum.inr y) = 1

    The distinguished endpoints are joined by exactly one cross edge.

    source
    theorem Utilities.graph_connected_bridgeGraph (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (hG : graphConnected G) (hH : graphConnected H) :
    graphConnected (bridgeGraph G H x y)

    Joining two connected graphs by a bridge produces a connected graph.