mathlib documentation

combinatorics.simple_graph

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 the set of vertices adjacent to a given vertex
neighbor_finset is the finset of vertices adjacent to a given vertex, if neighbor_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 and fintype 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.

structure simple_graph (V : Type u) :

Type u

adj : V → V → Prop
sym : symmetric c.adj . "obviously"
loopless : irreflexive c.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 edges; see simple_graph.edge_set for the corresponding edge set.

def complete_graph (V : Type u) :

The complete graph on a type V is the simple graph with all pairs of distinct vertices adjacent.

Equations

complete_graph V = {adj := ne V, sym := _, loopless := _}

@[instance]

def simple_graph.inhabited (V : Type u) :

inhabited (simple_graph V)

Equations

simple_graph.inhabited V = {default := complete_graph V}

@[instance]

def complete_graph_adj_decidable (V : Type u) [decidable_eq V] :

decidable_rel (complete_graph V).adj

Equations

complete_graph_adj_decidable V = id (λ (a b : V), ne.decidable a b)

def simple_graph.neighbor_set {V : Type u} (G : simple_graph V) (v : V) :

G.neighbor_set v is the set of vertices adjacent to v in G.

Equations

G.neighbor_set v = set_of (G.adj v)

theorem simple_graph.ne_of_adj {V : Type u} (G : simple_graph V) {a b : V} (hab : G.adj a b) :

a ≠ b

def simple_graph.edge_set {V : Type u} (G : simple_graph V) :

The edges of G consist of the unordered pairs of vertices related by G.adj.

Equations

G.edge_set = sym2.from_rel _

@[simp]

theorem simple_graph.mem_edge_set {V : Type u} (G : simple_graph V) {v w : V} :

⟦(v, w)⟧ ∈ G.edge_set ↔ G.adj v w

theorem simple_graph.adj_iff_exists_edge {V : Type u} (G : simple_graph V) {v w : V} :

G.adj v w ↔ v ≠ w ∧ ∃ (e : sym2 V) (H : e ∈ G.edge_set), v ∈ e ∧ w ∈ 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.

theorem simple_graph.edge_other_ne {V : Type u} (G : simple_graph V) {e : sym2 V} (he : e ∈ G.edge_set) {v : V} (h : v ∈ e) :

sym2.mem.other h ≠ v

@[instance]

def simple_graph.edges_fintype {V : Type u} (G : simple_graph V) [decidable_eq V] [fintype V] [decidable_rel G.adj] :

fintype ↥(G.edge_set)

Equations

G.edges_fintype = id (subtype.fintype (λ (x : sym2 V), x ∈ sym2.from_rel _))

def simple_graph.edge_finset {V : Type u} (G : simple_graph V) [decidable_eq V] [fintype V] [decidable_rel G.adj] :

finset (sym2 V)

The edge_set of the graph as a finset.

Equations

G.edge_finset = G.edge_set.to_finset

@[simp]

theorem simple_graph.mem_edge_finset {V : Type u} (G : simple_graph V) [decidable_eq V] [fintype V] [decidable_rel G.adj] (e : sym2 V) :

e ∈ G.edge_finset ↔ e ∈ G.edge_set

@[simp]

theorem simple_graph.irrefl {V : Type u} (G : simple_graph V) {v : V} :

¬G.adj v v

theorem simple_graph.edge_symm {V : Type u} (G : simple_graph V) (u v : V) :

G.adj u v ↔ G.adj v u

@[simp]

theorem simple_graph.mem_neighbor_set {V : Type u} (G : simple_graph V) (v w : V) :

w ∈ G.neighbor_set v ↔ G.adj v w

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.

def simple_graph.neighbor_finset {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] :

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

@[simp]

theorem simple_graph.mem_neighbor_finset {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] (w : V) :

w ∈ G.neighbor_finset v ↔ G.adj v w

def simple_graph.degree {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] :

G.degree v is the number of vertices adjacent to v.

Equations

G.degree v = (G.neighbor_finset v).card

@[simp]

theorem simple_graph.card_neighbor_set_eq_degree {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] :

fintype.card ↥(G.neighbor_set v) = G.degree v

def simple_graph.locally_finite {V : Type u} (G : simple_graph V) :

Type u

A graph is locally finite if every vertex has a finite neighbor set.

Equations

G.locally_finite = Π (v : V), fintype ↥(G.neighbor_set v)

def simple_graph.is_regular_of_degree {V : Type u} (G : simple_graph V) [G.locally_finite] (d : ℕ) :

Prop

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

@[instance]

def simple_graph.neighbor_set_fintype {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (v : V) :

fintype ↥(G.neighbor_set v)

Equations

G.neighbor_set_fintype v = subtype.fintype (λ (x : V), x ∈ G.neighbor_set v)

theorem simple_graph.neighbor_finset_eq_filter {V : Type u} (G : simple_graph V) [fintype V] {v : V} [decidable_rel G.adj] :

G.neighbor_finset v = finset.filter (G.adj v) finset.univ

@[simp]

theorem simple_graph.complete_graph_degree {V : Type u} [fintype V] [decidable_eq V] (v : V) :

(complete_graph V).degree v = fintype.card V - 1

theorem simple_graph.complete_graph_is_regular {V : Type u} [fintype V] [decidable_eq V] :

(complete_graph V).is_regular_of_degree (fintype.card V - 1)