Digraphs

This module defines directed graphs on a vertex type V, which is the same notion as a relation V → V → Prop. While this might be too simple of a notion to deserve the grandeur of a new definition, the intention here is to develop relations using the language of graph theory.

Note that in this treatment, a digraph may have self loops.

The type Digraph V is structurally equivalent to Quiver.{0} V, but a difference between these is that Quiver is a class — its purpose is to attach a quiver structure to a particular type V. In contrast, for Digraph V we are interested in working with the entire lattice of digraphs on V.

Main definitions

• Digraph is a structure for relations. Unlike SimpleGraph, the relation does not need to be symmetric or irreflexive.

• CompleteAtomicBooleanAlgebra instance: Under the subgraph relation, Digraph forms a CompleteAtomicBooleanAlgebra. In other words, this is the complete lattice of spanning subgraphs of the complete graph.

structure Digraph (V : Type u_1) : Type u_1

A digraph is a relation Adj on a vertex type V. The relation describes which pairs of vertices are adjacent.

In this treatment, a digraph may have self-loops.

• Adj : V → V → Prop

  The adjacency relation of a digraph.

theorem Digraph.ext_iff {V : Type u_1} {x y : Digraph V} : x = y ↔ x.Adj = y.Adj

theorem Digraph.ext {V : Type u_1} {x y : Digraph V} (Adj : x.Adj = y.Adj) : x = y

def Digraph.mk' {V : Type u_1} : (V → V → Bool) ↪ Digraph V

Constructor for digraphs using a Boolean function. This is useful for creating a digraph with a decidable Adj relation, and it's used in the construction of the Fintype (Digraph V) instance.

@[simp]

theorem Digraph.mk'_apply_Adj {V : Type u_1} (x : V → V → Bool) (v w : V) : (mk' x).Adj v w = (x v w = true)

@[implicit_reducible]

instance instDecidableRelAdjCoeEmbeddingForallForallBoolDigraphMk' {V : Type u_1} (adj : V → V → Bool) : DecidableRel (Digraph.mk' adj).Adj

@[implicit_reducible]

instance instFintypeDigraphOfDecidableEq {V : Type u_1} [DecidableEq V] [Fintype V] : Fintype (Digraph V)

def Digraph.completeDigraph (V : Type u_1) : Digraph V

The complete digraph on a type V (denoted by ⊤) is the digraph whose vertices are all adjacent. Note that every vertex is adjacent to itself in ⊤.

def Digraph.emptyDigraph (V : Type u_1) : Digraph V

The empty digraph on a type V (denoted by ⊥) is the digraph such that no pairs of vertices are adjacent. Note that ⊥ is called the empty digraph because it has no edges.

def Digraph.completeBipartiteGraph (V : Type u_1) (W : Type u_2) : Digraph (V ⊕ W)

Two vertices are adjacent in the complete bipartite digraph on two vertex types if and only if they are not from the same side. Any bipartite digraph may be regarded as a subgraph of one of these.

@[simp]

theorem Digraph.completeBipartiteGraph_Adj (V : Type u_1) (W : Type u_2) (v w : V ⊕ W) : (completeBipartiteGraph V W).Adj v w = (v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true)

theorem Digraph.adj_injective {V : Type u_2} : Function.Injective Adj

@[simp]

theorem Digraph.adj_inj {V : Type u_2} {G H : Digraph V} : G.Adj = H.Adj ↔ G = H

def Digraph.IsSubgraph {V : Type u_2} (x y : Digraph V) : Prop

The relation that one Digraph is a spanning subgraph of another. Note that Digraph.IsSubgraph G H should be spelled G ≤ H.

@[implicit_reducible]

instance Digraph.instLE {V : Type u_2} : LE (Digraph V)

For digraphs G, H, G ≤ H iff ∀ a b, G.Adj a b → H.Adj a b.

@[simp]

theorem Digraph.isSubgraph_eq_le {V : Type u_2} : Digraph.IsSubgraph = fun (x1 x2 : Digraph V) => x1 ≤ x2

@[implicit_reducible]

instance Digraph.instMax {V : Type u_2} : Max (Digraph V)

The supremum of two digraphs x ⊔ y has edges where either x or y have edges.

@[simp]

theorem Digraph.sup_adj {V : Type u_2} (x y : Digraph V) (v w : V) : (x ⊔ y).Adj v w ↔ x.Adj v w ∨ y.Adj v w

@[implicit_reducible]

instance Digraph.instMin {V : Type u_2} : Min (Digraph V)

The infimum of two digraphs x ⊓ y has edges where both x and y have edges.

@[simp]

theorem Digraph.inf_adj {V : Type u_2} (x y : Digraph V) (v w : V) : (x ⊓ y).Adj v w ↔ x.Adj v w ∧ y.Adj v w

@[implicit_reducible]

instance Digraph.instCompl {V : Type u_2} : Compl (Digraph V)

We define Gᶜ to be the Digraph V such that no two adjacent vertices in G are adjacent in the complement, and every nonadjacent pair of vertices is adjacent.

@[simp]

theorem Digraph.compl_adj {V : Type u_2} (G : Digraph V) (v w : V) : Gᶜ.Adj v w ↔ ¬G.Adj v w

@[implicit_reducible]

instance Digraph.sdiff {V : Type u_2} : SDiff (Digraph V)

The difference of two digraphs x \ y has the edges of x with the edges of y removed.

@[simp]

theorem Digraph.sdiff_adj {V : Type u_2} (x y : Digraph V) (v w : V) : (x \ y).Adj v w ↔ x.Adj v w ∧ ¬y.Adj v w

@[implicit_reducible]

instance Digraph.supSet {V : Type u_2} : SupSet (Digraph V)

@[implicit_reducible]

instance Digraph.infSet {V : Type u_2} : InfSet (Digraph V)

@[simp]

theorem Digraph.sSup_adj {V : Type u_2} {a b : V} {s : Set (Digraph V)} : (sSup s).Adj a b ↔ ∃ G ∈ s, G.Adj a b

@[simp]

theorem Digraph.sInf_adj {V : Type u_2} {a b : V} {s : Set (Digraph V)} : (sInf s).Adj a b ↔ ∀ G ∈ s, G.Adj a b

@[simp]

theorem Digraph.iSup_adj {ι : Sort u_1} {V : Type u_2} {a b : V} {f : ι → Digraph V} : (⨆ (i : ι), f i).Adj a b ↔ ∃ (i : ι), (f i).Adj a b

@[simp]

theorem Digraph.iInf_adj {ι : Sort u_1} {V : Type u_2} {a b : V} {f : ι → Digraph V} : (⨅ (i : ι), f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b

@[implicit_reducible]

instance Digraph.instPartialOrder {V : Type u_2} : PartialOrder (Digraph V)

@[implicit_reducible]

instance Digraph.distribLattice {V : Type u_2} : DistribLattice (Digraph V)

@[implicit_reducible]

instance Digraph.completeAtomicBooleanAlgebra {V : Type u_2} : CompleteAtomicBooleanAlgebra (Digraph V)

@[simp]

theorem Digraph.top_adj {V : Type u_2} (v w : V) : ⊤.Adj v w

@[simp]

theorem Digraph.bot_adj {V : Type u_2} (v w : V) : ⊥.Adj v w ↔ False

@[simp]

theorem Digraph.completeDigraph_eq_top (V : Type u_3) : Digraph.completeDigraph V = ⊤

@[simp]

theorem Digraph.emptyDigraph_eq_bot (V : Type u_3) : Digraph.emptyDigraph V = ⊥

@[implicit_reducible]

instance Digraph.instInhabited (V : Type u_3) : Inhabited (Digraph V)

@[simp]

theorem Digraph.default_def (V : Type u_3) : default = ⊥

@[implicit_reducible]

instance Digraph.instUniqueOfIsEmpty {V : Type u_2} [IsEmpty V] : Unique (Digraph V)

instance Digraph.instNontrivialOfNonempty {V : Type u_2} [Nonempty V] : Nontrivial (Digraph V)

@[implicit_reducible]

instance Digraph.Bot.adjDecidable (V : Type u_2) : DecidableRel ⊥.Adj

@[implicit_reducible]

instance Digraph.Sup.adjDecidable (V : Type u_2) (G H : Digraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] : DecidableRel (G ⊔ H).Adj

@[implicit_reducible]

instance Digraph.Inf.adjDecidable (V : Type u_2) (G H : Digraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] : DecidableRel (G ⊓ H).Adj

@[implicit_reducible]

instance Digraph.SDiff.adjDecidable (V : Type u_2) (G H : Digraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] : DecidableRel (G \ H).Adj

@[implicit_reducible]

instance Digraph.Top.adjDecidable (V : Type u_2) : DecidableRel ⊤.Adj

@[implicit_reducible]

instance Digraph.Compl.adjDecidable (V : Type u_2) (G : Digraph V) [DecidableRel G.Adj] : DecidableRel Gᶜ.Adj