Maps between graphs

This file defines vertex map between graphs Graph α β. Morphisms between graphs will also be defined in this file in the future.

Main definitions

• map: the map on graphs induced by a function on vertices f : α → α'

TODO

• Morphisms between graphs

def Graph.map {α : Type u_1} {α' : Type u_2} {β : Type u_4} (f : α → α') (G : Graph α β) : Graph α' β

Map G : Graph α β to a Graph α' β with the same edge set by applying a function f : α → α' to each vertex. Edges between identified vertices become loops.

Equations

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

@[simp]

theorem Graph.map_isLink {α : Type u_1} {α' : Type u_2} {β : Type u_4} (f : α → α') (G : Graph α β) (e : β) (a✝ a✝¹ : α') : (map f G).IsLink e a✝ a✝¹ = Relation.Map (G.IsLink e) f f a✝ a✝¹

@[simp]

theorem Graph.vertexSet_map {α : Type u_1} {α' : Type u_2} {β : Type u_4} (f : α → α') (G : Graph α β) : (map f G).vertexSet = f '' G.vertexSet

@[simp]

theorem Graph.edgeSet_map {α : Type u_1} {α' : Type u_2} {β : Type u_4} (f : α → α') (G : Graph α β) : (map f G).edgeSet = G.edgeSet

theorem Graph.IsLink.map {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {u v : α} {e : β} (f : α → α') (h : G.IsLink e u v) : (map f G).IsLink e (f u) (f v)

@[simp]

theorem Graph.map_inc {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {e : β} {x : α'} (f : α → α') : (map f G).Inc e x ↔ ∃ (v : α), G.Inc e v ∧ x = f v

theorem Graph.Inc.map {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {v : α} {e : β} (f : α → α') (h : G.Inc e v) : (map f G).Inc e (f v)

@[simp]

theorem Graph.map_isLoopAt {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {e : β} {x : α'} (f : α → α') : (map f G).IsLoopAt e x ↔ ∃ (u : α) (v : α), G.IsLink e u v ∧ f u = x ∧ f v = x

theorem Graph.IsLoopAt.map {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {v : α} {e : β} (f : α → α') (h : G.IsLoopAt e v) : (map f G).IsLoopAt e (f v)

@[simp]

theorem Graph.map_adj {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {x y : α'} (f : α → α') : (map f G).Adj x y ↔ Relation.Map G.Adj f f x y

theorem Graph.Adj.map {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {u v : α} (f : α → α') (h : G.Adj u v) : (map f G).Adj (f u) (f v)

@[simp]

theorem Graph.map_id {α : Type u_1} {β : Type u_4} {G : Graph α β} : map id G = G

@[simp]

theorem Graph.map_map {α : Type u_1} {α' : Type u_2} {α'' : Type u_3} {β : Type u_4} {G : Graph α β} (f : α → α') (f' : α' → α'') : map f' (map f G) = map (f' ∘ f) G

theorem Graph.IsSubgraph.map {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G H : Graph α β} (f : α → α') (h : G ≤ H) : map f G ≤ map f H

theorem Graph.map_mono {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G H : Graph α β} (f : α → α') (h : G ≤ H) : map f G ≤ map f H

Alias of Graph.IsSubgraph.map.

theorem Graph.IsSpanningSubgraph.map {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G H : Graph α β} (f : α → α') (hsle : G ≤s H) : map f G ≤s map f H

theorem Graph.map_eq_of_eqOn {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {f g : α → α'} (h : Set.EqOn f g G.vertexSet) : map f G = map g G