# Faithful morphisms of undirected graphs

Content created by Jonathan Prieto-Cubides, Egbert Rijke and Fredrik Bakke.

Created on 2022-06-15.

module graph-theory.faithful-morphisms-undirected-graphs where

Imports
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.propositions
open import foundation.universe-levels

open import graph-theory.morphisms-undirected-graphs
open import graph-theory.undirected-graphs


## Idea

A faithful morphism of undirected graphs is a morphism f : G → H of undirected graphs such that for each unordered pair p of vertices in G the map

  edge-hom-Undirected-Graph G H f p :
edge-Undirected-Graph G p →
edge-Undirected-Graph H
( unordered-pair-vertices-hom-Undirected-Graph G H f p)


is an embedding.

## Definition

module _
{l1 l2 l3 l4 : Level}
(G : Undirected-Graph l1 l2) (H : Undirected-Graph l3 l4)
where

is-faithful-hom-undirected-graph-Prop :
hom-Undirected-Graph G H → Prop (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l4)
is-faithful-hom-undirected-graph-Prop f =
Π-Prop
( unordered-pair-vertices-Undirected-Graph G)
( λ p → is-emb-Prop (edge-hom-Undirected-Graph G H f p))

is-faithful-hom-Undirected-Graph :
hom-Undirected-Graph G H → UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l4)
is-faithful-hom-Undirected-Graph f =
type-Prop (is-faithful-hom-undirected-graph-Prop f)

is-prop-is-faithful-hom-Undirected-Graph :
(f : hom-Undirected-Graph G H) →
is-prop (is-faithful-hom-Undirected-Graph f)
is-prop-is-faithful-hom-Undirected-Graph f =
is-prop-type-Prop (is-faithful-hom-undirected-graph-Prop f)

faithful-hom-Undirected-Graph : UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
faithful-hom-Undirected-Graph =
Σ (hom-Undirected-Graph G H) is-faithful-hom-Undirected-Graph

module _
{l1 l2 l3 l4 : Level}
(G : Undirected-Graph l1 l2) (H : Undirected-Graph l3 l4)
(f : faithful-hom-Undirected-Graph G H)
where

hom-faithful-hom-Undirected-Graph : hom-Undirected-Graph G H
hom-faithful-hom-Undirected-Graph = pr1 f

is-faithful-faithful-hom-Undirected-Graph :
is-faithful-hom-Undirected-Graph G H hom-faithful-hom-Undirected-Graph
is-faithful-faithful-hom-Undirected-Graph = pr2 f

vertex-faithful-hom-Undirected-Graph :
vertex-Undirected-Graph G → vertex-Undirected-Graph H
vertex-faithful-hom-Undirected-Graph =
vertex-hom-Undirected-Graph G H hom-faithful-hom-Undirected-Graph

unordered-pair-vertices-faithful-hom-Undirected-Graph :
unordered-pair-vertices-Undirected-Graph G →
unordered-pair-vertices-Undirected-Graph H
unordered-pair-vertices-faithful-hom-Undirected-Graph =
unordered-pair-vertices-hom-Undirected-Graph G H
hom-faithful-hom-Undirected-Graph

edge-faithful-hom-Undirected-Graph :
(p : unordered-pair-vertices-Undirected-Graph G) →
edge-Undirected-Graph G p →
edge-Undirected-Graph H
( unordered-pair-vertices-faithful-hom-Undirected-Graph p)
edge-faithful-hom-Undirected-Graph =
edge-hom-Undirected-Graph G H hom-faithful-hom-Undirected-Graph

is-emb-edge-faithful-hom-Undirected-Graph :
(p : unordered-pair-vertices-Undirected-Graph G) →
is-emb (edge-faithful-hom-Undirected-Graph p)
is-emb-edge-faithful-hom-Undirected-Graph =
is-faithful-faithful-hom-Undirected-Graph

emb-edge-faithful-hom-Undirected-Graph :
(p : unordered-pair-vertices-Undirected-Graph G) →
edge-Undirected-Graph G p ↪
edge-Undirected-Graph H
( unordered-pair-vertices-faithful-hom-Undirected-Graph p)
pr1 (emb-edge-faithful-hom-Undirected-Graph p) =
edge-faithful-hom-Undirected-Graph p
pr2 (emb-edge-faithful-hom-Undirected-Graph p) =
is-emb-edge-faithful-hom-Undirected-Graph p