Kernels of homomorphisms of algebras

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

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

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

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.equivalence-relations
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import lists.functoriality-tuples
open import lists.tuples

open import universal-algebra.algebraic-theories
open import universal-algebra.algebras
open import universal-algebra.congruences
open import universal-algebra.homomorphisms-of-algebras
open import universal-algebra.signatures

Idea

The kernel of a homomorphism f of algebras is the congruence relation given by x ~ y iff f x ~ f y.

Definitions

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

  sim-kernel-hom-Algebra : Relation l4 (type-Algebra σ T A)
  sim-kernel-hom-Algebra x y =
    map-hom-Algebra σ T A B F x ＝ map-hom-Algebra σ T A B F y

  is-prop-sim-kernel-hom-Algebra :
    (x y : type-Algebra σ T A) → is-prop (sim-kernel-hom-Algebra x y)
  is-prop-sim-kernel-hom-Algebra x y =
    is-set-type-Algebra σ T B
      ( map-hom-Algebra σ T A B F x)
      ( map-hom-Algebra σ T A B F y)

  sim-prop-kernel-hom-Algebra :
    Relation-Prop l4 (type-Algebra σ T A)
  sim-prop-kernel-hom-Algebra x y =
    ( sim-kernel-hom-Algebra x y , is-prop-sim-kernel-hom-Algebra x y)

  equivalence-relation-kernel-hom-Algebra :
    equivalence-relation l4 (type-Algebra σ T A)
  pr1 equivalence-relation-kernel-hom-Algebra =
    sim-prop-kernel-hom-Algebra
  pr1 (pr2 equivalence-relation-kernel-hom-Algebra) _ = refl
  pr1 (pr2 (pr2 equivalence-relation-kernel-hom-Algebra)) _ _ = inv
  pr2 (pr2 (pr2 equivalence-relation-kernel-hom-Algebra)) _ _ _ f g = g ∙ f

  abstract
    preserves-operations-sim-kernel-hom-Algebra :
      preserves-operations-equivalence-relation-Algebra σ T A
        ( equivalence-relation-kernel-hom-Algebra)
    preserves-operations-sim-kernel-hom-Algebra op v v' p =
      equational-reasoning
        f (is-model-set-Algebra σ T A op v)
        ＝ is-model-set-Algebra σ T B op (map-tuple f v)
          by preserves-operations-hom-Algebra σ T A B F op v
        ＝ is-model-set-Algebra σ T B op (map-tuple f v')
          by
            ap
              ( is-model-set-Algebra σ T B op)
              ( map-hom-Algebra-lemma (pr2 σ op) v v' p)
        ＝ f (is-model-set-Algebra σ T A op v')
          by inv (preserves-operations-hom-Algebra σ T A B F op v')
      where
      f : type-Algebra σ T A → type-Algebra σ T B
      f = map-hom-Algebra σ T A B F
      map-hom-Algebra-lemma :
        ( n : ℕ) →
        ( v v' : tuple (type-Algebra σ T A) n) →
        ( relation-holds-for-all-tuples-equivalence-relation-Algebra σ T A
          equivalence-relation-kernel-hom-Algebra v v') →
        (map-tuple f v) ＝ (map-tuple f v')
      map-hom-Algebra-lemma zero-ℕ empty-tuple empty-tuple p =
        refl
      map-hom-Algebra-lemma (succ-ℕ n) (x ∷ v) (x' ∷ v') (p , p') =
        ap-binary (_∷_) p (map-hom-Algebra-lemma n v v' p')

  kernel-hom-Algebra : congruence-Algebra l4 σ T A
  kernel-hom-Algebra =
    ( equivalence-relation-kernel-hom-Algebra ,
      preserves-operations-sim-kernel-hom-Algebra)

Recent changes