:: Homomorphisms of algebras. Quotient Universal Algebra
:: by Ma{\l}gorzata Korolkiewicz
::
:: Received October 12, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies UNIALG_1, SUBSET_1, NUMBERS, UNIALG_2, XBOOLE_0, FINSEQ_1,
FUNCT_1, RELAT_1, NAT_1, TARSKI, STRUCT_0, PARTFUN1, MSUALG_3, CQC_SIM1,
WELLORD1, FINSEQ_2, GROUP_6, EQREL_1, FUNCT_2, CARD_3, RELAT_2, ALG_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, RELAT_1,
RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, EQREL_1, FINSEQ_2,
FUNCT_2, STRUCT_0, MARGREL1, UNIALG_1, FINSEQOP, FINSEQ_3, UNIALG_2;
constructors EQREL_1, FINSEQOP, UNIALG_2, RELSET_1, CARD_3, FINSEQ_3, CARD_1,
NAT_1, NUMBERS;
registrations RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, EQREL_1, FINSEQ_2,
STRUCT_0, UNIALG_1, UNIALG_2, ORDINAL1, FINSEQ_1, CARD_1, RELSET_1,
MARGREL1;
requirements BOOLE, SUBSET;
definitions UNIALG_2, RELAT_2, TARSKI, FUNCT_1, XBOOLE_0, FUNCT_2, MARGREL1;
equalities UNIALG_2, XBOOLE_0;
expansions UNIALG_2, FUNCT_1, FUNCT_2, MARGREL1;
theorems FINSEQ_1, FINSEQ_2, FUNCT_1, FUNCT_2, PARTFUN1, UNIALG_1, UNIALG_2,
RELAT_1, RELSET_1, EQREL_1, ZFMISC_1, FINSEQ_3, XBOOLE_0, RELAT_2,
ORDERS_1, MARGREL1;
schemes FINSEQ_1, RELSET_1, FUNCT_2, FUNCT_1;
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 Th1:
for B be non empty Subset of U1 st B = the carrier of U1 holds
Opers(U1,B) = the charact of(U1)
proof
let B be non empty Subset of U1;
A1: dom Opers(U1,B) = dom the charact of(U1) by UNIALG_2:def 6;
assume
A2: B = the carrier of U1;
now
let n be Nat;
assume
A3: n in dom the charact of(U1);
then reconsider o = (the charact of U1).n as operation of U1 by
FUNCT_1:def 3;
thus Opers(U1,B).n = o/.B by A1,A3,UNIALG_2:def 6
.= (the charact of U1).n by A2,UNIALG_2:4;
end;
hence thesis by A1;
end;
reserve a for FinSequence of U1,
f for Function of U1,U2;
theorem
f*(<*>the carrier of U1) = <*>the carrier of U2;
theorem Th3:
(id the carrier of U1)*a = a
proof
set f = id the carrier of U1;
A1: dom (f*a) = dom a by FINSEQ_3:120;
A2: now
let n be Nat;
assume
A3: n in dom(f*a);
then reconsider u = a.n as Element of U1 by A1,FINSEQ_2:11;
f.u = u;
hence (f*a).n = a.n by A3,FINSEQ_3:120;
end;
len (f*a) = len a by FINSEQ_3:120;
hence thesis by A2,FINSEQ_2:9;
end;
theorem Th4:
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
proof
let h1 be Function of U1,U2, h2 be Function of U2,U3,a be FinSequence of U1;
A1: dom a = Seg len a by FINSEQ_1:def 3;
A2: dom (h2*(h1*a)) = dom(h1*a) by FINSEQ_3:120;
dom (h1*a) = dom a by FINSEQ_3:120;
then
A3: dom (h2*(h1*a)) = Seg len a by A2,FINSEQ_1:def 3;
A4: len a = len((h2 * h1 qua Function of the carrier of U1, the carrier of
U3) *(a qua FinSequence of the carrier of U1)) by FINSEQ_3:120;
then
A5: dom ((h2 * h1)*a) = Seg len a by FINSEQ_1:def 3;
A6: now
let n be Nat;
assume
A7: n in dom(h2*(h1*a));
hence (h2*(h1*a)).n = h2.((h1*a).n) by FINSEQ_3:120
.= h2.(h1.(a.n)) by A2,A7,FINSEQ_3:120
.= (h2*h1).(a.n) by A1,A3,A7,FINSEQ_2:11,FUNCT_2:15
.= ((h2 * h1)*a).n by A3,A5,A7,FINSEQ_3:120;
end;
len(h2*(h1*a)) = len(h1*a) & len(h1*a) = len a by FINSEQ_3:120;
hence thesis by A4,A6,FINSEQ_2:9;
end;
definition
let U1,U2,f;
pred f is_homomorphism means
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 means
f is_homomorphism & f is one-to-one;
pred f is_epimorphism means
f is_homomorphism & rng f = the carrier of U2;
end;
definition
let U1,U2,f;
pred f is_isomorphism means
f is_monomorphism & f is_epimorphism;
end;
definition
let U1,U2;
pred U1,U2 are_isomorphic means
ex f st f is_isomorphism;
end;
theorem Th5:
id the carrier of U1 is_homomorphism
proof
thus U1,U1 are_similar;
let n;
assume n in dom the charact of(U1);
let o1,o2 be operation of U1;
assume
A1: o1=(the charact of U1).n & o2=(the charact of U1).n;
set f = id the carrier of U1;
let x be FinSequence of U1;
assume x in dom o1;
then o1.x in rng o1 by FUNCT_1:def 3;
then reconsider u = o1.x as Element of U1;
f.u = u;
hence thesis by A1,Th3;
end;
theorem Th6:
for h1 be Function of U1,U2, h2 be Function of U2,U3 st h1
is_homomorphism & h2 is_homomorphism holds h2 * h1 is_homomorphism
proof
let h1 be Function of U1,U2, h2 be Function of U2,U3;
set s1 = signature U1, s2 = signature U2, s3 = signature U3;
assume that
A1: h1 is_homomorphism and
A2: h2 is_homomorphism;
U1,U2 are_similar by A1;
then
A3: s1 = s2;
U2,U3 are_similar by A2;
hence s1 = s3 by A3;
let n;
assume
A4: n in dom the charact of(U1);
let o1,o3;
assume that
A5: o1=(the charact of U1).n and
A6: o3=(the charact of U3).n;
let a;
reconsider b = h1*a as Element of (the carrier of U2)* by FINSEQ_1:def 11;
assume
A7: a in dom o1;
then
A8: o1.a in rng o1 by FUNCT_1:def 3;
dom o1 = (arity o1)-tuples_on (the carrier of U1) by MARGREL1:22;
then a in {w where w is Element of (the carrier of U1)*: len w = arity o1}
by A7,FINSEQ_2:def 4;
then
A9: ex w be Element of (the carrier of U1)* st w = a & len w = arity o1;
A10: len s1 = len the charact of(U1) & dom the charact of(U1) = Seg len the
charact of(U1) by FINSEQ_1:def 3,UNIALG_1:def 4;
A11: len s2 = len the charact of(U2) & dom the charact of(U2) = Seg len the
charact of(U2) by FINSEQ_1:def 3,UNIALG_1:def 4;
then reconsider o2 = (the charact of U2).n as operation of U2 by A3,A10,A4,
FUNCT_1:def 3;
A12: dom s1 = Seg len s1 by FINSEQ_1:def 3;
then
A13: s2.n = arity o2 by A3,A10,A4,UNIALG_1:def 4;
s1.n = arity o1 by A10,A12,A4,A5,UNIALG_1:def 4;
then len(h1*a) = arity o2 by A3,A13,A9,FINSEQ_3:120;
then dom o2 = (arity o2)-tuples_on (the carrier of U2) & b in {s where s is
Element of (the carrier of U2)*: len s = arity o2} by MARGREL1:22;
then h1*a in dom o2 by FINSEQ_2:def 4;
then
A14: h2.(o2.(h1*a)) = o3.(h2*(h1*a)) by A2,A3,A10,A11,A4,A6;
h1.(o1.a) = o2.(h1*a) by A1,A4,A5,A7;
hence (h2 * h1).(o1.a) = o3.(h2*(h1*a)) by A8,A14,FUNCT_2:15
.= o3.((h2 * h1)*a) by Th4;
end;
theorem Th7:
f is_isomorphism iff f is_homomorphism & rng f = the
carrier of U2 & f is one-to-one
proof
thus f is_isomorphism implies f is_homomorphism & rng f = the
carrier of U2 & f is one-to-one
proof
assume f is_isomorphism;
then f is_monomorphism & f is_epimorphism;
hence thesis;
end;
assume f is_homomorphism & rng f = the carrier of U2 & f is one-to-one;
then f is_monomorphism & f is_epimorphism;
hence thesis;
end;
theorem Th8:
f is_isomorphism implies dom f = the carrier of U1 & rng f
= the carrier of U2
proof
assume f is_isomorphism;
then f is_epimorphism;
hence thesis by FUNCT_2:def 1;
end;
theorem Th9:
for h be Function of U1,U2, h1 be Function of U2,U1 st h
is_isomorphism & h1=h" holds h1 is_homomorphism
proof
let h be Function of U1,U2,h1 be Function of U2,U1;
assume that
A1: h is_isomorphism and
A2: h1=h";
A3: h is one-to-one by A1,Th7;
A4: h is_homomorphism by A1,Th7;
then
A5: U1,U2 are_similar;
then
A6: signature U1 = signature U2;
A7: len (signature U1) = len the charact of(U1) & dom the charact of(U1) =
Seg len the charact of(U1) by FINSEQ_1:def 3,UNIALG_1:def 4;
A8: dom (signature U2) = Seg len (signature U2) by FINSEQ_1:def 3;
A9: len (signature U2) = len the charact of(U2) & dom the charact of(U2) =
Seg len the charact of(U2) by FINSEQ_1:def 3,UNIALG_1:def 4;
A10: rng h = the carrier of U2 by A1,Th7;
now
let n;
assume
A11: n in dom the charact of(U2);
let o2,o1;
assume
A12: o2 = (the charact of U2).n & o1 = (the charact of U1).n;
let x be FinSequence of U2;
defpred P[set,set] means h.$2 = x.$1;
A13: dom x = Seg len x by FINSEQ_1:def 3;
A14: for m be Nat st m in Seg len x ex a being Element of U1 st P[m,a]
proof
let m be Nat;
assume m in Seg len x;
then m in dom x by FINSEQ_1:def 3;
then x.m in the carrier of U2 by FINSEQ_2:11;
then consider a be object such that
A15: a in dom h and
A16: h.a = x.m by A10,FUNCT_1:def 3;
reconsider a as Element of U1 by A15;
take a;
thus thesis by A16;
end;
consider p being FinSequence of U1 such that
A17: dom p = Seg len x & for m be Nat st m in Seg len x holds P[m,p.m]
from FINSEQ_1:sch 5(A14);
A18: dom (h*p) = dom p by FINSEQ_3:120;
now
let n be Nat;
assume
A19: n in dom x;
hence x.n = h.(p.n) by A17,A13
.= (h*p).n by A17,A13,A18,A19,FINSEQ_3:120;
end;
then
A20: x = h*p by A17,A13,A18;
A21: len p = len x by A17,FINSEQ_1:def 3;
assume x in dom o2;
then x in (arity o2)-tuples_on the carrier of U2 by MARGREL1:22;
then x in {s where s is Element of (the carrier of U2)*: len s = arity o2
} by FINSEQ_2:def 4;
then
A22: ex s be Element of (the carrier of U2)* st x=s & len s = arity o2;
A23: (h1 * h) = (id dom h) by A2,A3,FUNCT_1:39
.= id the carrier of U1 by FUNCT_2:def 1;
then
A24: h1*x = (id the carrier of U1)*p by A20,Th4
.=p by Th3;
reconsider p as Element of (the carrier of U1)* by FINSEQ_1:def 11;
(signature U1).n = arity o1 & (signature U2).n = arity o2 by A6,A8,A9,A11
,A12,UNIALG_1:def 4;
then
p in {w where w is Element of (the carrier of U1)*: len w = arity o1}
by A6,A22,A21;
then p in (arity o1)-tuples_on the carrier of U1 by FINSEQ_2:def 4;
then
A25: p in dom o1 by MARGREL1:22;
then
A26: h1.(o2.x) = h1.(h.(o1.p)) by A4,A6,A7,A9,A11,A12,A20;
A27: o1.p in the carrier of U1 by A25,PARTFUN1:4;
then o1.p in dom h by FUNCT_2:def 1;
hence h1.(o2.x) = (id the carrier of U1).(o1.p) by A23,A26,FUNCT_1:13
.= o1.(h1*x) by A24,A27,FUNCT_1:17;
end;
hence thesis by A5;
end;
theorem Th10:
for h be Function of U1,U2, h1 be Function of U2,U1 st h
is_isomorphism & h1 = h" holds h1 is_isomorphism
proof
let h be Function of U1,U2,h1 be Function of U2,U1;
assume that
A1: h is_isomorphism and
A2: h1=h";
A3: h1 is_homomorphism by A1,A2,Th9;
A4: h is one-to-one by A1,Th7;
then rng h1 = dom h by A2,FUNCT_1:33
.= the carrier of U1 by FUNCT_2:def 1;
hence thesis by A2,A4,A3,Th7;
end;
theorem Th11:
for h be Function of U1,U2, h1 be Function of U2,U3 st h
is_isomorphism & h1 is_isomorphism holds h1 * h is_isomorphism
proof
let h be Function of U1,U2, h1 be Function of U2,U3;
assume that
A1: h is_isomorphism and
A2: h1 is_isomorphism;
dom h1 = the carrier of U2 & rng h = the carrier of U2 by A1,Th8,
FUNCT_2:def 1;
then
A3: rng (h1 * h) = rng h1 by RELAT_1:28
.= the carrier of U3 by A2,Th8;
h is_homomorphism & h1 is_homomorphism by A1,A2,Th7;
then
A4: h1 * h is_homomorphism by Th6;
h is one-to-one & h1 is one-to-one by A1,A2,Th7;
hence thesis by A3,A4,Th7;
end;
theorem
U1,U1 are_isomorphic
proof
set i = id the carrier of U1;
i is_homomorphism & rng i = the carrier of U1 by Th5;
then i is_isomorphism by Th7;
hence thesis;
end;
theorem
U1,U2 are_isomorphic implies U2,U1 are_isomorphic
proof
assume U1,U2 are_isomorphic;
then consider f such that
A1: f is_isomorphism;
f is_monomorphism by A1;
then
A2: f is one-to-one;
then
A3: rng(f") = dom f by FUNCT_1:33
.= the carrier of U1 by FUNCT_2:def 1;
A4: f is_epimorphism by A1;
dom(f") = rng f by A2,FUNCT_1:33
.= the carrier of U2 by A4;
then reconsider g = f" as Function of U2,U1 by A3,FUNCT_2:def 1,RELSET_1:4;
take g;
thus thesis by A1,Th10;
end;
theorem
U1,U2 are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic
proof
assume U1,U2 are_isomorphic;
then consider f such that
A1: f is_isomorphism;
assume U2,U3 are_isomorphic;
then consider g be Function of U2,U3 such that
A2: g is_isomorphism;
g * f is_isomorphism by A1,A2,Th11;
hence thesis;
end;
definition
let U1,U2,f;
assume
A1: f is_homomorphism;
func Image f -> strict SubAlgebra of U2 means
:Def6:
the carrier of it = f .: (the carrier of U1);
existence
proof
A2: dom f = the carrier of U1 by FUNCT_2:def 1;
then reconsider A = f .: (the carrier of U1) as non empty Subset of U2;
take B = UniAlgSetClosed(A);
A is opers_closed
proof
let o2 be operation of U2;
consider n being Nat such that
A3: n in dom the charact of(U2) and
A4: (the charact of U2).n = o2 by FINSEQ_2:10;
let s be FinSequence of A;
assume
A5: len s = arity o2;
defpred P[object,object] means f.$2 = s.$1;
A6: for x being object st x in dom s
ex y being object st y in the carrier of U1 & P[x,y]
proof
let x be object;
assume
A7: x in dom s;
then reconsider x0 = x as Element of NAT;
s.x0 in A by A7,FINSEQ_2:11;
then consider y being object such that
A8: y in dom f and
y in the carrier of U1 and
A9: f.y = s.x0 by FUNCT_1:def 6;
take y;
thus thesis by A8,A9;
end;
consider s1 be Function such that
A10: dom s1 = dom s & rng s1 c= the carrier of U1 &
for x being object st x in
dom s holds P[x,s1.x] from FUNCT_1:sch 6(A6);
dom s1 = Seg len s by A10,FINSEQ_1:def 3;
then reconsider s1 as FinSequence by FINSEQ_1:def 2;
reconsider s1 as FinSequence of U1 by A10,FINSEQ_1:def 4;
reconsider s1 as Element of (the carrier of U1)* by FINSEQ_1:def 11;
A11: len s1 = len s by A10,FINSEQ_3:29;
A12: dom (signature U2) = Seg len (signature U2) by FINSEQ_1:def 3;
A13: U1,U2 are_similar by A1;
then
A14: signature U1 = signature U2;
A15: dom (signature U1) = dom (signature U2) by A13;
A16: len (signature U2) = len the charact of(U2) & dom the charact of(U2)
= Seg len the charact of(U2) by FINSEQ_1:def 3,UNIALG_1:def 4;
then
A17: (signature U2).n = arity o2 by A3,A4,A12,UNIALG_1:def 4;
A18: len (f*s1) = len s1 by FINSEQ_3:120;
A19: dom (f*s1) = Seg len (f*s1) & dom s = Seg len s1 by A10,FINSEQ_1:def 3;
now
let m be Nat;
assume
A20: m in dom s;
then f.(s1.m) = s.m by A10;
hence (f*s1).m = s.m by A18,A19,A20,FINSEQ_3:120;
end;
then
A21: s = f*s1 by A11,A18,FINSEQ_2:9;
A22: dom (signature U1) = Seg len (signature U1) by FINSEQ_1:def 3;
A23: len (signature U1) = len the charact of(U1) & dom the charact of(U1)
= Seg len the charact of(U1) by FINSEQ_1:def 3,UNIALG_1:def 4;
then reconsider o1 = (the charact of U1).n as operation of U1 by A3,A16
,A22,A15,A12,FUNCT_1:def 3;
(signature U1).n = arity o1 by A3,A16,A15,A12,UNIALG_1:def 4;
then
s1 in {w where w is Element of (the carrier of U1)* : len w = arity
o1 } by A14,A5,A17,A11;
then s1 in (arity o1)-tuples_on the carrier of U1 by FINSEQ_2:def 4;
then
A24: s1 in dom o1 by MARGREL1:22;
then
A25: o1.s1 in rng o1 by FUNCT_1:def 3;
f.(o1.s1) = o2.(f*s1) by A1,A3,A4,A23,A16,A22,A15,A12,A24;
hence thesis by A2,A21,A25,FUNCT_1:def 6;
end;
then B = UAStr (# A,Opers(U2,A) #) by UNIALG_2:def 8;
hence thesis;
end;
uniqueness
proof
let A,B be strict SubAlgebra of U2;
reconsider A1 = the carrier of A as non empty Subset of U2
by UNIALG_2:def 7;
the charact of(A) = Opers(U2,A1) by UNIALG_2:def 7;
hence thesis by UNIALG_2:def 7;
end;
end;
theorem
for h be Function of U1,U2 st h is_homomorphism holds rng h =
the carrier of Image h
proof
let h be Function of U1,U2;
dom h = the carrier of U1 by FUNCT_2:def 1;
then
A1: rng h = h.:(the carrier of U1) by RELAT_1:113;
assume h is_homomorphism;
hence thesis by A1,Def6;
end;
theorem
for U2 being strict Universal_Algebra, f be Function of U1,U2 st f
is_homomorphism holds f is_epimorphism iff Image f = U2
proof
let U2 be strict Universal_Algebra;
let f be Function of U1,U2;
assume
A1: f is_homomorphism;
thus f is_epimorphism implies Image f = U2
proof
reconsider B = the carrier of Image f as non empty Subset of U2 by
UNIALG_2:def 7;
assume f is_epimorphism;
then
A2: the carrier of U2 = rng f
.= f.:(dom f) by RELAT_1:113
.= f.:(the carrier of U1) by FUNCT_2:def 1
.= the carrier of Image f by A1,Def6;
the charact of(Image f) = Opers(U2,B) by UNIALG_2:def 7;
hence thesis by A2,Th1;
end;
assume Image f = U2;
then the carrier of U2 = f.:(the carrier of U1) by A1,Def6
.= f.:(dom f) by FUNCT_2:def 1
.= rng f by RELAT_1:113;
hence thesis by A1;
end;
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;
end;
definition
let U1;
mode Congruence of U1 -> Equivalence_Relation of U1 means
:Def7:
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;
existence
proof
reconsider P = id the carrier of U1 as Equivalence_Relation of U1;
take P;
let n,o1;
assume that
n in dom the charact of(U1) and
o1 = (the charact of U1).n;
let x,y be FinSequence of U1;
assume that
A1: x in dom o1 and
y in dom o1 and
A2: [x,y] in ExtendRel(P);
[x,y] in id ((the carrier of U1)*) by A2,FINSEQ_3:121;
then
A3: x = y by RELAT_1:def 10;
o1.x in rng o1 by A1,FUNCT_1:def 3;
hence thesis by A3,RELAT_1:def 10;
end;
end;
reserve E for Congruence of U1;
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
:Def8:
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);
existence
proof
defpred P[object,object] means
for y be FinSequence of (Class E) st y = $1 holds
for x be FinSequence of the carrier of U1 st x is_representatives_FS y holds $2
= Class(E,o.x);
set X = (arity o)-tuples_on (Class E);
A1: for e be object st e in X ex u be object st u in Class(E) & P[e,u]
proof
let e be object;
A2: dom o = (arity o)-tuples_on the carrier of U1 by MARGREL1:22
.={q where q is Element of (the carrier of U1)*: len q = arity o} by
FINSEQ_2:def 4;
assume e in X;
then e in {s where s is Element of (Class E)*: len s = arity o} by
FINSEQ_2:def 4;
then consider s be Element of (Class E)* such that
A3: s = e and
A4: len s = arity o;
consider x be FinSequence of the carrier of U1 such that
A5: x is_representatives_FS s by FINSEQ_3:122;
take y = Class(E,o.x);
A6: len x = arity o by A4,A5,FINSEQ_3:def 4;
x is Element of (the carrier of U1)* by FINSEQ_1:def 11;
then
A7: x in dom o by A2,A6;
then
A8: o.x in rng o by FUNCT_1:def 3;
hence y in Class E by EQREL_1:def 3;
let a be FinSequence of (Class E);
assume
A9: a = e;
let b be FinSequence of the carrier of U1;
assume
A10: b is_representatives_FS a;
then
A11: len b = arity o by A3,A4,A9,FINSEQ_3:def 4;
for m st m in dom x holds [x.m,b.m] in E
proof
let m;
assume
A12: m in dom x;
then
A13: Class(E,x.m) = s.m & x.m in rng x by A5,FINSEQ_3:def 4,FUNCT_1:def 3;
dom x = Seg arity o by A6,FINSEQ_1:def 3
.= dom b by A11,FINSEQ_1:def 3;
then Class(E,b.m) = s.m by A3,A9,A10,A12,FINSEQ_3:def 4;
hence thesis by A13,EQREL_1:35;
end;
then
A14: [x,b] in ExtendRel(E) by A6,A11,FINSEQ_3:def 3;
b is Element of (the carrier of U1)* by FINSEQ_1:def 11;
then
(ex n being Nat st n in dom the charact of(U1) & (the charact of U1
).n = o ) & b in dom o by A2,A11,FINSEQ_2:10;
then [o.x,o.b] in E by A7,A14,Def7;
hence thesis by A8,EQREL_1:35;
end;
consider F being Function such that
A15: dom F = X & rng F c= Class(E) & for e be object st e in X holds P[e,
F.e] from FUNCT_1:sch 6(A1);
X in the set of all m-tuples_on Class E;
then X c= union the set of all m-tuples_on Class E by ZFMISC_1:74;
then X c= (Class E)* by FINSEQ_2:108;
then reconsider F as PartFunc of (Class E)*,Class E by A15,RELSET_1:4;
A16: dom F = {t where t is Element of (Class E)*: len t = arity o} by A15,
FINSEQ_2:def 4;
A17: for x,y be FinSequence of Class E st len x = len y & x in dom F holds
y in dom F
proof
let x,y be FinSequence of Class E;
assume that
A18: len x = len y and
A19: x in dom F;
A20: y is Element of (Class E)* by FINSEQ_1:def 11;
ex t1 be Element of (Class E)* st x = t1 & len t1 = arity o by A16,A19;
hence thesis by A16,A18,A20;
end;
A21: ex x being FinSequence st x in dom F
proof
set a = the Element of X;
a in X;
hence ex x being FinSequence st x in dom F by A15;
end;
dom F is with_common_domain
proof
let x,y be FinSequence;
assume x in dom F & y in dom F;
then (ex t1 be Element of (Class E)* st x = t1 & len t1 = arity o )& ex
t2 be Element of (Class E)* st y = t2 & len t2 = arity o by A16;
hence thesis;
end;
then reconsider
F as homogeneous quasi_total non empty PartFunc of (Class E)*,
Class E by A17,A21,MARGREL1:def 21,def 22;
take F;
thus dom F = (arity o)-tuples_on (Class E) by A15;
let y be FinSequence of (Class E);
assume
A22: y in dom F;
let x be FinSequence of the carrier of U1;
assume x is_representatives_FS y;
hence thesis by A15,A22;
end;
uniqueness
proof
let F,G be homogeneous quasi_total non empty PartFunc of (Class(E))*,Class
(E);
assume that
A23: dom F = (arity o)-tuples_on (Class E) and
A24: for y be FinSequence of Class(E) st y in dom F for x be
FinSequence of the carrier of U1 st x is_representatives_FS y holds F.y = Class
(E,o.x) and
A25: dom G = (arity(o))-tuples_on (Class(E)) and
A26: for y be FinSequence of Class(E) st y in dom G for x be
FinSequence of the carrier of U1 st x is_representatives_FS y holds G.y = Class
(E,o.x);
for a be object st a in dom F holds F.a = G.a
proof
let a be object;
assume
A27: a in dom F;
then reconsider b = a as FinSequence of Class(E) by FINSEQ_1:def 11;
consider x be FinSequence of the carrier of U1 such that
A28: x is_representatives_FS b by FINSEQ_3:122;
F.b = Class(E,o.x) by A24,A27,A28;
hence thesis by A23,A25,A26,A27,A28;
end;
hence thesis by A23,A25;
end;
end;
definition
let U1,E;
func QuotOpSeq(U1,E) -> PFuncFinSequence of Class E means
:Def9:
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);
existence
proof
defpred P[set,set] means for o be Element of Operations(U1) st o = (the
charact of(U1)).$1 holds $2 = QuotOp(o,E);
A1: for n be Nat st n in Seg len the charact of(U1) ex x be Element of
PFuncs((Class E)*,(Class E)) st P[n,x]
proof
let n be Nat;
assume n in Seg len the charact of(U1);
then n in dom the charact of(U1) by FINSEQ_1:def 3;
then reconsider o = (the charact of(U1)).n as operation of U1 by
FUNCT_1:def 3;
reconsider x = QuotOp(o,E) as Element of PFuncs((Class E)*,(Class E)) by
PARTFUN1:45;
take x;
thus thesis;
end;
consider p be FinSequence of PFuncs((Class E)*,(Class E)) such that
A2: dom p = Seg len the charact of(U1) & for n be Nat st n in Seg len
the charact of(U1) holds P[n,p.n] from FINSEQ_1:sch 5(A1);
reconsider p as PFuncFinSequence of Class E;
take p;
thus len p = len the charact of(U1) by A2,FINSEQ_1:def 3;
let n;
assume n in dom p;
hence thesis by A2;
end;
uniqueness
proof
let F,G be PFuncFinSequence of Class E;
assume that
A3: len F = len the charact of(U1) and
A4: for n st n in dom F for o1 st (the charact of(U1)).n = o1 holds F.
n = QuotOp(o1,E) and
A5: len G = len the charact of(U1) and
A6: for n st n in dom G for o1 st (the charact of(U1)).n = o1 holds G.
n = QuotOp(o1,E);
now
let n be Nat;
assume
A7: n in dom F;
dom F = Seg len the charact of(U1) by A3,FINSEQ_1:def 3;
then n in dom the charact of(U1) by A7,FINSEQ_1:def 3;
then reconsider o1 = (the charact of U1).n as operation of U1 by
FUNCT_1:def 3;
A8: dom F = dom the charact of(U1) & dom G = dom the charact of(U1) by A3,A5,
FINSEQ_3:29;
F.n = QuotOp(o1,E) by A4,A7;
hence F.n = G.n by A6,A8,A7;
end;
hence thesis by A3,A5,FINSEQ_2:9;
end;
end;
definition
let U1,E;
func QuotUnivAlg(U1,E) -> strict Universal_Algebra equals
UAStr (# Class(E),QuotOpSeq(U1,E) #);
coherence
proof
set UU = UAStr (# Class(E),QuotOpSeq(U1,E) #);
for n be Nat,h be PartFunc of (Class E)*,(Class E) st n in dom QuotOpSeq
(U1,E) & h = QuotOpSeq(U1,E).n holds h is homogeneous
proof
let n be Nat,h be PartFunc of (Class E)*,(Class E);
assume that
A1: n in dom QuotOpSeq(U1,E) and
A2: h = QuotOpSeq(U1,E).n;
n in Seg len QuotOpSeq(U1,E) by A1,FINSEQ_1:def 3;
then n in Seg len the charact of U1 by Def9;
then n in dom the charact of U1 by FINSEQ_1:def 3;
then reconsider o = (the charact of U1).n as operation of U1 by
FUNCT_1:def 3;
QuotOpSeq(U1,E).n = QuotOp(o,E) by A1,Def9;
hence thesis by A2;
end;
then
A3: the charact of UU is homogeneous;
for n be Nat ,h be PartFunc of (Class E)*,(Class E) st n in dom
QuotOpSeq(U1,E) & h = QuotOpSeq(U1,E).n holds h is quasi_total
proof
let n be Nat,h be PartFunc of (Class E)*,(Class E);
assume that
A4: n in dom QuotOpSeq(U1,E) and
A5: h = QuotOpSeq(U1,E).n;
n in Seg len QuotOpSeq(U1,E) by A4,FINSEQ_1:def 3;
then n in Seg len the charact of(U1) by Def9;
then n in dom the charact of U1 by FINSEQ_1:def 3;
then reconsider o = (the charact of U1).n as operation of U1 by
FUNCT_1:def 3;
QuotOpSeq(U1,E).n = QuotOp(o,E) by A4,Def9;
hence thesis by A5;
end;
then
A6: the charact of UU is quasi_total;
for n be object st n in dom QuotOpSeq(U1,E)
holds QuotOpSeq(U1,E).n is non empty
proof
let n be object;
assume
A7: n in dom QuotOpSeq(U1,E);
then n in Seg len QuotOpSeq(U1,E) by FINSEQ_1:def 3;
then n in Seg len the charact of U1 by Def9;
then
A8: n in dom the charact of U1 by FINSEQ_1:def 3;
reconsider n as Element of NAT by A7;
reconsider o = (the charact of U1).n as operation of U1
by A8,FUNCT_1:def 3;
QuotOpSeq(U1,E).n = QuotOp(o,E) by A7,Def9;
hence thesis;
end;
then
A9: the charact of UU is non-empty by FUNCT_1:def 9;
the charact of UU <> {}
proof
assume
A10: the charact of UU = {};
len the charact of UU = len the charact of U1 by Def9;
hence contradiction by A10;
end;
hence thesis by A3,A6,A9,UNIALG_1:def 1,def 2,def 3;
end;
end;
definition
let U1,E;
func Nat_Hom(U1,E) -> Function of U1,QuotUnivAlg(U1,E) means
:Def11:
for u be Element of U1 holds it.u = Class(E,u);
existence
proof
defpred P[Element of U1,set] means $2 = Class(E,$1);
A1: for x being Element of U1 ex y being Element of QuotUnivAlg(U1,E) st P
[x,y]
proof
let x be Element of U1;
reconsider y = Class(E,x) as Element of QuotUnivAlg(U1,E) by
EQREL_1:def 3;
take y;
thus thesis;
end;
consider f being Function of U1,QuotUnivAlg(U1,E) such that
A2: for x being Element of U1 holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
thus thesis by A2;
end;
uniqueness
proof
let f,g be Function of U1,QuotUnivAlg(U1,E);
assume that
A3: for u be Element of U1 holds f.u = Class(E,u) and
A4: for u be Element of U1 holds g.u = Class(E,u);
now
let u be Element of U1;
f.u = Class(E,u) by A3;
hence f.u = g.u by A4;
end;
hence thesis;
end;
end;
theorem Th17:
for U1,E holds Nat_Hom(U1,E) is_homomorphism
proof
let U1,E;
set f = Nat_Hom(U1,E), u1 = the carrier of U1, qu = the carrier of
QuotUnivAlg(U1,E);
A1: len (signature U1) = len the charact of(U1) by UNIALG_1:def 4;
A2: dom (signature U1) = Seg len(signature U1) by FINSEQ_1:def 3;
A3: len QuotOpSeq(U1,E) = len the charact of(U1) by Def9;
A4: len (signature QuotUnivAlg(U1,E)) = len the charact of(QuotUnivAlg(U1,E)
) by UNIALG_1:def 4;
now
let n be Nat;
assume
A5: n in dom (signature U1);
then n in dom the charact of(U1) by A1,A2,FINSEQ_1:def 3;
then reconsider o1 = (the charact of U1).n as operation of U1 by
FUNCT_1:def 3;
n in dom QuotOpSeq(U1,E) by A3,A1,A2,A5,FINSEQ_1:def 3;
then
A6: QuotOpSeq(U1,E).n = QuotOp(o1,E) by Def9;
reconsider cl = QuotOp(o1,E) as homogeneous quasi_total non empty PartFunc
of qu*,qu;
consider b be object such that
A7: b in dom cl by XBOOLE_0:def 1;
reconsider b as Element of qu* by A7;
dom QuotOp(o1,E) = (arity o1)-tuples_on Class(E) by Def8;
then b in {w where w is Element of (Class(E))*: len w = arity o1} by A7,
FINSEQ_2:def 4;
then ex w be Element of (Class(E))* st w = b & len w = arity o1;
then
A8: arity cl = arity o1 by A7,MARGREL1:def 25;
n in dom (signature QuotUnivAlg(U1,E)) & (signature U1).n = arity o1
by A3,A4,A2,A5,FINSEQ_1:def 3,UNIALG_1:def 4;
hence (signature U1).n = (signature QuotUnivAlg(U1,E)).n by A6,A8,
UNIALG_1:def 4;
end;
hence signature U1 = signature QuotUnivAlg(U1,E) by A3,A4,A1,FINSEQ_2:9;
let n;
assume n in dom the charact of(U1);
then n in Seg len the charact of(U1) by FINSEQ_1:def 3;
then
A9: n in dom QuotOpSeq(U1,E) by A3,FINSEQ_1:def 3;
let o1 be operation of U1, o2 be operation of QuotUnivAlg(U1,E);
assume
(the charact of U1).n = o1 & o2 = (the charact of QuotUnivAlg(U1,E) ).n;
then
A10: o2 = QuotOp(o1,E) by A9,Def9;
let x be FinSequence of U1;
reconsider x1 = x as Element of u1* by FINSEQ_1:def 11;
reconsider fx = f*x as FinSequence of Class(E);
reconsider fx as Element of (Class(E))* by FINSEQ_1:def 11;
A11: len (f*x) = len x by FINSEQ_3:120;
now
let m;
assume
A12: m in dom x;
then
A13: m in dom(f*x) by FINSEQ_3:120;
x.m in rng x by A12,FUNCT_1:def 3;
then reconsider xm = x.m as Element of u1;
thus Class(E,x.m) = f.xm by Def11
.= fx.m by A13,FINSEQ_3:120;
end;
then
A14: x is_representatives_FS fx by A11,FINSEQ_3:def 4;
assume
A15: x in dom o1;
then o1.x in rng o1 by FUNCT_1:def 3;
then reconsider ox = o1.x as Element of u1;
dom o1 = (arity o1)-tuples_on u1 by MARGREL1:22
.= {p where p is Element of u1* : len p = arity o1} by FINSEQ_2:def 4;
then
A16: ex p be Element of u1* st p = x1 & len p = arity o1 by A15;
A17: f.(o1.x) = Class(E,ox) by Def11
.= Class(E,o1.x);
dom QuotOp(o1,E) = (arity o1)-tuples_on Class(E) by Def8
.= {q where q is Element of (Class(E))*: len q = arity o1} by
FINSEQ_2:def 4;
then fx in dom QuotOp(o1,E) by A16,A11;
hence thesis by A17,A10,A14,Def8;
end;
theorem
for U1,E holds Nat_Hom(U1,E) is_epimorphism
proof
let U1,E;
set f = Nat_Hom(U1,E), qa = QuotUnivAlg(U1,E), cqa = the carrier of qa, u1 =
the carrier of U1;
thus f is_homomorphism by Th17;
thus rng f c= cqa;
let x be object;
assume
A1: x in cqa;
then reconsider x1 = x as Subset of u1;
consider y being object such that
A2: y in u1 and
A3: x1 = Class(E,y) by A1,EQREL_1:def 3;
reconsider y as Element of u1 by A2;
dom f = u1 by FUNCT_2:def 1;
then f.y in rng f by FUNCT_1:def 3;
hence thesis by A3,Def11;
end;
definition
let U1,U2;
let f be Function of U1,U2;
assume
A1: f is_homomorphism;
func Cng(f) -> Congruence of U1 means
:Def12:
for a,b be Element of U1 holds [a,b] in it iff f.a = f.b;
existence
proof
defpred P[set,set] means f.$1 = f.$2;
set u1 = the carrier of U1;
consider R being Relation of u1,u1 such that
A2: for x,y being Element of u1 holds [x,y] in R iff P[x,y] from
RELSET_1:sch 2;
R is_reflexive_in u1
proof
let x be object;
assume x in u1;
then reconsider x1 = x as Element of u1;
f.x1 =f.x1;
hence thesis by A2;
end;
then
A3: dom R = u1 & field R = u1 by ORDERS_1:13;
A4: R is_transitive_in u1
proof
let x,y,z be object;
assume that
A5: x in u1 & y in u1 & z in u1 and
A6: [x,y] in R & [y,z] in R;
reconsider x1 = x, y1=y, z1 = z as Element of u1 by A5;
f.x1 = f.y1 & f.y1 = f.z1 by A2,A6;
hence thesis by A2;
end;
R is_symmetric_in u1
proof
let x,y be object;
assume that
A7: x in u1 & y in u1 and
A8: [x,y] in R;
reconsider x1 = x, y1=y as Element of u1 by A7;
f.x1 = f.y1 by A2,A8;
hence thesis by A2;
end;
then reconsider R as Equivalence_Relation of U1 by A3,A4,PARTFUN1:def 2
,RELAT_2:def 11,def 16;
now
U1,U2 are_similar by A1;
then
A9: signature U1 = signature U2;
let n be Nat,o be operation of U1;
assume that
A10: n in dom the charact of(U1) and
A11: o = (the charact of U1).n;
len (signature U1) = len the charact of(U1) & len (signature U2) =
len the charact of(U2) by UNIALG_1:def 4;
then dom the charact of(U2) = dom the charact of(U1) by A9,FINSEQ_3:29;
then reconsider o2 = (the charact of U2).n as operation of U2 by A10,
FUNCT_1:def 3;
let x,y be FinSequence of U1;
assume that
A12: x in dom o & y in dom o and
A13: [x,y] in ExtendRel(R);
o.x in rng o & o.y in rng o by A12,FUNCT_1:def 3;
then reconsider ox = o.x, oy = o.y as Element of u1;
A14: len x = len y by A13,FINSEQ_3:def 3;
A15: len (f*y) = len y by FINSEQ_3:120;
then
A16: dom (f*y) = Seg len x by A14,FINSEQ_1:def 3;
A17: len (f*x) = len x by FINSEQ_3:120;
A18: now
let m be Nat;
assume
A19: m in dom (f*y);
then m in dom y by A14,A16,FINSEQ_1:def 3;
then
A20: y.m in rng y by FUNCT_1:def 3;
A21: m in dom x by A16,A19,FINSEQ_1:def 3;
then x.m in rng x by FUNCT_1:def 3;
then reconsider xm = x.m, ym = y.m as Element of u1 by A20;
[x.m,y.m] in R by A13,A21,FINSEQ_3:def 3;
then
A22: f.xm = f.ym by A2
.= (f*y).m by A19,FINSEQ_3:120;
m in dom (f*x) by A17,A16,A19,FINSEQ_1:def 3;
hence (f*y).m = (f*x).m by A22,FINSEQ_3:120;
end;
f.(o.x) = o2.(f*x) & f.(o.y) = o2.(f*y) by A1,A10,A11,A12;
then f.(ox) = f.(oy) by A14,A17,A15,A18,FINSEQ_2:9;
hence [o.x,o.y] in R by A2;
end;
then reconsider R as Congruence of U1 by Def7;
take R;
let a,b be Element of u1;
thus [a,b] in R implies f.a = f.b by A2;
assume f.a = f.b;
hence thesis by A2;
end;
uniqueness
proof
set u1 = the carrier of U1;
let X,Y be Congruence of U1;
assume that
A23: for a,b be Element of U1 holds [a,b] in X iff f.a = f.b and
A24: for a,b be Element of U1 holds [a,b] in Y iff f.a = f.b;
for x,y be object holds [x,y] in X iff [x,y] in Y
proof
let x,y be object;
thus [x,y] in X implies [x,y] in Y
proof
assume
A25: [x,y] in X;
then reconsider x1 = x,y1 = y as Element of u1 by ZFMISC_1:87;
f.x1 = f.y1 by A23,A25;
hence thesis by A24;
end;
assume
A26: [x,y] in Y;
then reconsider x1 = x,y1 = y as Element of u1 by ZFMISC_1:87;
f.x1 = f.y1 by A24,A26;
hence thesis by A23;
end;
hence thesis by RELAT_1:def 2;
end;
end;
definition
let U1,U2 be Universal_Algebra, f be Function of U1,U2;
assume
A1: f is_homomorphism;
func HomQuot(f) -> Function of QuotUnivAlg(U1,Cng(f)),U2 means
:Def13:
for a be Element of U1 holds it.(Class(Cng f,a)) = f.a;
existence
proof
set qa = QuotUnivAlg(U1,Cng(f)), cqa = the carrier of qa, u1 = the carrier
of U1, u2 = the carrier of U2;
defpred P[object,object] means
for a be Element of u1 st $1 = Class(Cng f,a)
holds $2 = f.a;
A2: for x being object st x in cqa ex y being object st y in u2 & P[x,y]
proof
let x be object;
assume
A3: x in cqa;
then reconsider x1 = x as Subset of u1;
consider a be object such that
A4: a in u1 and
A5: x1 = Class(Cng f,a) by A3,EQREL_1:def 3;
reconsider a as Element of u1 by A4;
take y = f.a;
thus y in u2;
let b be Element of u1;
assume x = Class(Cng f,b);
then b in Class(Cng f,a) by A5,EQREL_1:23;
then [b,a] in Cng(f) by EQREL_1:19;
hence thesis by A1,Def12;
end;
consider F being Function such that
A6: dom F = cqa & rng F c= u2 & for x being object st x in cqa holds P[x,F.x]
from
FUNCT_1:sch 6(A2);
reconsider F as Function of qa,U2 by A6,FUNCT_2:def 1,RELSET_1:4;
take F;
let a be Element of u1;
Class(Cng f,a) in Class(Cng f) by EQREL_1:def 3;
hence thesis by A6;
end;
uniqueness
proof
set qa = QuotUnivAlg(U1,Cng(f)), cqa = the carrier of qa, u1 = the carrier
of U1;
let F,G be Function of qa,U2;
assume that
A7: for a be Element of u1 holds F.(Class(Cng f,a)) = f.a and
A8: for a be Element of u1 holds G.(Class(Cng f,a)) = f.a;
let x be Element of cqa;
x in cqa;
then reconsider x1 = x as Subset of u1;
consider a be object such that
A9: a in u1 & x1 = Class(Cng f,a) by EQREL_1:def 3;
thus F.x = f.a by A7,A9
.= G.x by A8,A9;
end;
end;
theorem Th19:
f is_homomorphism implies HomQuot(f) is_homomorphism
& HomQuot(f) is_monomorphism
proof
set qa = QuotUnivAlg(U1,Cng(f)), cqa = the carrier of qa, u1 = the carrier
of U1, F = HomQuot(f);
assume
A1: f is_homomorphism;
thus
A2: F is_homomorphism
proof
Nat_Hom(U1,Cng f) is_homomorphism by Th17;
then U1,qa are_similar;
then
A3: signature U1 = signature qa;
U1,U2 are_similar by A1;
then signature U2 = signature qa by A3;
hence qa,U2 are_similar;
let n;
assume
A4: n in dom the charact of(qa);
A5: len (signature U1) = len the charact of(U1) & len (signature qa) =
len the charact of(qa) by UNIALG_1:def 4;
A6: dom the charact of(qa) = Seg len (the charact of qa) & dom the
charact of(U1 ) = Seg len (the charact of U1) by FINSEQ_1:def 3;
then reconsider o1 = (the charact of U1).n as operation of U1 by A3,A4,A5,
FUNCT_1:def 3;
A7: dom o1 = (arity o1)-tuples_on u1 by MARGREL1:22
.= {p where p is Element of u1* : len p = arity o1} by FINSEQ_2:def 4;
let oq be operation of qa, o2 be operation of U2;
assume that
A8: oq = (the charact of qa).n and
A9: o2 = (the charact of U2).n;
let x be FinSequence of qa;
assume
A10: x in dom oq;
reconsider x1 = x as FinSequence of Class(Cng f);
reconsider x1 as Element of (Class(Cng f))* by FINSEQ_1:def 11;
consider y be FinSequence of U1 such that
A11: y is_representatives_FS x1 by FINSEQ_3:122;
reconsider y as Element of u1* by FINSEQ_1:def 11;
A12: len x1 = len y by A11,FINSEQ_3:def 4;
then
A13: len (F*x) = len y by FINSEQ_3:120;
A14: len y = len (f*y) by FINSEQ_3:120;
A15: now
let m be Nat;
assume
A16: m in Seg len y;
then
A17: m in dom (F*x) by A13,FINSEQ_1:def 3;
A18: m in dom(f*y) by A14,A16,FINSEQ_1:def 3;
A19: m in dom y by A16,FINSEQ_1:def 3;
then reconsider ym = y.m as Element of u1 by FINSEQ_2:11;
x1.m = Class(Cng f,y.m) by A11,A19,FINSEQ_3:def 4;
hence (F*x).m = F.(Class(Cng f,ym)) by A17,FINSEQ_3:120
.= f.(y.m) by A1,Def13
.= (f*y).m by A18,FINSEQ_3:120;
end;
dom(F*x) = Seg len y by A13,FINSEQ_1:def 3;
then
A20: o2.(F*x) = o2.(f*y) by A13,A14,A15,FINSEQ_2:9;
A21: oq = QuotOp(o1,Cng f) by A4,A8,Def9;
then dom oq = (arity o1)-tuples_on Class(Cng f) by Def8
.= {w where w is Element of (Class(Cng f))*: len w = arity o1} by
FINSEQ_2:def 4;
then ex w be Element of (Class(Cng f))* st w = x1 & len w = arity o1 by A10
;
then
A22: y in dom o1 by A12,A7;
then o1.y in rng o1 by FUNCT_1:def 3;
then reconsider o1y = o1.y as Element of u1;
F.(oq.x) = F.(Class(Cng f,o1y)) by A10,A11,A21,Def8
.= f.(o1.y) by A1,Def13;
hence thesis by A1,A3,A4,A9,A6,A5,A22,A20;
end;
A23: dom F = cqa by FUNCT_2:def 1;
F is one-to-one
proof
let x,y be object;
assume that
A24: x in dom F and
A25: y in dom F and
A26: F.x = F.y;
reconsider x1 = x, y1 = y as Subset of u1 by A23,A24,A25;
consider a be object such that
A27: a in u1 and
A28: x1 = Class(Cng f,a) by A24,EQREL_1:def 3;
reconsider a as Element of u1 by A27;
consider b be object such that
A29: b in u1 and
A30: y1 = Class(Cng f,b) by A25,EQREL_1:def 3;
reconsider b as Element of u1 by A29;
A31: F.y1 = f.b by A1,A30,Def13;
F.x1 = f.a by A1,A28,Def13;
then [a,b] in Cng(f) by A1,A26,A31,Def12;
hence thesis by A28,A30,EQREL_1:35;
end;
hence thesis by A2;
end;
::$N First isomorphism theorem for universal algebras
theorem Th20:
f is_epimorphism implies HomQuot(f) is_isomorphism
proof
set qa = QuotUnivAlg(U1,Cng(f)), u1 = the carrier of U1, u2 = the carrier of
U2, F = HomQuot(f);
assume
A1: f is_epimorphism;
then
A2: f is_homomorphism;
then F is_monomorphism by Th19;
then
A3: F is one-to-one;
A4: rng f = u2 by A1;
A5: rng F = u2
proof
thus rng F c= u2;
let x be object;
assume x in u2;
then consider y being object such that
A6: y in dom f and
A7: f.y = x by A4,FUNCT_1:def 3;
reconsider y as Element of u1 by A6;
set u = Class(Cng f,y);
A8: dom F = the carrier of qa & u in Class(Cng f) by EQREL_1:def 3
,FUNCT_2:def 1;
F.u = x by A2,A7,Def13;
hence thesis by A8,FUNCT_1:def 3;
end;
F is_homomorphism by A2,Th19;
hence thesis by A3,A5,Th7;
end;
theorem
f is_epimorphism implies QuotUnivAlg(U1,Cng(f)),U2 are_isomorphic
proof
assume
A1: f is_epimorphism;
take HomQuot(f);
thus thesis by A1,Th20;
end;