Bipartitions of multigraphs

A bipartition of a multigraph G : Graph α β is a pair of disjoint finite sets L and R of actual vertices, together covering V(G), such that every edge joins a vertex of L to a vertex of R. Parallel edges are allowed, isolated vertices may lie on either side, and either side may be empty; loops are excluded, since the two ends of a loop coincide.

The sides are finite sets of actual vertices, so that sums of vertex capacities over a side, or over a part of it, are finite sums; in particular a multigraph with a bipartition has finitely many actual vertices. Since every actual edge has exactly one end in each side, summing over one side the values of the edges incident with each vertex counts every actual edge exactly once, so the total usage of either side by edge multiplicities equals their sum.

Main definitions

• Graph.IsBipartition G L R: the finite sets L and R of actual vertices form a bipartition of G.
• Graph.BipartiteHom G L: one arrow for every actual edge, directed from L to its other end.

Main results

• Graph.isBipartition_comm: a bipartition is symmetric in its two sides.
• Graph.IsBipartition.loopless: a multigraph with a bipartition has no loops.
• Graph.IsBipartition.finite: a multigraph with a bipartition has finitely many actual vertices.
• Graph.IsBipartition.deleteEdges: deleting edges preserves a displayed bipartition.
• SimpleGraph.isBipartition_ofSimpleGraph_iff: covering bipartitions of Graph.ofSimpleGraph H are precisely bipartitions of H whose two sides cover every vertex.
• Graph.IsBipartition.isVertexCover_left: the side L of a bipartition is a vertex cover, and similarly for R.
• Graph.IsBipartition.sum_sum_incidentEdges_left: summing over L the values of the edges incident with each vertex sums every actual edge once, and similarly for R.

structure Graph.IsBipartition {α : Type u} {β : Type v} (G : Graph α β) (L R : Finset ↑G.vertexSet) : Prop

The finite sets L and R of actual vertices form a bipartition of the multigraph G: they are disjoint, every actual vertex lies in one of them, and every edge joins a vertex of L to a vertex of R.

• disjoint : Disjoint L R
• mem_or_mem (x : ↑G.vertexSet) : x ∈ L ∨ x ∈ R
• isLink {e : β} {x y : ↑G.vertexSet} : G.IsLink e ↑x ↑y → x ∈ L ∧ y ∈ R ∨ x ∈ R ∧ y ∈ L

theorem Graph.IsBipartition.symm {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} (h : G.IsBipartition L R) : G.IsBipartition R L

Exchanging the two sides of a bipartition gives a bipartition.

theorem Graph.IsBipartition.notMem_left_iff {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} (h : G.IsBipartition L R) {x : ↑G.vertexSet} : x ∉ L ↔ x ∈ R

An actual vertex outside L lies in R.

theorem Graph.IsBipartition.notMem_right_iff {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} (h : G.IsBipartition L R) {x : ↑G.vertexSet} : x ∉ R ↔ x ∈ L

An actual vertex outside R lies in L.

theorem Graph.IsBipartition.mem_right_of_isLink {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} (h : G.IsBipartition L R) {e : β} {x y : ↑G.vertexSet} (he : G.IsLink e ↑x ↑y) (hx : x ∈ L) : y ∈ R

An edge with one end in L has its other end in R.

theorem Graph.IsBipartition.mem_left_of_isLink {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} (h : G.IsBipartition L R) {e : β} {x y : ↑G.vertexSet} (he : G.IsLink e ↑x ↑y) (hx : x ∈ R) : y ∈ L

An edge with one end in R has its other end in L.

theorem Graph.IsBipartition.loopless {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} (h : G.IsBipartition L R) : G.Loopless

A multigraph with a bipartition has no loops.

theorem Graph.IsBipartition.finite {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} (h : G.IsBipartition L R) : Finite ↑G.vertexSet

A multigraph with a bipartition has finitely many actual vertices.

theorem Graph.IsBipartition.deleteEdges {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} (h : G.IsBipartition L R) (F : Set β) : (G.deleteEdges F).IsBipartition L R

Deleting any set of edges preserves a displayed bipartition. The actual vertex set, including its isolated vertices, is unchanged.

theorem Graph.IsBipartition.isVertexCover_left {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} (h : G.IsBipartition L R) : G.IsVertexCover ↑L

The side L of a bipartition is a vertex cover.

theorem Graph.IsBipartition.isVertexCover_right {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} (h : G.IsBipartition L R) : G.IsVertexCover ↑R

The side R of a bipartition is a vertex cover.

theorem Graph.IsBipartition.existsUnique_mem_left_inc {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} (h : G.IsBipartition L R) (e : ↑G.edgeSet) : ∃! x : ↑G.vertexSet, x ∈ L ∧ G.Inc ↑e ↑x

Every actual edge has exactly one end in L.

theorem Graph.IsBipartition.existsUnique_mem_right_inc {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} (h : G.IsBipartition L R) (e : ↑G.edgeSet) : ∃! x : ↑G.vertexSet, x ∈ R ∧ G.Inc ↑e ↑x

Every actual edge has exactly one end in R.

theorem Graph.IsBipartition.sum_sum_incidentEdges_left {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} [Fintype ↑G.edgeSet] {M : Type u_1} [AddCommMonoid M] (h : G.IsBipartition L R) (f : ↑G.edgeSet → M) : ∑ x ∈ L, ∑ e ∈ G.incidentEdges {x}, f e = ∑ e : ↑G.edgeSet, f e

Every actual edge has exactly one end in L, so summing over L the values of the edges incident with each vertex sums every actual edge once.

theorem Graph.IsBipartition.sum_sum_incidentEdges_right {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} [Fintype ↑G.edgeSet] {M : Type u_1} [AddCommMonoid M] (h : G.IsBipartition L R) (f : ↑G.edgeSet → M) : ∑ x ∈ R, ∑ e ∈ G.incidentEdges {x}, f e = ∑ e : ↑G.edgeSet, f e

Every actual edge has exactly one end in R, so summing over R the values of the edges incident with each vertex sums every actual edge once.

theorem Graph.isBipartition_comm {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} : G.IsBipartition L R ↔ G.IsBipartition R L

A bipartition is symmetric in its two sides.

Bipartite arrow family

def Graph.BipartiteHom {α : Type u} {β : Type v} (G : Graph α β) (L : Finset ↑G.vertexSet) (x y : ↑G.vertexSet) : Type v

The arrow family obtained by directing every actual edge of G from its end in L to its other end. Under a bipartition by L, R, these are exactly the edges directed from L to R.

instance Graph.instFiniteBipartiteHomOfElemEdgeSet {α : Type u} {β : Type v} {G : Graph α β} [Finite ↑G.edgeSet] (L : Finset ↑G.vertexSet) (x y : ↑G.vertexSet) : Finite (G.BipartiteHom L x y)

@[instance_reducible]

noncomputable instance Graph.instFintypeBipartiteHomOfElemEdgeSet {α : Type u} {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] (L : Finset ↑G.vertexSet) (x y : ↑G.vertexSet) : Fintype (G.BipartiteHom L x y)

def Graph.BipartiteHom.edge {α : Type u} {β : Type v} {G : Graph α β} {L : Finset ↑G.vertexSet} {x y : ↑G.vertexSet} (e : G.BipartiteHom L x y) : ↑G.edgeSet

The original edge underlying an arrow of the bipartite arrow family.

@[simp]

theorem Graph.BipartiteHom.edge_mk {α : Type u} {β : Type v} {G : Graph α β} {L : Finset ↑G.vertexSet} {x y : ↑G.vertexSet} (e : ↑G.edgeSet) (h : G.IsLink ↑e ↑x ↑y ∧ x ∈ L) : edge ⟨e, h⟩ = e

theorem Graph.BipartiteHom.isLink {α : Type u} {β : Type v} {G : Graph α β} {L : Finset ↑G.vertexSet} {x y : ↑G.vertexSet} (e : G.BipartiteHom L x y) : G.IsLink ↑e.edge ↑x ↑y

The edge underlying a bipartite arrow links its source to its target.

theorem Graph.BipartiteHom.ext {α : Type u} {β : Type v} {G : Graph α β} {L : Finset ↑G.vertexSet} {x y : ↑G.vertexSet} {e e' : G.BipartiteHom L x y} (h : e.edge = e'.edge) : e = e'

Bipartite arrows are equal when their underlying edges are equal.

theorem Graph.BipartiteHom.ext_iff {α : Type u} {β : Type v} {G : Graph α β} {L : Finset ↑G.vertexSet} {x y : ↑G.vertexSet} {e e' : G.BipartiteHom L x y} : e = e' ↔ e.edge = e'.edge

theorem Graph.BipartiteHom.source_mem {α : Type u} {β : Type v} {G : Graph α β} {L : Finset ↑G.vertexSet} {x y : ↑G.vertexSet} (e : G.BipartiteHom L x y) : x ∈ L

The source of every bipartite arrow belongs to L.

theorem Graph.BipartiteHom.target_mem {α : Type u} {β : Type v} {G : Graph α β} {L R : Finset ↑G.vertexSet} (hLR : G.IsBipartition L R) {x y : ↑G.vertexSet} (e : G.BipartiteHom L x y) : y ∈ R

The target of every bipartite arrow belongs to R.

theorem SimpleGraph.isBipartition_ofSimpleGraph_iff {α : Type u} (H : SimpleGraph α) (L R : Finset ↑(Graph.ofSimpleGraph H).vertexSet) : (Graph.ofSimpleGraph H).IsBipartition L R ↔ H.IsBipartiteWith (Subtype.val '' ↑L) (Subtype.val '' ↑R) ∧ Subtype.val '' ↑L ∪ Subtype.val '' ↑R = Set.univ

Finite sets L and R form a covering bipartition of the multigraph associated to a simple graph H exactly when they are bipartition classes of H and cover its entire vertex type.

The covering condition is separate because SimpleGraph.IsBipartiteWith permits isolated vertices outside both displayed sets, whereas Graph.IsBipartition partitions all actual vertices.