Discrete directed graphs

Content created by Egbert Rijke.

Created on 2024-11-19.
Last modified on 2024-11-19.

module graph-theory.discrete-directed-graphs where
Imports 
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.discrete-binary-relations
open import foundation.empty-types
open import foundation.equivalences
open import foundation.homotopies
open import foundation.retractions
open import foundation.sections
open import foundation.universe-levels

open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.torsorial-type-families

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

Idea

A directed graph G ≐ (V , E) is said to be discrete if it has no edges. In other words, a directed graph is discrete if it is of the form Δ A, where Δ is the left adjoint to the forgetful functor (V , E) ↦ V from directed graphs to types.

Recall that reflexive graphs are said to be discrete if the edge relation is torsorial. The condition that a directed graph is discrete compares to the condition that a reflexive graph is discrete in the sense that in both cases discreteness implies initiality of the edge relation: The empty relation is the initial relation, while the identity relation is the initial reflexive relation.

One may wonder if the torsoriality condition of discreteness shouldn’t directly carry over to the discreteness condition on directed graphs. Indeed, an earlier implementation of discreteness in agda-unimath had this faulty definition. However, this leads to examples that are not typically considered discrete. Consider, for example, the directed graph with V := ℕ the natural numbers and E m n := (m + 1 ＝ n) as in

  0 ---> 1 ---> 2 ---> ⋯.

This directed graph satisfies the condition that the type family E m is torsorial for every m : ℕ, simply because E is a functional correspondence. However, this graph is not considered discrete since it relates distinct vertices.

Definitions

The predicate on graphs of being discrete

module _
  {l1 l2 : Level} (G : Directed-Graph l1 l2)
  where

  is-discrete-prop-Directed-Graph : Prop (l1 ⊔ l2)
  is-discrete-prop-Directed-Graph =
    is-discrete-prop-Relation (edge-Directed-Graph G)

  is-discrete-Directed-Graph : UU (l1 ⊔ l2)
  is-discrete-Directed-Graph =
    is-discrete-Relation (edge-Directed-Graph G)

  is-prop-is-discrete-Directed-Graph :
    is-prop is-discrete-Directed-Graph
  is-prop-is-discrete-Directed-Graph =
    is-prop-is-discrete-Relation (edge-Directed-Graph G)

The standard discrete directed graph

module _
  {l : Level} (A : UU l)
  where

  discrete-Directed-Graph : Directed-Graph l lzero
  pr1 discrete-Directed-Graph = A
  pr2 discrete-Directed-Graph x y = empty

Properties

Morphisms from a standard discrete directed graph are maps into vertices

module _
  {l1 l2 l3 : Level} {A : UU l1} (G : Directed-Graph l1 l2)
  where

  ev-hom-discrete-Directed-Graph :
    hom-Directed-Graph (discrete-Directed-Graph A) G →
    A → vertex-Directed-Graph G
  ev-hom-discrete-Directed-Graph =
    vertex-hom-Directed-Graph (discrete-Directed-Graph _) G

  map-inv-ev-hom-discrete-Directed-Graph :
    (A → vertex-Directed-Graph G) →
    hom-Directed-Graph (discrete-Directed-Graph A) G
  pr1 (map-inv-ev-hom-discrete-Directed-Graph f) = f
  pr2 (map-inv-ev-hom-discrete-Directed-Graph f) x y ()

  is-section-map-inv-ev-hom-discrete-Directed-Graph :
    is-section
      ( ev-hom-discrete-Directed-Graph)
      ( map-inv-ev-hom-discrete-Directed-Graph)
  is-section-map-inv-ev-hom-discrete-Directed-Graph f = refl

  htpy-is-retraction-map-inv-ev-hom-discrete-Directed-Graph :
    (f : hom-Directed-Graph (discrete-Directed-Graph A) G) →
    htpy-hom-Directed-Graph
      ( discrete-Directed-Graph A)
      ( G)
      ( map-inv-ev-hom-discrete-Directed-Graph
        ( ev-hom-discrete-Directed-Graph f))
      ( f)
  pr1 (htpy-is-retraction-map-inv-ev-hom-discrete-Directed-Graph f) =
    refl-htpy
  pr2 (htpy-is-retraction-map-inv-ev-hom-discrete-Directed-Graph f) x y ()

  is-retraction-map-inv-ev-hom-discrete-Directed-Graph :
    is-retraction
      ( ev-hom-discrete-Directed-Graph)
      ( map-inv-ev-hom-discrete-Directed-Graph)
  is-retraction-map-inv-ev-hom-discrete-Directed-Graph f =
    eq-htpy-hom-Directed-Graph
      ( discrete-Directed-Graph A)
      ( G)
      ( map-inv-ev-hom-discrete-Directed-Graph
        ( ev-hom-discrete-Directed-Graph f))
      ( f)
      ( htpy-is-retraction-map-inv-ev-hom-discrete-Directed-Graph f)

  abstract
    is-equiv-ev-hom-discrete-Directed-Graph :
      is-equiv ev-hom-discrete-Directed-Graph
    is-equiv-ev-hom-discrete-Directed-Graph =
      is-equiv-is-invertible
        map-inv-ev-hom-discrete-Directed-Graph
        is-section-map-inv-ev-hom-discrete-Directed-Graph
        is-retraction-map-inv-ev-hom-discrete-Directed-Graph

  ev-equiv-hom-discrete-Directed-Graph :
    hom-Directed-Graph (discrete-Directed-Graph A) G ≃
    (A → vertex-Directed-Graph G)
  pr1 ev-equiv-hom-discrete-Directed-Graph =
    ev-hom-discrete-Directed-Graph
  pr2 ev-equiv-hom-discrete-Directed-Graph =
    is-equiv-ev-hom-discrete-Directed-Graph

See also

Recent changes