Simple graphs
This module defines simple graphs on a vertex type V as an
irreflexive symmetric relation.
There is a basic API for locally finite graphs and for graphs with finitely many vertices.
Main definitions
simple_graphis a structure for symmetric, irreflexive relationsneighbor_setis thesetof vertices adjacent to a given vertexneighbor_finsetis thefinsetof vertices adjacent to a given vertex, ifneighbor_setis finite
Implementation notes
A locally finite graph is one with instances
∀ v, fintype (G.neighbor_set v).Given instances
decidable_rel G.adjandfintype V, then the graph is locally finite, too.
TODO: This is the simplest notion of an unoriented graph. This should eventually fit into a more complete combinatorics hierarchy which includes multigraphs and directed graphs. We begin with simple graphs in order to start learning what the combinatorics hierarchy should look like.
TODO: Part of this would include defining, for example, subgraphs of a simple graph.
A simple graph is an irreflexive symmetric relation adj on a vertex type V.
The relation describes which pairs of vertices are adjacent.
There is exactly one edge for every pair of adjacent edges;
see simple_graph.edge_set for the corresponding edge set.
The complete graph on a type V is the simple graph with all pairs of distinct vertices adjacent.
Equations
Equations
- complete_graph_adj_decidable V = id (λ (a b : V), ne.decidable a b)
G.neighbor_set v is the set of vertices adjacent to v in G.
Equations
- G.neighbor_set v = set_of (G.adj v)
The edges of G consist of the unordered pairs of vertices related by
G.adj.
Equations
- G.edge_set = sym2.from_rel _
Two vertices are adjacent iff there is an edge between them. The
condition v ≠ w ensures they are different endpoints of the edge,
which is necessary since when v = w the existential
∃ (e ∈ G.edge_set), v ∈ e ∧ w ∈ e is satisfied by every edge
incident to v.
Equations
- G.edges_fintype = id (subtype.fintype (λ (x : sym2 V), x ∈ sym2.from_rel _))
The edge_set of the graph as a finset.
Equations
Finiteness at a vertex
This section contains definitions and lemmas concerning vertices that
have finitely many adjacent vertices. We denote this condition by
fintype (G.neighbor_set v).
We define G.neighbor_finset v to be the finset version of G.neighbor_set v.
Use neighbor_finset_eq_filter to rewrite this definition as a filter.
G.neighbors v is the finset version of G.adj v in case G is
locally finite at v.
Equations
- G.neighbor_finset v = (G.neighbor_set v).to_finset
G.degree v is the number of vertices adjacent to v.
Equations
- G.degree v = (G.neighbor_finset v).card
A graph is locally finite if every vertex has a finite neighbor set.
Equations
- G.locally_finite = Π (v : V), fintype ↥(G.neighbor_set v)
A locally finite simple graph is regular of degree d if every vertex has degree d.
Equations
- G.is_regular_of_degree d = ∀ (v : V), G.degree v = d
Equations
- G.neighbor_set_fintype v = subtype.fintype (λ (x : V), x ∈ G.neighbor_set v)