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 -
simple_graph.neighbor_set
is theset
of vertices adjacent to a given vertex -
simple_graph.common_neighbors
is the intersection of the neighbor sets of two given vertices -
simple_graph.neighbor_finset
is thefinset
of vertices adjacent to a given vertex, ifneighbor_set
is finite -
simple_graph.incidence_set
is theset
of edges containing a given vertex -
simple_graph.incidence_finset
is thefinset
of edges containing a given vertex, ifincidence_set
is finite -
simple_graph.dart
is an ordered pair of adjacent vertices, thought of as being an orientated edge. These are also known as "half-edges" or "bonds." -
simple_graph.hom
,simple_graph.embedding
, andsimple_graph.iso
for graph homomorphisms, graph embeddings, and graph isomorphisms. Note that a graph embedding is a stronger notion than an injective graph homomorphism, since its image is an induced subgraph. -
boolean_algebra
instance: Under the subgraph relation,simple_graph
forms aboolean_algebra
. In other words, this is the lattice of spanning subgraphs of the complete graph.
Notations #
→g
,↪g
, and≃g
for graph homomorphisms, graph embeddings, and graph isomorphisms, respectively.
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. -
Morphisms of graphs are abbreviations for
rel_hom
,rel_embedding
, andrel_iso
. To make use of pre-existing simp lemmas, definitions involving morphisms are abbreviations as well.
Naming Conventions #
- If the vertex type of a graph is finite, we refer to its cardinality as
card_verts
.
Todo #
-
Upgrade
simple_graph.boolean_algebra
to acomplete_boolean_algebra
. -
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.
- adj : V → V → Prop
- symm : symmetric self.adj . "obviously"
- loopless : irreflexive self.adj . "obviously"
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 vertices;
see simple_graph.edge_set
for the corresponding edge set.
Instances for simple_graph
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. In mathlib
, this is usually referred to as ⊤
.
The graph with no edges on a given vertex type V
. mathlib
prefers the notation ⊥
.
Two vertices are adjacent in the complete bipartite graph on two vertex types if and only if they are not from the same side. Bipartite graphs in general may be regarded as being subgraphs of one of these.
TODO also introduce complete multi-partite graphs, where the vertex type is a sigma type of an indexed family of vertex types
The relation that one simple_graph
is a subgraph of another.
Note that this should be spelled ≤
.
Equations
- x.is_subgraph y = ∀ ⦃v w : V⦄, x.adj v w → y.adj v w
Equations
The supremum of two graphs x ⊔ y
has edges where either x
or y
have edges.
The infimum of two graphs x ⊓ y
has edges where both x
and y
have edges.
We define 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).
The difference of two graphs x \ y
has the edges of x
with the edges of y
removed.
Equations
- simple_graph.boolean_algebra = {sup := has_sup.sup simple_graph.has_sup, le := has_le.le simple_graph.has_le, lt := partial_order.lt (partial_order.lift simple_graph.adj simple_graph.ext), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf simple_graph.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, compl := has_compl.compl simple_graph.has_compl, sdiff := has_sdiff.sdiff simple_graph.has_sdiff, himp := λ (x y : simple_graph V), distrib_lattice.sup y xᶜ, top := complete_graph V, bot := empty_graph V, inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _, himp_eq := _}
Equations
- simple_graph.inhabited V = {default := ⊥}
Equations
- simple_graph.bot.adj_decidable V = λ (v w : V), decidable.false
Equations
- simple_graph.sup.adj_decidable V G H = λ (v w : V), or.decidable
Equations
- simple_graph.inf.adj_decidable V G H = λ (v w : V), and.decidable
Equations
- simple_graph.sdiff.adj_decidable V G H = λ (v w : V), and.decidable
Equations
- simple_graph.top.adj_decidable V = λ (v w : V), not.decidable
Equations
- simple_graph.compl.adj_decidable V G = λ (v w : V), and.decidable
G.support
is the set of vertices that form edges in G
.
G.neighbor_set v
is the set of vertices adjacent to v
in G
.
Equations
- G.neighbor_set v = set_of (G.adj v)
Instances for ↥simple_graph.neighbor_set
Equations
- simple_graph.neighbor_set.mem_decidable G v = _.mpr (λ (a : V), set.decidable_set_of a (λ (a : V), G.adj v a))
The edges of G consist of the unordered pairs of vertices related by
G.adj
.
The way edge_set
is defined is such that mem_edge_set
is proved by refl
.
(That is, ⟦(v, w)⟧ ∈ G.edge_set
is definitionally equal to G.adj v w
.)
Equations
- G.edge_set = sym2.from_rel _
Instances for ↥simple_graph.edge_set
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)
Darts #
A dart
is an oriented edge, implemented as an ordered pair of adjacent vertices.
This terminology comes from combinatorial maps, and they are also known as "half-edges"
or "bonds."
Instances for simple_graph.dart
- simple_graph.dart.has_sizeof_inst
- simple_graph.dart.fintype
- simple_graph.nonempty_dart_top
The first vertex for the dart.
The second vertex for the dart.
The edge associated to the dart.
Two darts are said to be adjacent if they could be consecutive darts in a walk -- that is, the first dart's second vertex is equal to the second dart's first vertex.
For a given vertex v
, this is the bijective map from the neighbor set at v
to the darts d
with d.fst = v
. -
Incidence set #
Set of edges incident to a given vertex, aka incidence set.
Equations
- G.incidence_set v = {e ∈ G.edge_set | v ∈ e}
Instances for ↥simple_graph.incidence_set
Equations
- G.decidable_mem_incidence_set 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
- G.decidable_mem_common_neighbors 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 := _}
Edge deletion #
Given a set of vertex pairs, remove all of the corresponding edges from the graph's edge set, if present.
See also: simple_graph.subgraph.delete_edges
.
Equations
- G.delete_edges s = {adj := G.adj \ sym2.to_rel s, symm := _, loopless := _}
Map and comap #
Given an injective function, there is an covariant induced map on graphs by pushing forward the adjacency relation.
This is injective (see simple_graph.map_injective
).
Equations
- simple_graph.map f G = {adj := relation.map G.adj ⇑f ⇑f, symm := _, loopless := _}
Given a function, there is a contravariant induced map on graphs by pulling back the
adjacency relation.
This is one of the ways of creating induced graphs. See simple_graph.induce
for a wrapper.
This is surjective when f
is injective (see simple_graph.comap_surjective
).
Induced graphs #
Restrict a graph to the vertices in the set s
, deleting all edges incident to vertices
outside the set. This is a wrapper around simple_graph.comap
.
Equations
- simple_graph.induce s G = simple_graph.comap ⇑(function.embedding.subtype (λ (x : V), x ∈ s)) G
Given a graph on a set of vertices, we can make it be a simple_graph V
by
adding in the remaining vertices without adding in any additional edges.
This is a wrapper around simple_graph.map
.
Equations
- G.spanning_coe = simple_graph.map (function.embedding.subtype (λ (x : V), x ∈ s)) G
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 (and 0
if there are no vertices).
The key properties of this are given in exists_minimal_degree_vertex
, min_degree_le_degree
and le_min_degree_of_forall_le_degree
.
Equations
- G.min_degree = with_top.untop' 0 (finset.image (λ (v : V), G.degree v) finset.univ).min
There exists a vertex of minimal degree. Note the assumption of being nonempty is necessary, as the lemma implies there exists a vertex.
The minimum degree in the graph is at most the degree of any particular vertex.
In a nonempty graph, if k
is at most the degree of every vertex, it is at most the minimum
degree. Note the assumption that the graph is nonempty is necessary as long as G.min_degree
is
defined to be a natural.
The maximum degree of all vertices (and 0
if there are no vertices).
The key properties of this are given in exists_maximal_degree_vertex
, degree_le_max_degree
and max_degree_le_of_forall_degree_le
.
Equations
- G.max_degree = option.get_or_else (finset.image (λ (v : V), G.degree v) finset.univ).max 0
There exists a vertex of maximal degree. Note the assumption of being nonempty is necessary, as the lemma implies there exists a vertex.
The maximum degree in the graph is at least the degree of any particular vertex.
In a graph, if k
is at least the degree of every vertex, then it is at least the maximum
degree.
The maximum degree of a nonempty graph is less than the number of vertices. Note that the assumption
that V
is nonempty is necessary, as otherwise this would assert the existence of a
natural number less than zero.
If the condition G.adj v w
fails, then card_common_neighbors_le_degree
is
the best we can do in general.
A graph homomorphism is a map on vertex sets that respects adjacency relations.
The notation G →g G'
represents the type of graph homomorphisms.
A graph embedding is an embedding f
such that for vertices v w : V
,
G.adj f(v) f(w) ↔ G.adj v w
. Its image is an induced subgraph of G'.
The notation G ↪g G'
represents the type of graph embeddings.
A graph isomorphism is an bijective map on vertex sets that respects adjacency relations.
The notation G ≃g G'
represents the type of graph isomorphisms.
The identity homomorphism from a graph to itself.
The map between edge sets induced by a homomorphism.
The underlying map on edges is given by sym2.map
.
The map between neighbor sets induced by a homomorphism.
Equations
- f.map_neighbor_set v w = ⟨⇑f ↑w, _⟩
The induced map for spanning subgraphs, which is the identity on vertices.
Equations
- simple_graph.hom.map_spanning_subgraphs h = {to_fun := λ (x : V), x, map_rel' := h}
Every graph homomomorphism from a complete graph is injective.
There is a homomorphism to a graph from a comapped graph.
When the function is injective, this is an embedding (see simple_graph.embedding.comap
).
Equations
- simple_graph.hom.comap f G = {to_fun := f, map_rel' := _}
Composition of graph homomorphisms.
The identity embedding from a graph to itself.
An embedding of graphs gives rise to a homomorphism of graphs.
A graph embedding induces an embedding of edge sets.
Equations
- f.map_edge_set = {to_fun := ↑f.map_edge_set, inj' := _}
A graph embedding induces an embedding of neighbor sets.
Equations
- f.map_neighbor_set v = {to_fun := λ (w : ↥(G.neighbor_set v)), ⟨⇑f ↑w, _⟩, inj' := _}
Given an injective function, there is an embedding from the comapped graph into the original graph.
Equations
- simple_graph.embedding.comap f G = {to_embedding := {to_fun := f.to_fun, inj' := _}, map_rel_iff' := _}
Given an injective function, there is an embedding from a graph into the mapped graph.
Equations
- simple_graph.embedding.map f G = {to_embedding := {to_fun := f.to_fun, inj' := _}, map_rel_iff' := _}
Induced graphs embed in the original graph.
Note that if G.induce s = ⊤
(i.e., if s
is a clique) then this gives the embedding of a
complete graph.
Equations
- simple_graph.embedding.induce s = simple_graph.embedding.comap (function.embedding.subtype (λ (x : V), x ∈ s)) G
Graphs on a set of vertices embed in their spanning_coe
.
Equations
- simple_graph.embedding.spanning_coe G = simple_graph.embedding.map (function.embedding.subtype (λ (x : V), x ∈ s)) G
Embeddings of types induce embeddings of complete graphs on those types.
Equations
- simple_graph.embedding.complete_graph f = {to_embedding := {to_fun := f.to_fun, inj' := _}, map_rel_iff' := _}
Composition of graph embeddings.
The identity isomorphism of a graph with itself.
An isomorphism of graphs gives rise to an embedding of graphs.
An isomorphism of graphs gives rise to a homomorphism of graphs.
The inverse of a graph isomorphism. -
An isomorphism of graphs induces an equivalence of edge sets.
Equations
- f.map_edge_set = {to_fun := ↑f.map_edge_set, inv_fun := ↑(f.symm).map_edge_set, left_inv := _, right_inv := _}
A graph isomorphism induces an equivalence of neighbor sets.
Given a bijection, there is an embedding from the comapped graph into the original graph.
Given an injective function, there is an embedding from a graph into the mapped graph.
Equivalences of types induce isomorphisms of complete graphs on those types.
Composition of graph isomorphisms.