# 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.

## Equations

- instDecidableRelAdjCoeEmbeddingForallForallBoolDigraphMk' adj = inferInstanceAs (DecidableRel fun (v w : V) => adj v w = true)

## Equations

- instFintypeDigraphOfDecidableEq = Fintype.ofBijective ⇑Digraph.mk' ⋯

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 `⊤`

.

## Equations

- Digraph.completeDigraph V = { Adj := ⊤ }

## Instances For

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.

## Equations

- Digraph.emptyDigraph V = { Adj := fun (x x : V) => False }

## Instances For

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.

## Equations

## Instances For

The relation that one `Digraph`

is a spanning subgraph of another.
Note that `Digraph.IsSubgraph G H`

should be spelled `G ≤ H`

.

## Equations

- x.IsSubgraph y = ∀ ⦃v w : V⦄, x.Adj v w → y.Adj v w

## Instances For

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.

For digraphs `G`

, `H`

, `G ≤ H`

iff `∀ a b, G.Adj a b → H.Adj a b`

.

## Equations

- Digraph.distribLattice = DistribLattice.mk ⋯

## Equations

- Digraph.completeAtomicBooleanAlgebra = CompleteAtomicBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

## Equations

- Digraph.instInhabited V = { default := ⊥ }

## Equations

- ⋯ = ⋯

## Equations

- Digraph.Bot.adjDecidable V = inferInstanceAs (DecidableRel fun (x x : V) => False)

## Equations

- Digraph.Sup.adjDecidable V G H = inferInstanceAs (DecidableRel fun (v w : V) => G.Adj v w ∨ H.Adj v w)

## Equations

- Digraph.Inf.adjDecidable V G H = inferInstanceAs (DecidableRel fun (v w : V) => G.Adj v w ∧ H.Adj v w)

## Equations

- Digraph.SDiff.adjDecidable V G H = inferInstanceAs (DecidableRel fun (v w : V) => G.Adj v w ∧ ¬H.Adj v w)

## Equations

- Digraph.Top.adjDecidable V = inferInstanceAs (DecidableRel fun (x x : V) => True)

## Equations

- Digraph.Compl.adjDecidable V G = inferInstanceAs (DecidableRel fun (v w : V) => ¬G.Adj v w)