Maps between graphs

This file defines two functions and three structures relating graphs. The structures directly correspond to the classification of functions as injective, surjective and bijective, and have corresponding notation.

Main definitions

• SimpleGraph.map: the graph obtained by pushing the adjacency relation through an injective function between vertex types.
• SimpleGraph.comap: the graph obtained by pulling the adjacency relation behind an arbitrary function between vertex types.
• SimpleGraph.induce: the subgraph induced by the given vertex set, a wrapper around comap.
• SimpleGraph.spanningCoe: the supergraph without any additional edges, a wrapper around map.
• SimpleGraph.Hom, G →g H: a graph homomorphism from G to H.
• SimpleGraph.Embedding, G ↪g H: a graph embedding of G in H.
• SimpleGraph.Iso, G ≃g H: a graph isomorphism between G and H.

Note that a graph embedding is a stronger notion than an injective graph homomorphism, since its image is an induced subgraph.

Implementation notes

Morphisms of graphs are abbreviations for RelHom, RelEmbedding and RelIso. To make use of pre-existing simp lemmas, definitions involving morphisms are abbreviations as well.

Map and comap

def SimpleGraph.map {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) : SimpleGraph W

Given an injective function, there is a covariant induced map on graphs by pushing forward the adjacency relation.

This is injective (see SimpleGraph.map_injective).

Equations

• SimpleGraph.map f G = { Adj := Relation.Map G.Adj ⇑f ⇑f, symm := ⋯, loopless := ⋯ }

instance SimpleGraph.instDecidableMapAdj {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) {f : V ↪ W} {a : W} {b : W} [Decidable (Relation.Map G.Adj (⇑f) (⇑f) a b)] : Decidable ((SimpleGraph.map f G).Adj a b)

Equations

• G.instDecidableMapAdj = inst

@[simp]

theorem SimpleGraph.map_adj {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) (u : W) (v : W) : (SimpleGraph.map f G).Adj u v ↔ ∃ (u' : V) (v' : V), G.Adj u' v' ∧ f u' = u ∧ f v' = v

theorem SimpleGraph.map_adj_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {f : V ↪ W} {a : V} {b : V} : (SimpleGraph.map f G).Adj (f a) (f b) ↔ G.Adj a b

theorem SimpleGraph.map_monotone {V : Type u_1} {W : Type u_2} (f : V ↪ W) : Monotone (SimpleGraph.map f)

@[simp]

theorem SimpleGraph.map_id {V : Type u_1} (G : SimpleGraph V) : SimpleGraph.map (Function.Embedding.refl V) G = G

@[simp]

theorem SimpleGraph.map_map {V : Type u_1} {W : Type u_2} {X : Type u_3} (G : SimpleGraph V) (f : V ↪ W) (g : W ↪ X) : SimpleGraph.map g (SimpleGraph.map f G) = SimpleGraph.map (f.trans g) G

def SimpleGraph.comap {V : Type u_1} {W : Type u_2} (f : V → W) (G : SimpleGraph W) : SimpleGraph V

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 SimpleGraph.induce for a wrapper.

This is surjective when f is injective (see SimpleGraph.comap_surjective).

Equations

• SimpleGraph.comap f G = { Adj := fun (u v : V) => G.Adj (f u) (f v), symm := ⋯, loopless := ⋯ }

@[simp]

theorem SimpleGraph.comap_adj {V : Type u_1} {W : Type u_2} {u : V} {v : V} {G : SimpleGraph W} {f : V → W} : (SimpleGraph.comap f G).Adj u v ↔ G.Adj (f u) (f v)

@[simp]

theorem SimpleGraph.comap_id {V : Type u_1} {G : SimpleGraph V} : SimpleGraph.comap id G = G

@[simp]

theorem SimpleGraph.comap_comap {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph X} (f : V → W) (g : W → X) : SimpleGraph.comap f (SimpleGraph.comap g G) = SimpleGraph.comap (g ∘ f) G

instance SimpleGraph.instDecidableComapAdj {V : Type u_1} {W : Type u_2} (f : V → W) (G : SimpleGraph W) [DecidableRel G.Adj] : DecidableRel (SimpleGraph.comap f G).Adj

Equations

• SimpleGraph.instDecidableComapAdj f G x✝ x = inst (f x✝) (f x)

theorem SimpleGraph.comap_symm {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (e : V ≃ W) : SimpleGraph.comap (⇑e.symm.toEmbedding) G = SimpleGraph.map e.toEmbedding G

theorem SimpleGraph.map_symm {V : Type u_1} {W : Type u_2} (G : SimpleGraph W) (e : V ≃ W) : SimpleGraph.map e.symm.toEmbedding G = SimpleGraph.comap (⇑e.toEmbedding) G

theorem SimpleGraph.comap_monotone {V : Type u_1} {W : Type u_2} (f : V ↪ W) : Monotone (SimpleGraph.comap ⇑f)

@[simp]

theorem SimpleGraph.comap_map_eq {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) : SimpleGraph.comap (⇑f) (SimpleGraph.map f G) = G

theorem SimpleGraph.leftInverse_comap_map {V : Type u_1} {W : Type u_2} (f : V ↪ W) : Function.LeftInverse (SimpleGraph.comap ⇑f) (SimpleGraph.map f)

theorem SimpleGraph.map_injective {V : Type u_1} {W : Type u_2} (f : V ↪ W) : Function.Injective (SimpleGraph.map f)

theorem SimpleGraph.comap_surjective {V : Type u_1} {W : Type u_2} (f : V ↪ W) : Function.Surjective (SimpleGraph.comap ⇑f)

theorem SimpleGraph.map_le_iff_le_comap {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) (G' : SimpleGraph W) : SimpleGraph.map f G ≤ G' ↔ G ≤ SimpleGraph.comap (⇑f) G'

theorem SimpleGraph.map_comap_le {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph W) : SimpleGraph.map f (SimpleGraph.comap (⇑f) G) ≤ G

theorem SimpleGraph.le_comap_of_subsingleton {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) (f : V → W) [Subsingleton V] : G ≤ SimpleGraph.comap f G'

theorem SimpleGraph.map_le_of_subsingleton {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) (f : V ↪ W) [Subsingleton V] : SimpleGraph.map f G ≤ G'

@[reducible, inline]

abbrev SimpleGraph.completeMultipartiteGraph {ι : Type u_4} (V : ι → Type u_5) : SimpleGraph ((i : ι) × V i)

Given a family of vertex types indexed by ι, pulling back from ⊤ : SimpleGraph ι yields the complete multipartite graph on the family. Two vertices are adjacent if and only if their indices are not equal.

Equations

• SimpleGraph.completeMultipartiteGraph V = SimpleGraph.comap Sigma.fst ⊤

def Equiv.simpleGraph {V : Type u_1} {W : Type u_2} (e : V ≃ W) : SimpleGraph V ≃ SimpleGraph W

Equivalent types have equivalent simple graphs.

Equations

• e.simpleGraph = { toFun := SimpleGraph.comap ⇑e.symm, invFun := SimpleGraph.comap ⇑e, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.simpleGraph_apply {V : Type u_1} {W : Type u_2} (e : V ≃ W) (G : SimpleGraph V) : e.simpleGraph G = SimpleGraph.comap (⇑e.symm) G

@[simp]

theorem Equiv.simpleGraph_refl {V : Type u_1} : (Equiv.refl V).simpleGraph = Equiv.refl (SimpleGraph V)

@[simp]

theorem Equiv.simpleGraph_trans {V : Type u_1} {W : Type u_2} {X : Type u_3} (e₁ : V ≃ W) (e₂ : W ≃ X) : (e₁.trans e₂).simpleGraph = e₁.simpleGraph.trans e₂.simpleGraph

@[simp]

theorem Equiv.symm_simpleGraph {V : Type u_1} {W : Type u_2} (e : V ≃ W) : e.simpleGraph.symm = e.symm.simpleGraph

Induced graphs

@[reducible, inline]

abbrev SimpleGraph.induce {V : Type u_1} (s : Set V) (G : SimpleGraph V) : SimpleGraph ↑s

Restrict a graph to the vertices in the set s, deleting all edges incident to vertices outside the set. This is a wrapper around SimpleGraph.comap.

Equations

• SimpleGraph.induce s G = SimpleGraph.comap (⇑(Function.Embedding.subtype fun (x : V) => x ∈ s)) G

@[simp]

theorem SimpleGraph.induce_singleton_eq_top {V : Type u_1} (G : SimpleGraph V) (v : V) : SimpleGraph.induce {v} G = ⊤

@[reducible, inline]

abbrev SimpleGraph.spanningCoe {V : Type u_1} {s : Set V} (G : SimpleGraph ↑s) : SimpleGraph V

Given a graph on a set of vertices, we can make it be a SimpleGraph V by adding in the remaining vertices without adding in any additional edges. This is a wrapper around SimpleGraph.map.

Equations

• G.spanningCoe = SimpleGraph.map (Function.Embedding.subtype fun (x : V) => x ∈ s) G

theorem SimpleGraph.induce_spanningCoe {V : Type u_1} {s : Set V} {G : SimpleGraph ↑s} : SimpleGraph.induce s G.spanningCoe = G

theorem SimpleGraph.spanningCoe_induce_le {V : Type u_1} (G : SimpleGraph V) (s : Set V) : (SimpleGraph.induce s G).spanningCoe ≤ G

Homomorphisms, embeddings and isomorphisms

@[reducible, inline]

abbrev SimpleGraph.Hom {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) : Type (max u_1 u_2)

A graph homomorphism is a map on vertex sets that respects adjacency relations.

The notation G →g G' represents the type of graph homomorphisms.

Equations

• (G →g G') = (G.Adj →r G'.Adj)

@[reducible, inline]

abbrev SimpleGraph.Embedding {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) : Type (max u_1 u_2)

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.

Equations

• (G ↪g G') = (G.Adj ↪r G'.Adj)

@[reducible, inline]

abbrev SimpleGraph.Iso {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) : Type (max u_1 u_2)

A graph isomorphism is a bijective map on vertex sets that respects adjacency relations.

The notation G ≃g G' represents the type of graph isomorphisms.

Equations

• (G ≃g G') = (G.Adj ≃r G'.Adj)

def SimpleGraph.«term_→g_» : Lean.TrailingParserDescr

A graph homomorphism is a map on vertex sets that respects adjacency relations.

The notation G →g G' represents the type of graph homomorphisms.

Equations

• SimpleGraph.«term_→g_» = Lean.ParserDescr.trailingNode `SimpleGraph.«term_→g_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →g ") (Lean.ParserDescr.cat `term 51))

def SimpleGraph.«term_↪g_» : Lean.TrailingParserDescr

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.

Equations

• SimpleGraph.«term_↪g_» = Lean.ParserDescr.trailingNode `SimpleGraph.«term_↪g_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↪g ") (Lean.ParserDescr.cat `term 51))

def SimpleGraph.«term_≃g_» : Lean.TrailingParserDescr

A graph isomorphism is a bijective map on vertex sets that respects adjacency relations.

The notation G ≃g G' represents the type of graph isomorphisms.

Equations

• SimpleGraph.«term_≃g_» = Lean.ParserDescr.trailingNode `SimpleGraph.«term_≃g_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃g ") (Lean.ParserDescr.cat `term 51))

@[reducible, inline]

abbrev SimpleGraph.Hom.id {V : Type u_1} {G : SimpleGraph V} : G →g G

The identity homomorphism from a graph to itself.

Equations

• SimpleGraph.Hom.id = RelHom.id G.Adj

@[simp]

theorem SimpleGraph.Hom.coe_id {V : Type u_1} {G : SimpleGraph V} : ⇑SimpleGraph.Hom.id = id

instance SimpleGraph.Hom.instSubsingletonOfForall {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Subsingleton (V → W)] : Subsingleton (G →g H)

Equations

• ⋯ = ⋯

instance SimpleGraph.Hom.instUniqueOfIsEmpty {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [IsEmpty V] : Unique (G →g H)

Equations

• SimpleGraph.Hom.instUniqueOfIsEmpty = { default := { toFun := fun (a : V) => isEmptyElim a, map_rel' := ⋯ }, uniq := ⋯ }

instance SimpleGraph.Hom.instFinite {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Finite V] [Finite W] : Finite (G →g H)

Equations

• ⋯ = ⋯

theorem SimpleGraph.Hom.map_adj {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v : V} {w : V} (h : G.Adj v w) : G'.Adj (f v) (f w)

theorem SimpleGraph.Hom.map_mem_edgeSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {e : Sym2 V} (h : e ∈ G.edgeSet) : Sym2.map (⇑f) e ∈ G'.edgeSet

theorem SimpleGraph.Hom.apply_mem_neighborSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v : V} {w : V} (h : w ∈ G.neighborSet v) : f w ∈ G'.neighborSet (f v)

def SimpleGraph.Hom.mapEdgeSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (e : ↑G.edgeSet) : ↑G'.edgeSet

The map between edge sets induced by a homomorphism. The underlying map on edges is given by Sym2.map.

Equations

• f.mapEdgeSet e = ⟨Sym2.map ⇑f ↑e, ⋯⟩

@[simp]

theorem SimpleGraph.Hom.mapEdgeSet_coe {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (e : ↑G.edgeSet) : ↑(f.mapEdgeSet e) = Sym2.map ⇑f ↑e

def SimpleGraph.Hom.mapNeighborSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (v : V) (w : ↑(G.neighborSet v)) : ↑(G'.neighborSet (f v))

The map between neighbor sets induced by a homomorphism.

Equations

• f.mapNeighborSet v w = ⟨f ↑w, ⋯⟩

@[simp]

theorem SimpleGraph.Hom.mapNeighborSet_coe {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (v : V) (w : ↑(G.neighborSet v)) : ↑(f.mapNeighborSet v w) = f ↑w

def SimpleGraph.Hom.mapDart {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (d : G.Dart) : G'.Dart

The map between darts induced by a homomorphism.

Equations

• f.mapDart d = { toProd := Prod.map (⇑f) (⇑f) d.toProd, adj := ⋯ }

@[simp]

theorem SimpleGraph.Hom.mapDart_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (d : G.Dart) : f.mapDart d = { toProd := Prod.map (⇑f) (⇑f) d.toProd, adj := ⋯ }

def SimpleGraph.Hom.mapSpanningSubgraphs {V : Type u_1} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') : G →g G'

The induced map for spanning subgraphs, which is the identity on vertices.

Equations

• SimpleGraph.Hom.mapSpanningSubgraphs h = { toFun := fun (x : V) => x, map_rel' := ⋯ }

@[simp]

theorem SimpleGraph.Hom.mapSpanningSubgraphs_apply {V : Type u_1} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') (x : V) : (SimpleGraph.Hom.mapSpanningSubgraphs h) x = x

theorem SimpleGraph.Hom.mapEdgeSet.injective {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (hinj : Function.Injective ⇑f) : Function.Injective f.mapEdgeSet

theorem SimpleGraph.Hom.injective_of_top_hom {V : Type u_1} {W : Type u_2} {G' : SimpleGraph W} (f : ⊤ →g G') : Function.Injective ⇑f

Every graph homomorphism from a complete graph is injective.

def SimpleGraph.Hom.comap {V : Type u_1} {W : Type u_2} (f : V → W) (G : SimpleGraph W) : SimpleGraph.comap f G →g G

There is a homomorphism to a graph from a comapped graph. When the function is injective, this is an embedding (see SimpleGraph.Embedding.comap).

Equations

• SimpleGraph.Hom.comap f G = { toFun := f, map_rel' := ⋯ }

@[simp]

theorem SimpleGraph.Hom.comap_apply {V : Type u_1} {W : Type u_2} (f : V → W) (G : SimpleGraph W) : ∀ (a : V), (SimpleGraph.Hom.comap f G) a = f a

@[reducible, inline]

abbrev SimpleGraph.Hom.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' →g G'') (f : G →g G') : G →g G''

Composition of graph homomorphisms.

Equations

• f'.comp f = RelHom.comp f' f

@[simp]

theorem SimpleGraph.Hom.coe_comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' →g G'') (f : G →g G') : ⇑(f'.comp f) = ⇑f' ∘ ⇑f

def SimpleGraph.Hom.ofLE {V : Type u_1} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} (h : G₁ ≤ G₂) : G₁ →g G₂

The graph homomorphism from a smaller graph to a bigger one.

Equations

• SimpleGraph.Hom.ofLE h = { toFun := id, map_rel' := h }

@[simp]

theorem SimpleGraph.Hom.coe_ofLE {V : Type u_1} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} (h : G₁ ≤ G₂) : ⇑(SimpleGraph.Hom.ofLE h) = id

@[reducible, inline]

abbrev SimpleGraph.Embedding.refl {V : Type u_1} {G : SimpleGraph V} : G ↪g G

The identity embedding from a graph to itself.

Equations

• SimpleGraph.Embedding.refl = RelEmbedding.refl G.Adj

@[reducible, inline]

abbrev SimpleGraph.Embedding.toHom {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') : G →g G'

An embedding of graphs gives rise to a homomorphism of graphs.

Equations

• f.toHom = RelEmbedding.toRelHom f

@[simp]

theorem SimpleGraph.Embedding.coe_toHom {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ↪g H) : ⇑f.toHom = ⇑f

@[simp]

theorem SimpleGraph.Embedding.map_adj_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') {v : V} {w : V} : G'.Adj (f v) (f w) ↔ G.Adj v w

theorem SimpleGraph.Embedding.map_mem_edgeSet_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') {e : Sym2 V} : Sym2.map (⇑f) e ∈ G'.edgeSet ↔ e ∈ G.edgeSet

theorem SimpleGraph.Embedding.apply_mem_neighborSet_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') {v : V} {w : V} : f w ∈ G'.neighborSet (f v) ↔ w ∈ G.neighborSet v

def SimpleGraph.Embedding.mapEdgeSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') : ↑G.edgeSet ↪ ↑G'.edgeSet

A graph embedding induces an embedding of edge sets.

Equations

• f.mapEdgeSet = { toFun := SimpleGraph.Hom.mapEdgeSet (RelEmbedding.toRelHom f), inj' := ⋯ }

@[simp]

theorem SimpleGraph.Embedding.mapEdgeSet_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') (e : ↑G.edgeSet) : f.mapEdgeSet e = SimpleGraph.Hom.mapEdgeSet (RelEmbedding.toRelHom f) e

def SimpleGraph.Embedding.mapNeighborSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') (v : V) : ↑(G.neighborSet v) ↪ ↑(G'.neighborSet (f v))

A graph embedding induces an embedding of neighbor sets.

Equations

• f.mapNeighborSet v = { toFun := fun (w : ↑(G.neighborSet v)) => ⟨f ↑w, ⋯⟩, inj' := ⋯ }

@[simp]

theorem SimpleGraph.Embedding.mapNeighborSet_apply_coe {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') (v : V) (w : ↑(G.neighborSet v)) : ↑((f.mapNeighborSet v) w) = f ↑w

def SimpleGraph.Embedding.comap {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph W) : SimpleGraph.comap (⇑f) G ↪g G

Given an injective function, there is an embedding from the comapped graph into the original graph.

Equations

• SimpleGraph.Embedding.comap f G = { toEmbedding := f, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.Embedding.comap_apply {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph W) (v : V) : (SimpleGraph.Embedding.comap f G) v = f v

def SimpleGraph.Embedding.map {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) : G ↪g SimpleGraph.map f G

Given an injective function, there is an embedding from a graph into the mapped graph.

Equations

• SimpleGraph.Embedding.map f G = { toEmbedding := f, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.Embedding.map_apply {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) (v : V) : (SimpleGraph.Embedding.map f G) v = f v

@[reducible, inline]

abbrev SimpleGraph.Embedding.induce {V : Type u_1} {G : SimpleGraph V} (s : Set V) : SimpleGraph.induce s G ↪g G

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

• SimpleGraph.Embedding.induce s = SimpleGraph.Embedding.comap (Function.Embedding.subtype fun (x : V) => x ∈ s) G

@[reducible, inline]

abbrev SimpleGraph.Embedding.spanningCoe {V : Type u_1} {s : Set V} (G : SimpleGraph ↑s) : G ↪g G.spanningCoe

Graphs on a set of vertices embed in their spanningCoe.

Equations

• SimpleGraph.Embedding.spanningCoe G = SimpleGraph.Embedding.map (Function.Embedding.subtype fun (x : V) => x ∈ s) G

def SimpleGraph.Embedding.completeGraph {α : Type u_4} {β : Type u_5} (f : α ↪ β) : ⊤ ↪g ⊤

Embeddings of types induce embeddings of complete graphs on those types.

Equations

• SimpleGraph.Embedding.completeGraph f = { toEmbedding := f, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.Embedding.coe_completeGraph {α : Type u_4} {β : Type u_5} (f : α ↪ β) : ⇑(SimpleGraph.Embedding.completeGraph f) = ⇑f

@[reducible, inline]

abbrev SimpleGraph.Embedding.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' ↪g G'') (f : G ↪g G') : G ↪g G''

Composition of graph embeddings.

Equations

• f'.comp f = RelEmbedding.trans f f'

@[simp]

theorem SimpleGraph.Embedding.coe_comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' ↪g G'') (f : G ↪g G') : ⇑(f'.comp f) = ⇑f' ∘ ⇑f

def SimpleGraph.induceHom {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {s : Set V} {t : Set W} (φ : G →g G') (φst : Set.MapsTo (⇑φ) s t) : SimpleGraph.induce s G →g SimpleGraph.induce t G'

The restriction of a morphism of graphs to induced subgraphs.

Equations

• SimpleGraph.induceHom φ φst = { toFun := Set.MapsTo.restrict (⇑φ) s t φst, map_rel' := ⋯ }

@[simp]

theorem SimpleGraph.coe_induceHom {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {s : Set V} {t : Set W} (φ : G →g G') (φst : Set.MapsTo (⇑φ) s t) : ⇑(SimpleGraph.induceHom φ φst) = Set.MapsTo.restrict (⇑φ) s t φst

@[simp]

theorem SimpleGraph.induceHom_id {V : Type u_1} (G : SimpleGraph V) (s : Set V) : SimpleGraph.induceHom SimpleGraph.Hom.id ⋯ = SimpleGraph.Hom.id

@[simp]

theorem SimpleGraph.induceHom_comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} {s : Set V} {t : Set W} {r : Set X} (φ : G →g G') (φst : Set.MapsTo (⇑φ) s t) (ψ : G' →g G'') (ψtr : Set.MapsTo (⇑ψ) t r) : (SimpleGraph.induceHom ψ ψtr).comp (SimpleGraph.induceHom φ φst) = SimpleGraph.induceHom (ψ.comp φ) ⋯

theorem SimpleGraph.induceHom_injective {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {s : Set V} {t : Set W} (φ : G →g G') (φst : Set.MapsTo (⇑φ) s t) (hi : Set.InjOn (⇑φ) s) : Function.Injective ⇑(SimpleGraph.induceHom φ φst)

def SimpleGraph.induceHomOfLE {V : Type u_1} (G : SimpleGraph V) {s : Set V} {s' : Set V} (h : s ≤ s') : SimpleGraph.induce s G ↪g SimpleGraph.induce s' G

Given an inclusion of vertex subsets, the induced embedding on induced graphs. This is not an abbreviation for induceHom since we get an embedding in this case.

Equations

• G.induceHomOfLE h = { toEmbedding := s.embeddingOfSubset s' h, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.induceHomOfLE_apply {V : Type u_1} (G : SimpleGraph V) {s : Set V} {s' : Set V} (h : s ≤ s') (v : ↑s) : (G.induceHomOfLE h) v = Set.inclusion h v

@[simp]

theorem SimpleGraph.induceHomOfLE_toHom {V : Type u_1} (G : SimpleGraph V) {s : Set V} {s' : Set V} (h : s ≤ s') : (G.induceHomOfLE h).toHom = SimpleGraph.induceHom SimpleGraph.Hom.id ⋯

@[reducible, inline]

abbrev SimpleGraph.Iso.refl {V : Type u_1} {G : SimpleGraph V} : G ≃g G

The identity isomorphism of a graph with itself.

Equations

• SimpleGraph.Iso.refl = RelIso.refl G.Adj

@[reducible, inline]

abbrev SimpleGraph.Iso.toEmbedding {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') : G ↪g G'

An isomorphism of graphs gives rise to an embedding of graphs.

Equations

• f.toEmbedding = RelIso.toRelEmbedding f

@[reducible, inline]

abbrev SimpleGraph.Iso.toHom {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') : G →g G'

An isomorphism of graphs gives rise to a homomorphism of graphs.

Equations

• f.toHom = f.toEmbedding.toHom

@[reducible, inline]

abbrev SimpleGraph.Iso.symm {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') : G' ≃g G

The inverse of a graph isomorphism.

Equations

• f.symm = RelIso.symm f

theorem SimpleGraph.Iso.map_adj_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') {v : V} {w : V} : G'.Adj (f v) (f w) ↔ G.Adj v w

theorem SimpleGraph.Iso.map_mem_edgeSet_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') {e : Sym2 V} : Sym2.map (⇑f) e ∈ G'.edgeSet ↔ e ∈ G.edgeSet

theorem SimpleGraph.Iso.apply_mem_neighborSet_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') {v : V} {w : V} : f w ∈ G'.neighborSet (f v) ↔ w ∈ G.neighborSet v

@[simp]

theorem SimpleGraph.Iso.symm_toHom_comp_toHom {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') : f.symm.toHom.comp f.toHom = SimpleGraph.Hom.id

@[simp]

theorem SimpleGraph.Iso.toHom_comp_symm_toHom {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') : f.toHom.comp f.symm.toHom = SimpleGraph.Hom.id

def SimpleGraph.Iso.mapEdgeSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') : ↑G.edgeSet ≃ ↑G'.edgeSet

An isomorphism of graphs induces an equivalence of edge sets.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SimpleGraph.Iso.mapEdgeSet_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (e : ↑G.edgeSet) : f.mapEdgeSet e = SimpleGraph.Hom.mapEdgeSet (RelIso.toRelEmbedding f).toRelHom e

@[simp]

theorem SimpleGraph.Iso.mapEdgeSet_symm_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (e : ↑G'.edgeSet) : f.mapEdgeSet.symm e = SimpleGraph.Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom e

def SimpleGraph.Iso.mapNeighborSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (v : V) : ↑(G.neighborSet v) ≃ ↑(G'.neighborSet (f v))

A graph isomorphism induces an equivalence of neighbor sets.

Equations

• f.mapNeighborSet v = { toFun := fun (w : ↑(G.neighborSet v)) => ⟨f ↑w, ⋯⟩, invFun := fun (w : ↑(G'.neighborSet (f v))) => ⟨f.symm ↑w, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem SimpleGraph.Iso.mapNeighborSet_symm_apply_coe {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (v : V) (w : ↑(G'.neighborSet (f v))) : ↑((f.mapNeighborSet v).symm w) = f.symm ↑w

@[simp]

theorem SimpleGraph.Iso.mapNeighborSet_apply_coe {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (v : V) (w : ↑(G.neighborSet v)) : ↑((f.mapNeighborSet v) w) = f ↑w

theorem SimpleGraph.Iso.card_eq {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') [Fintype V] [Fintype W] : Fintype.card V = Fintype.card W

def SimpleGraph.Iso.comap {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph W) : SimpleGraph.comap (⇑f.toEmbedding) G ≃g G

Given a bijection, there is an embedding from the comapped graph into the original graph.

Equations

• SimpleGraph.Iso.comap f G = { toEquiv := f, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.Iso.comap_apply {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph W) (v : V) : (SimpleGraph.Iso.comap f G) v = f v

@[simp]

theorem SimpleGraph.Iso.comap_symm_apply {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph W) (w : W) : (SimpleGraph.Iso.comap f G).symm w = f.symm w

def SimpleGraph.Iso.map {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph V) : G ≃g SimpleGraph.map f.toEmbedding G

Given an injective function, there is an embedding from a graph into the mapped graph.

Equations

• SimpleGraph.Iso.map f G = { toEquiv := f, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.Iso.map_apply {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph V) (v : V) : (SimpleGraph.Iso.map f G) v = f v

@[simp]

theorem SimpleGraph.Iso.map_symm_apply {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph V) (w : W) : (SimpleGraph.Iso.map f G).symm w = f.symm w

def SimpleGraph.Iso.completeGraph {α : Type u_4} {β : Type u_5} (f : α ≃ β) : ⊤ ≃g ⊤

Equivalences of types induce isomorphisms of complete graphs on those types.

Equations

• SimpleGraph.Iso.completeGraph f = { toEquiv := f, map_rel_iff' := ⋯ }

theorem SimpleGraph.Iso.toEmbedding_completeGraph {α : Type u_4} {β : Type u_5} (f : α ≃ β) : (SimpleGraph.Iso.completeGraph f).toEmbedding = SimpleGraph.Embedding.completeGraph f.toEmbedding

@[reducible, inline]

abbrev SimpleGraph.Iso.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' ≃g G'') (f : G ≃g G') : G ≃g G''

Composition of graph isomorphisms.

Equations

• f'.comp f = RelIso.trans f f'

@[simp]

theorem SimpleGraph.Iso.coe_comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' ≃g G'') (f : G ≃g G') : ⇑(f'.comp f) = ⇑f' ∘ ⇑f

def SimpleGraph.induceUnivIso {V : Type u_1} (G : SimpleGraph V) : SimpleGraph.induce Set.univ G ≃g G

The graph induced on Set.univ is isomorphic to the original graph.

Equations

• G.induceUnivIso = { toEquiv := Equiv.Set.univ V, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.induceUnivIso_apply {V : Type u_1} (G : SimpleGraph V) (self : { x : V // x ∈ Set.univ }) : G.induceUnivIso self = ↑self

@[simp]

theorem SimpleGraph.induceUnivIso_symm_apply_coe {V : Type u_1} (G : SimpleGraph V) (a : V) : ↑((RelIso.symm G.induceUnivIso) a) = a

def SimpleGraph.overFin {V : Type u_1} (G : SimpleGraph V) [Fintype V] {n : ℕ} (hc : Fintype.card V = n) : SimpleGraph (Fin n)

Given a graph over a finite vertex type V and a proof hc that Fintype.card V = n, G.overFin n is an isomorphic (as shown in overFinIso) graph over Fin n.

Equations

• G.overFin hc = { Adj := fun (x y : Fin n) => G.Adj ((Fintype.equivFinOfCardEq hc).symm x) ((Fintype.equivFinOfCardEq hc).symm y), symm := ⋯, loopless := ⋯ }

noncomputable def SimpleGraph.overFinIso {V : Type u_1} (G : SimpleGraph V) [Fintype V] {n : ℕ} (hc : Fintype.card V = n) : G ≃g G.overFin hc

The isomorphism between G and G.overFin hc.

Equations

• G.overFinIso hc = { toEquiv := Fintype.equivFinOfCardEq hc, map_rel_iff' := ⋯ }