Kernels of homomorphisms of algebras
Content created by Fredrik Bakke, Egbert Rijke, Fernando Chu, Julian KG, fernabnor and louismntnu.
Created on 2023-03-28.
Last modified on 2023-06-25.
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.universe-levels open import linear-algebra.functoriality-vectors open import linear-algebra.vectors open import universal-algebra.algebraic-theories open import universal-algebra.algebras-of-theories 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 : Level} ( Sg : signature l1) { l2 : Level} ( Th : Theory Sg l2) { l3 l4 : Level} ( Alg1 : Algebra Sg Th l3) ( Alg2 : Algebra Sg Th l4) ( F : type-hom-Algebra Sg Th Alg1 Alg2) where rel-prop-kernel-hom-Algebra : Relation-Prop l4 (type-Algebra Sg Th Alg1) pr1 (rel-prop-kernel-hom-Algebra x y) = map-hom-Algebra Sg Th Alg1 Alg2 F x = map-hom-Algebra Sg Th Alg1 Alg2 F y pr2 (rel-prop-kernel-hom-Algebra x y) = is-set-Algebra Sg Th Alg2 _ _ eq-rel-kernel-hom-Algebra : Equivalence-Relation l4 (type-Algebra Sg Th Alg1) pr1 eq-rel-kernel-hom-Algebra = rel-prop-kernel-hom-Algebra pr1 (pr2 eq-rel-kernel-hom-Algebra) _ = refl pr1 (pr2 (pr2 eq-rel-kernel-hom-Algebra)) _ _ = inv pr2 (pr2 (pr2 eq-rel-kernel-hom-Algebra)) _ _ _ f g = g ∙ f kernel-hom-Algebra : congruence-Algebra Sg Th Alg1 l4 pr1 kernel-hom-Algebra = eq-rel-kernel-hom-Algebra pr2 kernel-hom-Algebra op v v' p = equational-reasoning f (is-model-set-Algebra Sg Th Alg1 op v) = is-model-set-Algebra Sg Th Alg2 op (map-vec f v) by preserves-operations-hom-Algebra Sg Th Alg1 Alg2 F op v = is-model-set-Algebra Sg Th Alg2 op (map-vec f v') by ap ( is-model-set-Algebra Sg Th Alg2 op) ( map-hom-Algebra-lemma (pr2 Sg op) v v' p) = f (is-model-set-Algebra Sg Th Alg1 op v') by inv (preserves-operations-hom-Algebra Sg Th Alg1 Alg2 F op v') where f = map-hom-Algebra Sg Th Alg1 Alg2 F map-hom-Algebra-lemma : ( n : ℕ) → ( v v' : vec (type-Algebra Sg Th Alg1) n) → ( relation-holds-all-vec Sg Th Alg1 eq-rel-kernel-hom-Algebra v v') → (map-vec f v) = (map-vec f v') map-hom-Algebra-lemma zero-ℕ empty-vec empty-vec 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')
Recent changes
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-05-28. Fredrik Bakke. Enforce even indentation and automate some conventions (#635).
- 2023-05-06. Egbert Rijke. Big cleanup throughout library (#594).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).