Quotient algebras

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-09-05.

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

open import foundation.dependent-pair-types
open import foundation.equivalence-classes
open import foundation.equivalence-relations
open import foundation.equivalences
open import foundation.finite-sequences-set-quotients
open import foundation.functoriality-propositional-truncation
open import foundation.multivariable-functoriality-set-quotients
open import foundation.multivariable-operations
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.set-quotients
open import foundation.sets
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-of-theories
open import universal-algebra.congruences
open import universal-algebra.models-of-signatures
open import universal-algebra.signatures

Idea

The quotient of an algebra by a congruence is the set quotient by that congruence. This quotient again has the structure of an algebra inherited by the original one.

Definitions

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

  set-quotient-Algebra : Set (l3 ⊔ l4)
  set-quotient-Algebra =
    quotient-Set (equivalence-relation-congruence-Algebra σ T A R)

  type-quotient-Algebra : UU (l3 ⊔ l4)
  type-quotient-Algebra = pr1 set-quotient-Algebra

  is-set-set-quotient-Algebra : is-set type-quotient-Algebra
  is-set-set-quotient-Algebra = pr2 set-quotient-Algebra

  compute-quotient-Algebra :
    equivalence-class
      (equivalence-relation-congruence-Algebra σ T A R) ≃
      (type-quotient-Algebra)
  compute-quotient-Algebra =
    compute-set-quotient
      ( equivalence-relation-congruence-Algebra σ T A R)

  set-quotient-equivalence-class-Algebra :
    equivalence-class
      (equivalence-relation-congruence-Algebra σ T A R) →
    type-quotient-Algebra
  set-quotient-equivalence-class-Algebra =
    map-equiv compute-quotient-Algebra

  equivalence-class-set-quotient-Algebra :
    type-quotient-Algebra →
    equivalence-class
      (equivalence-relation-congruence-Algebra σ T A R)
  equivalence-class-set-quotient-Algebra =
    map-inv-equiv compute-quotient-Algebra

  tuple-type-quotient-tuple-type-Algebra :
    {n : ℕ} →
    tuple type-quotient-Algebra n →
    type-trunc-Prop (tuple (type-Algebra σ T A) n)
  tuple-type-quotient-tuple-type-Algebra empty-tuple =
    unit-trunc-Prop empty-tuple
  tuple-type-quotient-tuple-type-Algebra (x ∷ v) =
    map-universal-property-trunc-Prop
      ( trunc-Prop _)
      ( λ (z , p) →
        map-trunc-Prop
          (λ v' → z ∷ v')
          ( tuple-type-quotient-tuple-type-Algebra v))
      ( pr2 (equivalence-class-set-quotient-Algebra x))

  relation-holds-all-tuple-all-sim-equivalence-relation :
    {n : ℕ}
    (v v' : multivariable-input n ( λ _ → type-Algebra σ T A)) →
    (type-Prop
      (prop-equivalence-relation
        (all-sim-equivalence-relation n
          (λ _ → type-Algebra σ T A)
          (λ _ → equivalence-relation-congruence-Algebra σ T A R)) v v')) →
    relation-holds-all-tuple σ T A
      (equivalence-relation-congruence-Algebra σ T A R)
      (tuple-multivariable-input n (type-Algebra σ T A) v)
      (tuple-multivariable-input n (type-Algebra σ T A) v')
  relation-holds-all-tuple-all-sim-equivalence-relation {zero-ℕ} v v' p =
    raise-star
  relation-holds-all-tuple-all-sim-equivalence-relation
    {succ-ℕ n} (x , v) (x' , v') (p , p') =
    p , (relation-holds-all-tuple-all-sim-equivalence-relation v v' p')

  is-model-set-quotient-Algebra :
    is-model-signature σ set-quotient-Algebra
  is-model-set-quotient-Algebra op v =
    multivariable-map-set-quotient
      ( arity-operation-signature σ op)
      ( λ _ → type-Algebra σ T A)
      ( λ _ → equivalence-relation-congruence-Algebra σ T A R)
      ( equivalence-relation-congruence-Algebra σ T A R)
      ( pair
        ( λ v →
          is-model-set-Algebra σ T A op
            ( tuple-multivariable-input
              ( arity-operation-signature σ op)
              ( type-Algebra σ T A)
              ( v)))
        ( λ {v} {v'} p →
          preserves-operations-congruence-Algebra σ T A R op
            ( tuple-multivariable-input
              ( arity-operation-signature σ op)
              ( type-Algebra σ T A)
              ( v))
            ( tuple-multivariable-input
              ( arity-operation-signature σ op)
              ( type-Algebra σ T A)
              ( v'))
            (relation-holds-all-tuple-all-sim-equivalence-relation v v' p)))
      ( multivariable-input-tuple
        ( arity-operation-signature σ op)
        ( type-quotient-Algebra)
        ( v))

Recent changes