Base change of dependent directed graphs

Content created by Egbert Rijke.

Created on 2024-12-03.
Last modified on 2024-12-03.

module graph-theory.base-change-dependent-directed-graphs where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import graph-theory.dependent-directed-graphs
open import graph-theory.directed-graphs
open import graph-theory.morphisms-directed-graphs

Idea

Consider a dependent directed graph B over a directed graph A, and consider a graph homomorphism f : C → A. The base change f*B of B along f is defined by substituting the values of f into B. More precisely, f*B is defined by

  (f*B)₀ c := B₀ (f₀ c)
  (f*B)₁ e := B₁ (f₁ e).

Definitions

Base change of dependent directed graphs

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  {A : Directed-Graph l1 l2}
  (C : Directed-Graph l3 l4) (f : hom-Directed-Graph C A)
  (B : Dependent-Directed-Graph l5 l6 A)
  where

  vertex-base-change-Dependent-Directed-Graph :
    (c : vertex-Directed-Graph C) → UU l5
  vertex-base-change-Dependent-Directed-Graph c =
    vertex-Dependent-Directed-Graph B (vertex-hom-Directed-Graph C A f c)

  edge-base-change-Dependent-Directed-Graph :
    {x y : vertex-Directed-Graph C} (e : edge-Directed-Graph C x y) →
    vertex-base-change-Dependent-Directed-Graph x →
    vertex-base-change-Dependent-Directed-Graph y → UU l6
  edge-base-change-Dependent-Directed-Graph e =
    edge-Dependent-Directed-Graph B (edge-hom-Directed-Graph C A f e)

  base-change-Dependent-Directed-Graph :
    Dependent-Directed-Graph l5 l6 C
  pr1 base-change-Dependent-Directed-Graph =
    vertex-base-change-Dependent-Directed-Graph
  pr2 base-change-Dependent-Directed-Graph _ _ =
    edge-base-change-Dependent-Directed-Graph

Recent changes