Congruences

Content created by Fredrik Bakke, Egbert Rijke, Fernando Chu, Garrett Figueroa, Julian KG, Louis Wasserman, fernabnor and louismntnu.

Created on 2023-03-20.
Last modified on 2025-10-31.

module universal-algebra.congruences where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equivalence-relations
open import foundation.propositions
open import foundation.unit-type
open import foundation.universe-levels

open import lists.tuples

open import universal-algebra.algebraic-theories
open import universal-algebra.algebras
open import universal-algebra.signatures

Idea

A congruence in an algebra of an algebraic theory is an equivalence relation that respects all operations of the algebra.

Definitions

The predicate on an equivalence relation of preserving the operations of an algebra

module _
  {l1 l2 l3 l4 : Level} (σ : signature l1)
  (T : Algebraic-Theory l2 σ) (A : Algebra l3 σ T)
  (R : equivalence-relation l4 (type-Algebra σ T A))
  where

  relation-holds-for-all-tuples-equivalence-relation-Algebra :
    {n : ℕ} →
    (v : tuple (type-Algebra σ T A) n) →
    (v' : tuple (type-Algebra σ T A) n) →
    UU l4
  relation-holds-for-all-tuples-equivalence-relation-Algebra
    { .zero-ℕ} empty-tuple empty-tuple =
    raise-unit l4
  relation-holds-for-all-tuples-equivalence-relation-Algebra
    { .(succ-ℕ _)} (x ∷ v) (x' ∷ v') =
    ( sim-equivalence-relation R x x') ×
    ( relation-holds-for-all-tuples-equivalence-relation-Algebra v v')

  preserves-operations-equivalence-relation-Algebra :
    UU (l1 ⊔ l3 ⊔ l4)
  preserves-operations-equivalence-relation-Algebra =
    ( op : operation-signature σ) →
    ( v : tuple (type-Algebra σ T A) (arity-operation-signature σ op)) →
    ( v' : tuple (type-Algebra σ T A) (arity-operation-signature σ op)) →
    relation-holds-for-all-tuples-equivalence-relation-Algebra v v' →
    sim-equivalence-relation R
      ( is-model-set-Algebra σ T A op v)
      ( is-model-set-Algebra σ T A op v')

Congruences

congruence-Algebra :
  {l1 l2 l3 : Level} (l4 : Level)
  (σ : signature l1) (T : Algebraic-Theory l2 σ) (A : Algebra l3 σ T) →
  UU (l1 ⊔ l3 ⊔ lsuc l4)
congruence-Algebra l4 σ T A =
  Σ ( equivalence-relation l4 (type-Algebra σ T A))
    ( preserves-operations-equivalence-relation-Algebra σ T A)

module _
  {l1 l2 l3 l4 : Level} (σ : signature l1)
  (T : Algebraic-Theory l2 σ) (A : Algebra l3 σ T)
  (R : congruence-Algebra l4 σ T A)
  where

  equivalence-relation-congruence-Algebra :
    equivalence-relation l4 (type-Algebra σ T A)
  equivalence-relation-congruence-Algebra = pr1 R

  preserves-operations-congruence-Algebra :
    preserves-operations-equivalence-relation-Algebra σ T A
      ( equivalence-relation-congruence-Algebra)
  preserves-operations-congruence-Algebra = pr2 R

Recent changes