Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

### Homomorphisms of Algebras. Quotient Universal Algebra

by
Malgorzata Korolkiewicz

MML identifier: ALG_1
[ Mizar article, MML identifier index ]

```environ

vocabulary UNIALG_1, UNIALG_2, FINSEQ_1, FUNCT_1, RELAT_1, FINSEQ_4, BOOLE,
CQC_SIM1, GROUP_6, WELLORD1, FINSEQ_2, EQREL_1, FUNCT_2, PARTFUN1,
TARSKI, ZF_REFLE, RELAT_2, ALG_1;
notation TARSKI, XBOOLE_0, SUBSET_1, NAT_1, RELAT_1, RELAT_2, RELSET_1,
FUNCT_1, STRUCT_0, FINSEQ_1, PARTFUN1, EQREL_1, FINSEQ_2, FUNCT_2,
TOPREAL1, UNIALG_1, FINSEQOP, UNIALG_2;
constructors RELAT_2, EQREL_1, UNIALG_2, FINSEQOP, MEMBERED, XBOOLE_0;
clusters UNIALG_1, UNIALG_2, RELSET_1, STRUCT_0, FINSEQ_2, PARTFUN1, SUBSET_1,
ARYTM_3, FILTER_1, MEMBERED, ZFMISC_1, FUNCT_1, FUNCT_2, XBOOLE_0;
requirements BOOLE, SUBSET;

begin

reserve U1,U2,U3 for Universal_Algebra,
n,m for Nat,
o1 for operation of U1,
o2 for operation of U2,
o3 for operation of U3,
x,y for set;

theorem :: ALG_1:1
for D1,D2 be non empty set, p be FinSequence of D1, f be Function of D1,D2
holds dom(f*p) = dom p & len (f*p) = len p &
for n st n in dom (f*p) holds (f*p).n = f.(p.n);

theorem :: ALG_1:2
for B be non empty Subset of U1 st B = the carrier of U1 holds
Opers(U1,B) = the charact of(U1);

definition
let U1, U2 be 1-sorted;
mode Function of U1,U2 is Function of the carrier of U1,the carrier of U2;
end;

reserve a for FinSequence of U1,
f for Function of U1,U2;

theorem :: ALG_1:3
f*(<*>the carrier of U1) = <*>the carrier of U2;

theorem :: ALG_1:4
(id the carrier of U1)*a = a;

theorem :: ALG_1:5
for h1 be Function of U1,U2, h2 be Function of U2,U3,a be FinSequence of U1
holds h2*(h1*a) = (h2 * h1)*a;

definition let U1,U2,f;
pred f is_homomorphism U1,U2 means
:: ALG_1:def 1
U1,U2 are_similar &
for n st n in dom the charact of(U1)
for o1,o2 st o1=(the charact of U1).n & o2=(the charact of U2).n
for x be FinSequence of U1 st x in dom o1 holds f.(o1.x) = o2.(f*x);
end;

definition let U1,U2,f;
pred f is_monomorphism U1,U2 means
:: ALG_1:def 2
f is_homomorphism U1,U2 & f is one-to-one;
pred f is_epimorphism U1,U2 means
:: ALG_1:def 3
f is_homomorphism U1,U2 & rng f = the carrier of U2;
end;

definition let U1,U2,f;
pred f is_isomorphism U1,U2 means
:: ALG_1:def 4
f is_monomorphism U1,U2 & f is_epimorphism U1,U2;
end;

definition let U1,U2;
pred U1,U2 are_isomorphic means
:: ALG_1:def 5
ex f st f is_isomorphism U1,U2;
end;

theorem :: ALG_1:6
id the carrier of U1 is_homomorphism U1,U1;

theorem :: ALG_1:7
for h1 be Function of U1,U2, h2 be Function of U2,U3 st
h1 is_homomorphism U1,U2 & h2 is_homomorphism U2,U3 holds
h2 * h1 is_homomorphism U1,U3;

theorem :: ALG_1:8
f is_isomorphism U1,U2 iff
f is_homomorphism U1,U2 & rng f = the carrier of U2 & f is one-to-one;

theorem :: ALG_1:9
f is_isomorphism U1,U2 implies dom f = the carrier of U1 &
rng f = the carrier of U2;

theorem :: ALG_1:10
for h be Function of U1,U2, h1 be Function of U2,U1 st
h is_isomorphism U1,U2 & h1=h" holds h1 is_homomorphism U2,U1;

theorem :: ALG_1:11
for h be Function of U1,U2, h1 be Function of U2,U1 st
h is_isomorphism U1,U2 & h1 = h" holds h1 is_isomorphism U2,U1;

theorem :: ALG_1:12
for h be Function of U1,U2, h1 be Function of U2,U3 st
h is_isomorphism U1,U2 & h1 is_isomorphism U2,U3
holds h1 * h is_isomorphism U1,U3;

theorem :: ALG_1:13
U1,U1 are_isomorphic;

theorem :: ALG_1:14
U1,U2 are_isomorphic implies U2,U1 are_isomorphic;

theorem :: ALG_1:15
U1,U2 are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic;

definition let U1,U2,f;
assume  f is_homomorphism U1,U2;
func Image f -> strict SubAlgebra of U2 means
:: ALG_1:def 6
the carrier of it = f .: (the carrier of U1);
end;

theorem :: ALG_1:16
for h be Function of U1,U2 st h is_homomorphism U1,U2 holds
rng h = the carrier of Image h;

theorem :: ALG_1:17
for U2 being strict Universal_Algebra, f be Function of U1,U2
st f is_homomorphism U1,U2 holds f is_epimorphism U1,U2 iff Image f = U2;

begin
::
:: Quotient Universal Algebra
::

definition let U1 be 1-sorted;
mode Relation of U1 is Relation of the carrier of U1;
mode Equivalence_Relation of U1 is Equivalence_Relation of the carrier of U1;
canceled 2;
end;

definition let D be non empty set,
R be Relation of D;
func ExtendRel(R) -> Relation of D* means
:: ALG_1:def 9
for x,y be FinSequence of D holds
[x,y] in it iff len x = len y & for n st n in dom x holds [x.n,y.n] in R;
end;

theorem :: ALG_1:18
for D be non empty set holds ExtendRel(id D) = id (D*);

definition let U1;
mode Congruence of U1 -> Equivalence_Relation of U1 means
:: ALG_1:def 10
for n,o1 st n in dom the charact of(U1) & o1 = (the charact of U1).n
for x,y be FinSequence of U1 st x in dom o1 & y in dom o1 &
[x,y] in ExtendRel(it) holds [o1.x,o1.y] in it;
end;

reserve E for Congruence of U1;

definition let D be non empty set,
R be Equivalence_Relation of D;
let y be FinSequence of Class(R),
x be FinSequence of D;
pred x is_representatives_FS y means
:: ALG_1:def 11
len x = len y &
for n st n in dom x holds Class(R,x.n) = y.n;
end;

theorem :: ALG_1:19
for D be non empty set, R be Equivalence_Relation of D,
y be FinSequence of Class(R)
ex x be FinSequence of D st x is_representatives_FS y;

definition let U1 be Universal_Algebra,
E be Congruence of U1,
o be operation of U1;
func QuotOp(o,E) -> homogeneous quasi_total non empty
PartFunc of (Class E)*,(Class E) means
:: ALG_1:def 12
dom it = (arity o)-tuples_on (Class E) &
for y be FinSequence of (Class E) st y in dom it
for x be FinSequence of the carrier of U1 st x is_representatives_FS y
holds it.y = Class(E,o.x);
end;

definition let U1,E;
func QuotOpSeq(U1,E) -> PFuncFinSequence of Class E means
:: ALG_1:def 13
len it = len the charact of(U1) &
for n st n in dom it
for o1 st (the charact of(U1)).n = o1 holds it.n = QuotOp(o1,E);
end;

theorem :: ALG_1:20
for U1,E holds
UAStr (# Class(E),QuotOpSeq(U1,E) #) is strict Universal_Algebra;

definition let U1,E;
func QuotUnivAlg(U1,E) -> strict Universal_Algebra equals
:: ALG_1:def 14
UAStr (# Class(E),QuotOpSeq(U1,E) #);
end;

definition let U1,E;
func Nat_Hom(U1,E) -> Function of U1,QuotUnivAlg(U1,E) means
:: ALG_1:def 15
for u be Element of U1 holds it.u = Class(E,u);
end;

theorem :: ALG_1:21
for U1,E holds Nat_Hom(U1,E) is_homomorphism U1,QuotUnivAlg(U1,E);

theorem :: ALG_1:22
for U1,E holds Nat_Hom(U1,E) is_epimorphism U1,QuotUnivAlg(U1,E);

definition let U1,U2;let f be Function of U1,U2;
assume  f is_homomorphism U1,U2;
func Cng(f) -> Congruence of U1 means
:: ALG_1:def 16
for a,b be Element of U1 holds [a,b] in it iff f.a = f.b;
end;

definition
let U1,U2 be Universal_Algebra,
f be Function of U1,U2;
assume  f is_homomorphism U1,U2;
func HomQuot(f) -> Function of QuotUnivAlg(U1,Cng(f)),U2 means
:: ALG_1:def 17
for a be Element of U1 holds it.(Class(Cng f,a)) = f.a;
end;

theorem :: ALG_1:23
f is_homomorphism U1,U2 implies
HomQuot(f) is_homomorphism QuotUnivAlg(U1,Cng(f)),U2 &
HomQuot(f) is_monomorphism QuotUnivAlg(U1,Cng(f)),U2;

theorem :: ALG_1:24
f is_epimorphism U1,U2 implies HomQuot(f)
is_isomorphism QuotUnivAlg(U1,Cng(f)),U2;

theorem :: ALG_1:25
f is_epimorphism U1,U2 implies QuotUnivAlg(U1,Cng(f)),U2 are_isomorphic;
```