---
layout: default
title : "Legacy.Base.Structures.Graphs module"
date : "2021-06-22"
author: "agda-algebras development team"
---

### <a id="graph-structures">Graph Structures</a>

This is the [Legacy.Base.Structures.Graphs][] module of the [Agda Universal Algebra Library][].

N.B. This module differs from 0Graphs.lagda in that this module is universe polymorphic; i.e., we do not restrict universe levels (to, e.g., `β„“β‚€`). This complicates some things; e.g., we must use lift and lower in some places (cf. [Legacy/Base/Structures/Graphs0.lagda][]).

**Definition** (Graph of a structure). Let `𝑨` be an `(𝑅, 𝐹)`-structure (relations from `𝑅` and operations from `𝐹`). The *graph* of `𝑨` is the structure `Gr 𝑨` with the same domain as `𝑨` with relations from `𝑅` together with a (`k+1`)-ary relation symbol `G 𝑓` for each `𝑓 ∈ 𝐹` of arity `k`, which is interpreted in `Gr 𝑨` as all tuples `(t , y) ∈ Aᡏ⁺¹` such that `𝑓 t ≑ y`. (See also Definition 2 of https://arxiv.org/pdf/2010.04958v2.pdf)

```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Legacy.Base.Structures.Graphs where

open import Agda.Primitive  using () renaming  ( Set to Type )

-- imports from Agda and the Agda Standard Library -------------------------------------------
open import Data.Product    using ( _,_ ; Ξ£-syntax ; _Γ—_ )
open import Data.Sum.Base   using ( _⊎_ ) renaming  ( inj₁ to inl ; injβ‚‚ to inr )
open import Data.Unit.Base  using ( ⊀ ; tt )
open import Level           using (  _βŠ”_ ; Level ; Lift ; lift ; lower ) renaming ( 0β„“ to β„“β‚€ )
open import Function.Base   using ( _∘_  )
open import Relation.Binary.PropositionalEquality as ≑
                            using ( _≑_ ; module ≑-Reasoning )

-- Imports from the Agda Universal Algebra Library ---------------------------------------------
open import Overture               using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Legacy.Base.Relations         using ( Rel )
open import Legacy.Base.Structures.Basic  using ( signature ; structure )
open import Legacy.Base.Structures.Homs   using ( hom ; ∘-hom ; is-hom-rel ; is-hom-op)
open import Examples.Structures.Signatures  using ( Sβˆ… )

open signature ; open structure ; open _⊎_

Gr-sig : signature β„“β‚€ β„“β‚€ β†’ signature β„“β‚€ β„“β‚€ β†’ signature β„“β‚€ β„“β‚€

Gr-sig 𝐹 𝑅 = record  { symbol = symbol 𝑅 ⊎ symbol 𝐹
                     ; arity  = ar
                     }
 where
 ar : symbol 𝑅 ⊎ symbol 𝐹 β†’ Type _
 ar (inl π‘Ÿ) = (arity 𝑅) π‘Ÿ
 ar (inr 𝑓) = (arity 𝐹) 𝑓 ⊎ ⊀

private variable
 𝐹 𝑅 : signature β„“β‚€ β„“β‚€
 α ρ : Level

Gr : βˆ€{Ξ± ρ} β†’ structure 𝐹 𝑅 {Ξ±} {ρ} β†’ structure Sβˆ… (Gr-sig 𝐹 𝑅) {Ξ±} {Ξ± βŠ” ρ}
Gr {𝐹}{𝑅}{Ξ±}{ρ} 𝑨 = record { carrier = carrier 𝑨 ; op = Ξ» () ; rel = split }
  where
  split : (s : symbol 𝑅 ⊎ symbol 𝐹) β†’ Rel (carrier 𝑨) (arity (Gr-sig 𝐹 𝑅) s) {Ξ± βŠ” ρ}
  split (inl π‘Ÿ) arg = Lift Ξ± (rel 𝑨 π‘Ÿ arg)
  split (inr 𝑓) args = Lift ρ (op 𝑨 𝑓 (args ∘ inl) ≑ args (inr tt))

open ≑-Reasoning

private variable ρᡃ Ξ² ρᡇ : Level

module _ {𝑨 : structure 𝐹 𝑅 {Ξ±} {ρᡃ}} {𝑩 : structure 𝐹 𝑅 {Ξ²} {ρᡇ}} where

 homβ†’Grhom : hom 𝑨 𝑩 β†’ hom (Gr 𝑨) (Gr 𝑩)
 hom→Grhom (h , hhom) = h , (i , ii)
  where
  i : is-hom-rel (Gr 𝑨) (Gr 𝑩) h
  i (inl π‘Ÿ) a x = lift (∣ hhom ∣ π‘Ÿ a (lower x))
  i (inr 𝑓) a x = lift goal
   where
   homop : h (op 𝑨 𝑓 (a ∘ inl)) ≑ op 𝑩 𝑓 (h ∘ (a ∘ inl))
   homop = βˆ₯ hhom βˆ₯ 𝑓 (a ∘ inl)

   goal : op 𝑩 𝑓 (h ∘ (a ∘ inl)) ≑ h (a (inr tt))
   goal =  op 𝑩 𝑓 (h ∘ (a ∘ inl))  β‰‘βŸ¨ ≑.sym homop ⟩
           h (op 𝑨 𝑓 (a ∘ inl))    β‰‘βŸ¨ ≑.cong h (lower x) ⟩
           h (a (inr tt))          ∎

  ii : is-hom-op (Gr 𝑨) (Gr 𝑩) h
  ii = Ξ» ()

 Grhomβ†’hom : hom (Gr 𝑨) (Gr 𝑩) β†’ hom 𝑨 𝑩
 Grhom→hom (h , hhom) = h , (i , ii)
  where
  i : is-hom-rel 𝑨 𝑩 h
  i R a x = lower (∣ hhom ∣ (inl R) a (lift x))
  ii : is-hom-op 𝑨 𝑩 h
  ii f a = goal
   where
   split : arity 𝐹 f ⊎ ⊀ β†’ carrier 𝑨
   split (inl x) = a x
   split (inr y) = op 𝑨 f a
   goal : h (op 𝑨 f a) ≑ op 𝑩 f (Ξ» x β†’ h (a x))
   goal = ≑.sym (lower (∣ hhom ∣ (inr f) split (lift ≑.refl)))
```

**Lemma III.1**. Let `𝑆` be a signature and `𝑨` be an `𝑆`-structure.
Let `β„°` be a finite set of identities such that `𝑨 ⊧ β„°`. For every
instance `𝑿` of CSP(`𝑨`), one can compute in polynomial time an
instance `𝒀` of CSP(`𝑨`) such that `𝒀 ⊧ β„°` and `| hom 𝑿 𝑨 | = | hom 𝒀 𝑨 |`.

**Proof**. `βˆ€ s β‰ˆ t` in `β„°` and each tuple `b` such that `𝑩 ⟦ s ⟧ b β‰’ 𝑩 ⟦ t ⟧ b`, one can compute
the congruence `ΞΈ = Cg (𝑩 ⟦ s ⟧ b , 𝑩 ⟦ t ⟧ b)` generated by `𝑩 ⟦ s ⟧ b` and `𝑩 ⟦ t ⟧ b`.
Let `𝑩₁ := 𝑩 / ΞΈ`, and note that `| 𝑩₁ | < | 𝑩 |`.

We show there exists a bijection from `hom 𝑩 𝑨` to `hom 𝑩₁ 𝑨`.
Fix an `h : hom 𝑩 𝑨`. For all `s β‰ˆ t` in `β„°`, we have

`h (𝑩 ⟦ s ⟧ b) = 𝑨 ⟦ s ⟧ (h b) = 𝑨 ⟦ t ⟧ (h b) = h (𝑩 ⟦ t ⟧ b)`.

Therefore, `ΞΈ βŠ† ker h`, so `h` factors uniquely as `h = h' ∘ Ο€ : 𝑩 β†’ (𝑩 / ΞΈ) β†’ 𝑨`,
where `Ο€` is the canonical projection onto `𝑩 / ΞΈ`.

Thus the mapping `Ο† : hom 𝑩 𝑨 β†’ hom 𝑩₁ 𝑨` that takes each `h` to `h'` such that `h = h' ∘ Ο€`
is injective.  It is also surjective since each `g' : 𝑩 / ΞΈ β†’ 𝑨` is mapped back to
a `g : 𝑩 β†’ 𝑨` such that `g = g' ∘ Ο€`. Iterating over all identities in `β„°`, possibly
several times, at the final step we obtain a structure `𝑩ₙ` that satisfies `β„°`
and is such that `∣ hom 𝑩 𝑨 ∣ = ∣ hom 𝑩ₙ 𝑨 ∣`. Moreover, since the number of elements
in the intermediate structures decreases at each step, `| π‘©α΅’β‚Šβ‚ | < | 𝑩ᡒ |`, the process
finishes in time that is bounded by a polynomial in the size of `𝑩`.

```agda
record _⇛_β‡š_ (𝑩 𝑨 π‘ͺ : structure 𝐹 𝑅) : Type β„“β‚€ where
 field
  to   : hom 𝑩 𝑨 β†’ hom π‘ͺ 𝑨
  from : hom π‘ͺ 𝑨 β†’ hom 𝑩 𝑨
  to∼from : βˆ€ h β†’ (to ∘ from) h ≑ h
  from∼to : βˆ€ h β†’ (from ∘ to) h ≑ h

 -- TODO: formalize Lemma III.1
 -- module _ {Ο‡ : Level}{X : Type Ο‡}
 --          {𝑨 : structure 𝐹 𝑅 {β„“β‚€} {β„“β‚€}} where
 -- LEMMAIII1 : {n : β„•}(β„° : Fin n β†’ (Term X Γ— Term X))(𝑨 ∈ fMod β„°)
 --  β†’          βˆ€(𝑩 : structure 𝐹 𝑅) β†’ Ξ£[ π‘ͺ ∈ structure 𝐹 𝑅 ] (π‘ͺ ∈ fMod β„° Γ— (𝑩 ⇛ 𝑨 β‡š π‘ͺ))
 -- LEMMAIII1 β„° π‘¨βŠ§β„° 𝑩 = {!!} , {!!}
```