Fibers of directed graphs
module graph-theory.fibers-directed-graphs where
Imports
open import foundation.contractible-types open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.equality-dependent-pair-types open import foundation.equivalences open import foundation.homotopies open import foundation.identity-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import graph-theory.directed-graphs open import graph-theory.morphisms-directed-graphs open import graph-theory.walks-directed-graphs open import trees.directed-trees
Idea
Consider a vertex x in a directed graph G. The fiber of G at x is a
directed tree of which the type of nodes consists of vertices y equipped with
a walk w from y to x, and the type of edges from (y , w) to (z , v)
consist of an edge e : y → z such that w ＝ cons e v.
Definitions
The underlying graph of the fiber of G at x
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) (x : vertex-Directed-Graph G) where node-fiber-Directed-Graph : UU (l1 ⊔ l2) node-fiber-Directed-Graph = Σ (vertex-Directed-Graph G) (λ y → walk-Directed-Graph G y x) module _ (u : node-fiber-Directed-Graph) where node-inclusion-fiber-Directed-Graph : vertex-Directed-Graph G node-inclusion-fiber-Directed-Graph = pr1 u walk-node-inclusion-fiber-Directed-Graph : walk-Directed-Graph G node-inclusion-fiber-Directed-Graph x walk-node-inclusion-fiber-Directed-Graph = pr2 u root-fiber-Directed-Graph : node-fiber-Directed-Graph pr1 root-fiber-Directed-Graph = x pr2 root-fiber-Directed-Graph = refl-walk-Directed-Graph is-root-fiber-Directed-Graph : node-fiber-Directed-Graph → UU (l1 ⊔ l2) is-root-fiber-Directed-Graph y = root-fiber-Directed-Graph ＝ y edge-fiber-Directed-Graph : (y z : node-fiber-Directed-Graph) → UU (l1 ⊔ l2) edge-fiber-Directed-Graph y z = Σ ( edge-Directed-Graph G ( node-inclusion-fiber-Directed-Graph y) ( node-inclusion-fiber-Directed-Graph z)) ( λ e → ( walk-node-inclusion-fiber-Directed-Graph y) ＝ ( cons-walk-Directed-Graph e ( walk-node-inclusion-fiber-Directed-Graph z))) module _ (y z : node-fiber-Directed-Graph) (e : edge-fiber-Directed-Graph y z) where edge-inclusion-fiber-Directed-Graph : edge-Directed-Graph G ( node-inclusion-fiber-Directed-Graph y) ( node-inclusion-fiber-Directed-Graph z) edge-inclusion-fiber-Directed-Graph = pr1 e walk-edge-fiber-Directed-Graph : walk-node-inclusion-fiber-Directed-Graph y ＝ cons-walk-Directed-Graph ( edge-inclusion-fiber-Directed-Graph) ( walk-node-inclusion-fiber-Directed-Graph z) walk-edge-fiber-Directed-Graph = pr2 e graph-fiber-Directed-Graph : Directed-Graph (l1 ⊔ l2) (l1 ⊔ l2) pr1 graph-fiber-Directed-Graph = node-fiber-Directed-Graph pr2 graph-fiber-Directed-Graph = edge-fiber-Directed-Graph walk-fiber-Directed-Graph : (y z : node-fiber-Directed-Graph) → UU (l1 ⊔ l2) walk-fiber-Directed-Graph = walk-Directed-Graph graph-fiber-Directed-Graph walk-to-root-fiber-walk-Directed-Graph : (y : vertex-Directed-Graph G) (w : walk-Directed-Graph G y x) → walk-fiber-Directed-Graph (y , w) root-fiber-Directed-Graph walk-to-root-fiber-walk-Directed-Graph y refl-walk-Directed-Graph = refl-walk-Directed-Graph walk-to-root-fiber-walk-Directed-Graph .y ( cons-walk-Directed-Graph {y} {z} e w) = cons-walk-Directed-Graph ( e , refl) ( walk-to-root-fiber-walk-Directed-Graph z w) walk-to-root-fiber-Directed-Graph : (y : node-fiber-Directed-Graph) → walk-fiber-Directed-Graph y root-fiber-Directed-Graph walk-to-root-fiber-Directed-Graph (y , w) = walk-to-root-fiber-walk-Directed-Graph y w inclusion-fiber-Directed-Graph : hom-Directed-Graph graph-fiber-Directed-Graph G pr1 inclusion-fiber-Directed-Graph = node-inclusion-fiber-Directed-Graph pr2 inclusion-fiber-Directed-Graph = edge-inclusion-fiber-Directed-Graph
The fiber of G at x as a directed tree
center-unique-direct-successor-fiber-Directed-Graph : (y : node-fiber-Directed-Graph) → ( is-root-fiber-Directed-Graph y) + ( Σ ( node-fiber-Directed-Graph) ( edge-fiber-Directed-Graph y)) center-unique-direct-successor-fiber-Directed-Graph ( y , refl-walk-Directed-Graph) = inl refl center-unique-direct-successor-fiber-Directed-Graph ( y , cons-walk-Directed-Graph {y} {z} e w) = inr ((z , w) , (e , refl)) contraction-unique-direct-successor-fiber-Directed-Graph : (y : node-fiber-Directed-Graph) → ( p : ( is-root-fiber-Directed-Graph y) + ( Σ ( node-fiber-Directed-Graph) (edge-fiber-Directed-Graph y))) → center-unique-direct-successor-fiber-Directed-Graph y ＝ p contraction-unique-direct-successor-fiber-Directed-Graph ._ (inl refl) = refl contraction-unique-direct-successor-fiber-Directed-Graph ( y , .(cons-walk-Directed-Graph e v)) (inr ((z , v) , e , refl)) = refl unique-direct-successor-fiber-Directed-Graph : unique-direct-successor-Directed-Graph ( graph-fiber-Directed-Graph) ( root-fiber-Directed-Graph) pr1 (unique-direct-successor-fiber-Directed-Graph y) = center-unique-direct-successor-fiber-Directed-Graph y pr2 (unique-direct-successor-fiber-Directed-Graph y) = contraction-unique-direct-successor-fiber-Directed-Graph y is-tree-fiber-Directed-Graph : is-tree-Directed-Graph graph-fiber-Directed-Graph is-tree-fiber-Directed-Graph = is-tree-unique-direct-successor-Directed-Graph graph-fiber-Directed-Graph root-fiber-Directed-Graph unique-direct-successor-fiber-Directed-Graph walk-to-root-fiber-Directed-Graph fiber-Directed-Graph : Directed-Tree (l1 ⊔ l2) (l1 ⊔ l2) pr1 fiber-Directed-Graph = graph-fiber-Directed-Graph pr2 fiber-Directed-Graph = is-tree-fiber-Directed-Graph
Computing the direct predecessors of a node in a fiber
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) (x : vertex-Directed-Graph G) where direct-predecessor-fiber-Directed-Graph : (y : node-fiber-Directed-Graph G x) → UU (l1 ⊔ l2) direct-predecessor-fiber-Directed-Graph = direct-predecessor-Directed-Graph (graph-fiber-Directed-Graph G x) direct-predecessor-inclusion-fiber-Directed-Graph : (y : node-fiber-Directed-Graph G x) → direct-predecessor-fiber-Directed-Graph y → direct-predecessor-Directed-Graph G ( node-inclusion-fiber-Directed-Graph G x y) direct-predecessor-inclusion-fiber-Directed-Graph = direct-predecessor-hom-Directed-Graph ( graph-fiber-Directed-Graph G x) ( G) ( inclusion-fiber-Directed-Graph G x) compute-direct-predecessor-fiber-Directed-Graph : (y : node-fiber-Directed-Graph G x) → direct-predecessor-fiber-Directed-Graph y ≃ direct-predecessor-Directed-Graph G ( node-inclusion-fiber-Directed-Graph G x y) compute-direct-predecessor-fiber-Directed-Graph y = ( right-unit-law-Σ-is-contr (λ (u , e) → is-contr-total-path' _)) ∘e ( interchange-Σ-Σ _) map-compute-direct-predecessor-fiber-Directed-Graph : (y : node-fiber-Directed-Graph G x) → direct-predecessor-fiber-Directed-Graph y → direct-predecessor-Directed-Graph G ( node-inclusion-fiber-Directed-Graph G x y) map-compute-direct-predecessor-fiber-Directed-Graph y = map-equiv (compute-direct-predecessor-fiber-Directed-Graph y) htpy-compute-direct-predecessor-fiber-Directed-Graph : (y : node-fiber-Directed-Graph G x) → direct-predecessor-inclusion-fiber-Directed-Graph y ~ map-compute-direct-predecessor-fiber-Directed-Graph y htpy-compute-direct-predecessor-fiber-Directed-Graph y t = refl inv-compute-direct-predecessor-fiber-Directed-Graph : (y : node-fiber-Directed-Graph G x) → direct-predecessor-Directed-Graph G ( node-inclusion-fiber-Directed-Graph G x y) ≃ direct-predecessor-fiber-Directed-Graph y inv-compute-direct-predecessor-fiber-Directed-Graph y = inv-equiv (compute-direct-predecessor-fiber-Directed-Graph y) Eq-direct-predecessor-fiber-Directed-Graph : (y : node-fiber-Directed-Graph G x) → (u v : direct-predecessor-fiber-Directed-Graph y) → UU (l1 ⊔ l2) Eq-direct-predecessor-fiber-Directed-Graph y u v = Σ ( pr1 (direct-predecessor-inclusion-fiber-Directed-Graph y u) ＝ pr1 (direct-predecessor-inclusion-fiber-Directed-Graph y v)) ( λ p → tr ( λ t → edge-Directed-Graph G t (node-inclusion-fiber-Directed-Graph G x y)) ( p) ( pr2 (direct-predecessor-inclusion-fiber-Directed-Graph y u)) ＝ pr2 (direct-predecessor-inclusion-fiber-Directed-Graph y v)) eq-Eq-direct-predecessor-fiber-Directed-Graph : (y : node-fiber-Directed-Graph G x) → ( u v : direct-predecessor-fiber-Directed-Graph y) → Eq-direct-predecessor-fiber-Directed-Graph y u v → u ＝ v eq-Eq-direct-predecessor-fiber-Directed-Graph y u v p = map-inv-equiv ( equiv-ap (compute-direct-predecessor-fiber-Directed-Graph y) u v) ( eq-pair-Σ' p)