# 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 : ) :

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
• = { Adj := Relation.Map G.Adj f f, symm := , loopless := }
Instances For
instance SimpleGraph.instDecidableMapAdj {V : Type u_1} {W : Type u_2} (G : ) {f : V W} {a : W} {b : W} [Decidable (Relation.Map G.Adj (f) (f) a b)] :
Decidable (().Adj a b)
Equations
• G.instDecidableMapAdj = inst
@[simp]
theorem SimpleGraph.map_adj {V : Type u_1} {W : Type u_2} (f : V W) (G : ) (u : W) (v : W) :
().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 : } {f : V W} {a : V} {b : V} :
().Adj (f a) (f b) G.Adj a b
theorem SimpleGraph.map_monotone {V : Type u_1} {W : Type u_2} (f : V W) :
@[simp]
theorem SimpleGraph.map_id {V : Type u_1} (G : ) :
@[simp]
theorem SimpleGraph.map_map {V : Type u_1} {W : Type u_2} {X : Type u_3} (G : ) (f : V W) (g : W X) :
= SimpleGraph.map (f.trans g) G
def SimpleGraph.comap {V : Type u_1} {W : Type u_2} (f : VW) (G : ) :

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
• = { Adj := fun (u v : V) => G.Adj (f u) (f v), symm := , loopless := }
Instances For
@[simp]
theorem SimpleGraph.comap_adj {V : Type u_1} {W : Type u_2} {u : V} {v : V} {G : } {f : VW} :
().Adj u v G.Adj (f u) (f v)
@[simp]
theorem SimpleGraph.comap_id {V : Type u_1} {G : } :
= G
@[simp]
theorem SimpleGraph.comap_comap {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : } (f : VW) (g : WX) :
instance SimpleGraph.instDecidableComapAdj {V : Type u_1} {W : Type u_2} (f : VW) (G : ) [DecidableRel G.Adj] :
Equations
• = inst (f x✝) (f x)
theorem SimpleGraph.comap_symm {V : Type u_1} {W : Type u_2} (G : ) (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 : ) (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) :
@[simp]
theorem SimpleGraph.comap_map_eq {V : Type u_1} {W : Type u_2} (f : V W) (G : ) :
SimpleGraph.comap (f) () = G
theorem SimpleGraph.leftInverse_comap_map {V : Type u_1} {W : Type u_2} (f : V W) :
theorem SimpleGraph.map_injective {V : Type u_1} {W : Type u_2} (f : V W) :
theorem SimpleGraph.comap_surjective {V : Type u_1} {W : Type u_2} (f : V W) :
theorem SimpleGraph.map_le_iff_le_comap {V : Type u_1} {W : Type u_2} (f : V W) (G : ) (G' : ) :
G' G SimpleGraph.comap (f) G'
theorem SimpleGraph.map_comap_le {V : Type u_1} {W : Type u_2} (f : V W) (G : ) :
theorem SimpleGraph.le_comap_of_subsingleton {V : Type u_1} {W : Type u_2} (G : ) (G' : ) (f : VW) [] :
G
theorem SimpleGraph.map_le_of_subsingleton {V : Type u_1} {W : Type u_2} (G : ) (G' : ) (f : V W) [] :
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
Instances For
@[simp]
theorem Equiv.simpleGraph_apply {V : Type u_1} {W : Type u_2} (e : V W) (G : ) :
e.simpleGraph G = SimpleGraph.comap (e.symm) G
def Equiv.simpleGraph {V : Type u_1} {W : Type u_2} (e : V W) :

Equivalent types have equivalent simple graphs.

Equations
• e.simpleGraph = { toFun := SimpleGraph.comap e.symm, invFun := , left_inv := , right_inv := }
Instances For
@[simp]
theorem Equiv.simpleGraph_refl {V : Type u_1} :
().simpleGraph =
@[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 : ) :

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
Instances For
@[simp]
theorem SimpleGraph.induce_singleton_eq_top {V : Type u_1} (G : ) (v : V) :
@[reducible, inline]
abbrev SimpleGraph.spanningCoe {V : Type u_1} {s : Set V} (G : ) :

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
Instances For
theorem SimpleGraph.induce_spanningCoe {V : Type u_1} {s : Set V} {G : } :
SimpleGraph.induce s G.spanningCoe = G
theorem SimpleGraph.spanningCoe_induce_le {V : Type u_1} (G : ) (s : Set V) :
().spanningCoe G

## Homomorphisms, embeddings and isomorphisms #

@[reducible, inline]
abbrev SimpleGraph.Hom {V : Type u_1} {W : Type u_2} (G : ) (G' : ) :
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
Instances For
@[reducible, inline]
abbrev SimpleGraph.Embedding {V : Type u_1} {W : Type u_2} (G : ) (G' : ) :
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
Instances For
@[reducible, inline]
abbrev SimpleGraph.Iso {V : Type u_1} {W : Type u_2} (G : ) (G' : ) :
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
Instances For

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
Instances For

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
Instances For

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
Instances For
@[reducible, inline]
abbrev SimpleGraph.Hom.id {V : Type u_1} {G : } :
G →g G

The identity homomorphism from a graph to itself.

Equations
Instances For
@[simp]
theorem SimpleGraph.Hom.coe_id {V : Type u_1} {G : } :
SimpleGraph.Hom.id = id
instance SimpleGraph.Hom.instSubsingletonOfForall {V : Type u_1} {W : Type u_2} {G : } {H : } [Subsingleton (VW)] :
Equations
• =
instance SimpleGraph.Hom.instUniqueOfIsEmpty {V : Type u_1} {W : Type u_2} {G : } {H : } [] :
Unique (G →g H)
Equations
• SimpleGraph.Hom.instUniqueOfIsEmpty = { default := { toFun := fun (a : V) => , map_rel' := }, uniq := }
instance SimpleGraph.Hom.instFintype {V : Type u_1} {W : Type u_2} {G : } {H : } [] [] [] [DecidableRel G.Adj] [DecidableRel H.Adj] :
Equations
• One or more equations did not get rendered due to their size.
instance SimpleGraph.Hom.instFinite {V : Type u_1} {W : Type u_2} {G : } {H : } [] [] :
Finite (G →g H)
Equations
• =
theorem SimpleGraph.Hom.map_adj {V : Type u_1} {W : Type u_2} {G : } {G' : } (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 : } {G' : } (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 : } {G' : } (f : G →g G') {v : V} {w : V} (h : w G.neighborSet v) :
f w G'.neighborSet (f v)
@[simp]
theorem SimpleGraph.Hom.mapEdgeSet_coe {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G →g G') (e : G.edgeSet) :
(f.mapEdgeSet e) = Sym2.map f e
def SimpleGraph.Hom.mapEdgeSet {V : Type u_1} {W : Type u_2} {G : } {G' : } (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,
Instances For
@[simp]
theorem SimpleGraph.Hom.mapNeighborSet_coe {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G →g G') (v : V) (w : (G.neighborSet v)) :
(f.mapNeighborSet v w) = f w
def SimpleGraph.Hom.mapNeighborSet {V : Type u_1} {W : Type u_2} {G : } {G' : } (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,
Instances For
def SimpleGraph.Hom.mapDart {V : Type u_1} {W : Type u_2} {G : } {G' : } (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 := }
Instances For
@[simp]
theorem SimpleGraph.Hom.mapDart_apply {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G →g G') (d : G.Dart) :
f.mapDart d = { toProd := Prod.map (f) (f) d.toProd, adj := }
@[simp]
theorem SimpleGraph.Hom.mapSpanningSubgraphs_apply {V : Type u_1} {G : } {G' : } (h : G G') (x : V) :
def SimpleGraph.Hom.mapSpanningSubgraphs {V : Type u_1} {G : } {G' : } (h : G G') :
G →g G'

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

Equations
• = { toFun := fun (x : V) => x, map_rel' := }
Instances For
theorem SimpleGraph.Hom.mapEdgeSet.injective {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G →g G') (hinj : ) :
Function.Injective f.mapEdgeSet
theorem SimpleGraph.Hom.injective_of_top_hom {V : Type u_1} {W : Type u_2} {G' : } (f : →g G') :

Every graph homomorphism from a complete graph is injective.

@[simp]
theorem SimpleGraph.Hom.comap_apply {V : Type u_1} {W : Type u_2} (f : VW) (G : ) :
∀ (a : V), () a = f a
def SimpleGraph.Hom.comap {V : Type u_1} {W : Type u_2} (f : VW) (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
• = { toFun := f, map_rel' := }
Instances For
@[reducible, inline]
abbrev SimpleGraph.Hom.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : } {G' : } {G'' : } (f' : G' →g G'') (f : G →g G') :
G →g G''

Composition of graph homomorphisms.

Equations
Instances For
@[simp]
theorem SimpleGraph.Hom.coe_comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : } {G' : } {G'' : } (f' : G' →g G'') (f : G →g G') :
(f'.comp f) = f' f
def SimpleGraph.Hom.ofLE {V : Type u_1} {G₁ : } {G₂ : } (h : G₁ G₂) :
G₁ →g G₂

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

Equations
• = { toFun := id, map_rel' := h }
Instances For
@[simp]
theorem SimpleGraph.Hom.coe_ofLE {V : Type u_1} {G₁ : } {G₂ : } (h : G₁ G₂) :
= id
@[reducible, inline]
abbrev SimpleGraph.Embedding.refl {V : Type u_1} {G : } :
G ↪g G

The identity embedding from a graph to itself.

Equations
Instances For
@[reducible, inline]
abbrev SimpleGraph.Embedding.toHom {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G ↪g G') :
G →g G'

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

Equations
• f.toHom =
Instances For
@[simp]
theorem SimpleGraph.Embedding.coe_toHom {V : Type u_1} {W : Type u_2} {G : } {H : } (f : G ↪g H) :
f.toHom = f
@[simp]
theorem SimpleGraph.Embedding.map_adj_iff {V : Type u_1} {W : Type u_2} {G : } {G' : } (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 : } {G' : } (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 : } {G' : } (f : G ↪g G') {v : V} {w : V} :
f w G'.neighborSet (f v) w G.neighborSet v
@[simp]
theorem SimpleGraph.Embedding.mapEdgeSet_apply {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G ↪g G') (e : G.edgeSet) :
f.mapEdgeSet e =
def SimpleGraph.Embedding.mapEdgeSet {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G ↪g G') :
G.edgeSet G'.edgeSet

A graph embedding induces an embedding of edge sets.

Equations
• f.mapEdgeSet = { toFun := , inj' := }
Instances For
@[simp]
theorem SimpleGraph.Embedding.mapNeighborSet_apply_coe {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G ↪g G') (v : V) (w : (G.neighborSet v)) :
((f.mapNeighborSet v) w) = f w
def SimpleGraph.Embedding.mapNeighborSet {V : Type u_1} {W : Type u_2} {G : } {G' : } (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' := }
Instances For
def SimpleGraph.Embedding.comap {V : Type u_1} {W : Type u_2} (f : V W) (G : ) :

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

Equations
• = { toEmbedding := f, map_rel_iff' := }
Instances For
@[simp]
theorem SimpleGraph.Embedding.comap_apply {V : Type u_1} {W : Type u_2} (f : V W) (G : ) (v : V) :
v = f v
def SimpleGraph.Embedding.map {V : Type u_1} {W : Type u_2} (f : V W) (G : ) :
G ↪g

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

Equations
• = { toEmbedding := f, map_rel_iff' := }
Instances For
@[simp]
theorem SimpleGraph.Embedding.map_apply {V : Type u_1} {W : Type u_2} (f : V W) (G : ) (v : V) :
v = f v
@[reducible, inline]
abbrev SimpleGraph.Embedding.induce {V : Type u_1} {G : } (s : Set V) :
↪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
Instances For
@[reducible, inline]
abbrev SimpleGraph.Embedding.spanningCoe {V : Type u_1} {s : Set V} (G : ) :
G ↪g G.spanningCoe

Graphs on a set of vertices embed in their spanningCoe.

Equations
Instances For
def SimpleGraph.Embedding.completeGraph {α : Type u_4} {β : Type u_5} (f : α β) :

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

Equations
• = { toEmbedding := f, map_rel_iff' := }
Instances For
@[simp]
theorem SimpleGraph.Embedding.coe_completeGraph {α : Type u_4} {β : Type u_5} (f : α β) :
@[reducible, inline]
abbrev SimpleGraph.Embedding.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : } {G' : } {G'' : } (f' : G' ↪g G'') (f : G ↪g G') :
G ↪g G''

Composition of graph embeddings.

Equations
• f'.comp f =
Instances For
@[simp]
theorem SimpleGraph.Embedding.coe_comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : } {G' : } {G'' : } (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 : } {G' : } {s : Set V} {t : Set W} (φ : G →g G') (φst : Set.MapsTo (φ) s t) :

The restriction of a morphism of graphs to induced subgraphs.

Equations
Instances For
@[simp]
theorem SimpleGraph.coe_induceHom {V : Type u_1} {W : Type u_2} {G : } {G' : } {s : Set V} {t : Set W} (φ : G →g G') (φst : Set.MapsTo (φ) s t) :
() = Set.MapsTo.restrict (φ) s t φst
@[simp]
theorem SimpleGraph.induceHom_id {V : Type u_1} (G : ) (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 : } {G' : } {G'' : } {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) :
().comp () = SimpleGraph.induceHom (ψ.comp φ)
theorem SimpleGraph.induceHom_injective {V : Type u_1} {W : Type u_2} {G : } {G' : } {s : Set V} {t : Set W} (φ : G →g G') (φst : Set.MapsTo (φ) s t) (hi : Set.InjOn (φ) s) :
def SimpleGraph.induceHomOfLE {V : Type u_1} (G : ) {s : Set V} {s' : Set V} (h : s s') :

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' := }
Instances For
@[simp]
theorem SimpleGraph.induceHomOfLE_apply {V : Type u_1} (G : ) {s : Set V} {s' : Set V} (h : s s') (v : s) :
(G.induceHomOfLE h) v =
@[simp]
theorem SimpleGraph.induceHomOfLE_toHom {V : Type u_1} (G : ) {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 : } :
G ≃g G

The identity isomorphism of a graph with itself.

Equations
Instances For
@[reducible, inline]
abbrev SimpleGraph.Iso.toEmbedding {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G ≃g G') :
G ↪g G'

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

Equations
• f.toEmbedding =
Instances For
@[reducible, inline]
abbrev SimpleGraph.Iso.toHom {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G ≃g G') :
G →g G'

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

Equations
• f.toHom = f.toEmbedding.toHom
Instances For
@[reducible, inline]
abbrev SimpleGraph.Iso.symm {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G ≃g G') :
G' ≃g G

The inverse of a graph isomorphism.

Equations
• f.symm =
Instances For
theorem SimpleGraph.Iso.map_adj_iff {V : Type u_1} {W : Type u_2} {G : } {G' : } (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 : } {G' : } (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 : } {G' : } (f : G ≃g G') {v : V} {w : V} :
f w G'.neighborSet (f v) w G.neighborSet v
@[simp]
theorem SimpleGraph.Iso.mapEdgeSet_apply {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G ≃g G') (e : G.edgeSet) :
f.mapEdgeSet e = SimpleGraph.Hom.mapEdgeSet .toRelHom e
@[simp]
theorem SimpleGraph.Iso.mapEdgeSet_symm_apply {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G ≃g G') (e : G'.edgeSet) :
f.mapEdgeSet.symm e = SimpleGraph.Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom e
def SimpleGraph.Iso.mapEdgeSet {V : Type u_1} {W : Type u_2} {G : } {G' : } (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.
Instances For
@[simp]
theorem SimpleGraph.Iso.mapNeighborSet_symm_apply_coe {V : Type u_1} {W : Type u_2} {G : } {G' : } (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 : } {G' : } (f : G ≃g G') (v : V) (w : (G.neighborSet v)) :
((f.mapNeighborSet v) w) = f w
def SimpleGraph.Iso.mapNeighborSet {V : Type u_1} {W : Type u_2} {G : } {G' : } (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 := }
Instances For
theorem SimpleGraph.Iso.card_eq {V : Type u_1} {W : Type u_2} {G : } {G' : } (f : G ≃g G') [] [] :
def SimpleGraph.Iso.comap {V : Type u_1} {W : Type u_2} (f : V W) (G : ) :
SimpleGraph.comap (f.toEmbedding) G ≃g G

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

Equations
• = { toEquiv := f, map_rel_iff' := }
Instances For
@[simp]
theorem SimpleGraph.Iso.comap_apply {V : Type u_1} {W : Type u_2} (f : V W) (G : ) (v : V) :
() v = f v
@[simp]
theorem SimpleGraph.Iso.comap_symm_apply {V : Type u_1} {W : Type u_2} (f : V W) (G : ) (w : W) :
().symm w = f.symm w
def SimpleGraph.Iso.map {V : Type u_1} {W : Type u_2} (f : V W) (G : ) :
G ≃g SimpleGraph.map f.toEmbedding G

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

Equations
• = { toEquiv := f, map_rel_iff' := }
Instances For
@[simp]
theorem SimpleGraph.Iso.map_apply {V : Type u_1} {W : Type u_2} (f : V W) (G : ) (v : V) :
() v = f v
@[simp]
theorem SimpleGraph.Iso.map_symm_apply {V : Type u_1} {W : Type u_2} (f : V W) (G : ) (w : W) :
().symm w = f.symm w
def SimpleGraph.Iso.completeGraph {α : Type u_4} {β : Type u_5} (f : α β) :

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

Equations
• = { toEquiv := f, map_rel_iff' := }
Instances For
theorem SimpleGraph.Iso.toEmbedding_completeGraph {α : Type u_4} {β : Type u_5} (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 : } {G' : } {G'' : } (f' : G' ≃g G'') (f : G ≃g G') :
G ≃g G''

Composition of graph isomorphisms.

Equations
Instances For
@[simp]
theorem SimpleGraph.Iso.coe_comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : } {G' : } {G'' : } (f' : G' ≃g G'') (f : G ≃g G') :
(f'.comp f) = f' f
@[simp]
theorem SimpleGraph.induceUnivIso_apply {V : Type u_1} (G : ) (self : { x : V // x Set.univ }) :
G.induceUnivIso self = self
@[simp]
theorem SimpleGraph.induceUnivIso_symm_apply_coe {V : Type u_1} (G : ) (a : V) :
((RelIso.symm G.induceUnivIso) a) = a
def SimpleGraph.induceUnivIso {V : Type u_1} (G : ) :

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

Equations
• G.induceUnivIso = { toEquiv := , map_rel_iff' := }
Instances For
def SimpleGraph.overFin {V : Type u_1} (G : ) [] {n : } (hc : ) :

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 (.symm x) (.symm y), symm := , loopless := }
Instances For
noncomputable def SimpleGraph.overFinIso {V : Type u_1} (G : ) [] {n : } (hc : ) :
G ≃g G.overFin hc

The isomorphism between G and G.overFin hc.

Equations
• G.overFinIso hc = { toEquiv := , map_rel_iff' := }
Instances For