Comap of a directed graph

The minimal pullback API for Mathlib's Digraph, mirroring SimpleGraph.comap. A candidate for upstreaming to Mathlib (tracked on issue #24). Only comap is provided — map is unnecessary for restriction consistency and has less canonical behaviour, so it is omitted.

def Digraph.comap {V : Type u_2} {W : Type u_3} (f : V → W) (G : Digraph W) : Digraph V

The comap of a digraph along a function: x and y are adjacent in G.comap f iff f x and f y are adjacent in G.

Equations

• Digraph.comap f G = { Adj := fun (x y : V) => G.Adj (f x) (f y) }

@[simp]

theorem Digraph.comap_adj {V : Type u_2} {W : Type u_3} (f : V → W) (G : Digraph W) (x y : V) : (Digraph.comap f G).Adj x y ↔ G.Adj (f x) (f y)

@[simp]

theorem Digraph.comap_id {V : Type u_2} (G : Digraph V) : Digraph.comap id G = G

@[simp]

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

@[implicit_reducible]

instance Digraph.decidableRelComap {V : Type u_2} {W : Type u_3} (f : V → W) (G : Digraph W) [DecidableRel G.Adj] : DecidableRel (Digraph.comap f G).Adj

Equations

• Digraph.decidableRelComap f G x y = decidable_of_iff (G.Adj (f x) (f y)) ⋯