Lax Lean Archive

Bipartite graphs and bipartite complements

Lax185574.BipartiteGraphs · concepts/Lax185574/BipartiteGraphs.lean · lax-185574

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A bipartite graph B = (X, Y, E) has parts X and Y and an edge set E of pairs xy with x ∈ X and y ∈ Y. Its bipartite complement, denoted B̄, is the bipartite graph with parts X, Y and edge set XY ∖ E.

    For a graph G and disjoint vertex sets X, Y ⊆ V(G), G[X, Y] is the bipartite graph with parts X and Y whose edges connect pairs of vertices that are adjacent in G. Furthermore, G[X, X] denotes the bipartite graph whose parts are two copies of X, and whose edges connect two vertices in opposite parts if the corresponding vertices of G are either adjacent or equal. The edges of G[X, X] connecting the two copies of a vertex are its diagonal edges. Finally, Ḡ[X, X] is the bipartite complement of G[X, X], extended with the diagonal edges.

    Concept map
    1 concept; 7 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 32 of this submission's paper
    • page 33 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Basic
    2
    3/-!
    4---
    5title: Bipartite graphs and bipartite complements
    6type: definition
    7---
    8A *bipartite graph* B = (X, Y, E) has parts X and Y and an edge set E
    9of pairs xy with x ∈ X and y ∈ Y. Its *bipartite complement*, denoted
    10B̄, is the bipartite graph with parts X, Y and edge set XY ∖ E.
    11
    12For a graph G and disjoint vertex sets X, Y ⊆ V(G), G[X, Y] is the
    13bipartite graph with parts X and Y whose edges connect pairs of vertices
    14that are adjacent in G. Furthermore, G[X, X] denotes the bipartite
    15graph whose parts are two copies of X, and whose edges connect two
    16vertices in opposite parts if the corresponding vertices of G are
    17either adjacent or equal. The edges of G[X, X] connecting the two copies
    18of a vertex are its *diagonal edges*. Finally, Ḡ[X, X] is the bipartite
    19complement of G[X, X], extended with the diagonal edges.
    20
    21# Formalization notes
    22
    23A bipartite graph with parts α and β is given by a relation
    24E : α → β → Prop, and `bipartiteGraph E` is the simple graph on α ⊕ β
    25that it defines. The bipartite complement is `bipartiteGraph` of the
    26negated relation.
    27
    28The graphs G[X, Y] and Ḡ[X, Y] are built uniformly on two copies of the
    29vertex set, V ⊕ V, as `pairGraph` and `coPairGraph`. The left copy of
    30X is one part and the right copy of Y is the other. A left vertex u ∈ X
    31and a right vertex v ∈ Y are adjacent if u = v or u and v are adjacent
    32in G, respectively non-adjacent in G. For X = Y this is G[X, X], with
    33its diagonal edges, and Ḡ[X, X]. For disjoint X and Y the case u = v
    34never occurs, so this is G[X, Y], and Ḡ[X, Y] is its bipartite
    35complement, the bipartite graph of the non-adjacent pairs. The other
    36vertices of V ⊕ V are isolated. So the distance from the left copy of u
    37to the right copy of v in `pairGraph G X Y` is the distance between u
    38and v in G[X, Y], and likewise for Ḡ[X, Y].
    39-/
    40
    41namespace Lax185574.BipartiteGraphs
    42
    43universe u w z
    44
    45/-- The bipartite graph on `α ⊕ β` with an edge between `inl a` and
    46`inr b` exactly when `E a b`. -/
    47def bipartiteGraph {α : Type u} {β : Type w} (E : α → β → Prop) : SimpleGraph (α ⊕ β) :=
    48 SimpleGraph.fromRel fun s t => ∃ a b, s = .inl a ∧ t = .inr b ∧ E a b
    49
    50variable {V : Type z}
    51
    52/-- `G[X, Y]`, on two copies of `V`: the left copy of `u ∈ X` and the
    53right copy of `v ∈ Y` are adjacent if `u = v` or `u` and `v` are
    54adjacent in `G`. -/
    55def pairGraph (G : SimpleGraph V) (X Y : Set V) : SimpleGraph (V ⊕ V) :=
    56 bipartiteGraph fun u v => u ∈ X ∧ v ∈ Y ∧ (u = v ∨ G.Adj u v)
    57
    58/-- `Ḡ[X, Y]`, on two copies of `V`: the left copy of `u ∈ X` and the
    59right copy of `v ∈ Y` are adjacent if `u = v` or `u` and `v` are
    60non-adjacent in `G`. -/
    61def coPairGraph (G : SimpleGraph V) (X Y : Set V) : SimpleGraph (V ⊕ V) :=
    62 bipartiteGraph fun u v => u ∈ X ∧ v ∈ Y ∧ (u = v ∨ ¬ G.Adj u v)
    63
    64end Lax185574.BipartiteGraphs
    65
    Formalization notes

    A bipartite graph with parts α and β is given by a relation E : α → β → Prop, and bipartiteGraphEbipartiteGraph E is the simple graph on α ⊕ β that it defines. The bipartite complement is bipartiteGraphbipartiteGraph of the negated relation.

    The graphs G[X, Y] and Ḡ[X, Y] are built uniformly on two copies of the vertex set, V ⊕ V, as pairGraphpairGraph and coPairGraphcoPairGraph. The left copy of X is one part and the right copy of Y is the other. A left vertex u ∈ X and a right vertex v ∈ Y are adjacent if u = v or u and v are adjacent in G, respectively non-adjacent in G. For X = Y this is G[X, X], with its diagonal edges, and Ḡ[X, X]. For disjoint X and Y the case u = v never occurs, so this is G[X, Y], and Ḡ[X, Y] is its bipartite complement, the bipartite graph of the non-adjacent pairs. The other vertices of V ⊕ V are isolated. So the distance from the left copy of u to the right copy of v in pairGraphGXYpairGraph G X Y is the distance between u and v in G[X, Y], and likewise for Ḡ[X, Y].

    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…