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_graph
is a structure for symmetric, irreflexive relations -
neighbor_set
is theset
of vertices adjacent to a given vertex -
neighbor_finset
is thefinset
of vertices adjacent to a given vertex, ifneighbor_set
is finite -
incidence_set
is theset
of edges containing a given vertex -
incidence_finset
is thefinset
of edges containing a given vertex, ifincidence_set
is finite
Implementation notes #
-
A locally finite graph is one with instances
∀ v, fintype (G.neighbor_set v)
. -
Given instances
decidable_rel G.adj
andfintype V
, then the graph is locally finite, too.
Naming Conventions #
- If the vertex type of a graph is finite, we refer to its cardinality as
card_verts
.
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.
Construct the simple graph induced by the given relation. It symmetrizes the relation and makes it irreflexive.
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 = λ (v w : V), not.decidable
G.neighbor_set v
is the set of vertices adjacent to v
in G
.
Equations
- G.neighbor_set v = set_of (G.adj v)
Equations
- simple_graph.neighbor_set.mem_decidable G v = _.mpr (λ (a : V), set.decidable_set_of (λ (a : V), G.adj v a) a)
The edges of G consist of the unordered pairs of vertices related by
G.adj
.
Equations
- G.edge_set = sym2.from_rel _
The incidence_set
is the set of edges incident to a given vertex.
Equations
- G.incidence_set v = {e ∈ G.edge_set | v ∈ e}
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
Equations
- G.edges_fintype = subtype.fintype (λ (x : sym2 V), x ∈ G.edge_set)
Equations
- G.incidence_set_decidable_pred v = λ (e : sym2 V), and.decidable
The edge_set
of the graph as a finset
.
Equations
The set of common neighbors between two vertices v
and w
in a graph G
is the
intersection of the neighbor sets of v
and w
.
Equations
- G.common_neighbors v w = G.neighbor_set v ∩ G.neighbor_set w
Equations
- simple_graph.common_neighbors.decidable_pred G v w = λ (a : V), and.decidable
Given an edge incident to a particular vertex, get the other vertex on the edge.
Equations
There is an equivalence between the set of edges incident to a given vertex and the set of vertices adjacent to the vertex.
Equations
- G.incidence_set_equiv_neighbor_set v = {to_fun := λ (e : ↥(G.incidence_set v)), ⟨G.other_vertex_of_incident _, _⟩, inv_fun := λ (w : ↥(G.neighbor_set v)), ⟨⟦(v, w.val)⟧, _⟩, left_inv := _, right_inv := _}
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
Equations
This is the finset
version of incidence_set
.
Equations
- G.incidence_finset v = (G.incidence_set v).to_finset
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)
The minimum degree of all vertices
Equations
- G.min_degree = (finset.image (λ (v : V), G.degree v) finset.univ).min' _
The maximum degree of all vertices
Equations
- G.max_degree = (finset.image (λ (v : V), G.degree v) finset.univ).max' _
If the condition G.adj v w
fails, then card_common_neighbors_le_degree
is
the best we can do in general.
Complement of a simple graph #
This section contains definitions and lemmas concerning the complement of a simple graph.
We define compl G
to be the simple_graph V
such that no two adjacent vertices in G
are adjacent in the complement, and every nonadjacent pair of vertices is adjacent
(still ensuring that vertices are not adjacent to themselves.)
Equations
Equations
- simple_graph.compl_adj_decidable V G = λ (v w : V), and.decidable