let U1, U2 be Universal_Algebra; for f being Function of U1,U2 st f is_homomorphism U1,U2 holds
( HomQuot f is_homomorphism QuotUnivAlg U1,(Cng f),U2 & HomQuot f is_monomorphism QuotUnivAlg U1,(Cng f),U2 )
let f be Function of U1,U2; ( f is_homomorphism U1,U2 implies ( HomQuot f is_homomorphism QuotUnivAlg U1,(Cng f),U2 & HomQuot f is_monomorphism QuotUnivAlg U1,(Cng f),U2 ) )
set qa = QuotUnivAlg U1,(Cng f);
set cqa = the carrier of (QuotUnivAlg U1,(Cng f));
set u1 = the carrier of U1;
set F = HomQuot f;
assume A1:
f is_homomorphism U1,U2
; ( HomQuot f is_homomorphism QuotUnivAlg U1,(Cng f),U2 & HomQuot f is_monomorphism QuotUnivAlg U1,(Cng f),U2 )
thus A2:
HomQuot f is_homomorphism QuotUnivAlg U1,(Cng f),U2
HomQuot f is_monomorphism QuotUnivAlg U1,(Cng f),U2proof
Nat_Hom U1,
(Cng f) is_homomorphism U1,
QuotUnivAlg U1,
(Cng f)
by Th21;
then
U1,
QuotUnivAlg U1,
(Cng f) are_similar
by Def1;
then A3:
signature U1 = signature (QuotUnivAlg U1,(Cng f))
by UNIALG_2:def 2;
U1,
U2 are_similar
by A1, Def1;
then
signature U2 = signature (QuotUnivAlg U1,(Cng f))
by A3, UNIALG_2:def 2;
hence
QuotUnivAlg U1,
(Cng f),
U2 are_similar
by UNIALG_2:def 2;
ALG_1:def 1 for n being Element of NAT st n in dom the charact of (QuotUnivAlg U1,(Cng f)) holds
for o1 being operation of (QuotUnivAlg U1,(Cng f))
for o2 being operation of U2 st o1 = the charact of (QuotUnivAlg U1,(Cng f)) . n & o2 = the charact of U2 . n holds
for x being FinSequence of (QuotUnivAlg U1,(Cng f)) st x in dom o1 holds
(HomQuot f) . (o1 . x) = o2 . ((HomQuot f) * x)
let n be
Element of
NAT ;
( n in dom the charact of (QuotUnivAlg U1,(Cng f)) implies for o1 being operation of (QuotUnivAlg U1,(Cng f))
for o2 being operation of U2 st o1 = the charact of (QuotUnivAlg U1,(Cng f)) . n & o2 = the charact of U2 . n holds
for x being FinSequence of (QuotUnivAlg U1,(Cng f)) st x in dom o1 holds
(HomQuot f) . (o1 . x) = o2 . ((HomQuot f) * x) )
assume A4:
n in dom the
charact of
(QuotUnivAlg U1,(Cng f))
;
for o1 being operation of (QuotUnivAlg U1,(Cng f))
for o2 being operation of U2 st o1 = the charact of (QuotUnivAlg U1,(Cng f)) . n & o2 = the charact of U2 . n holds
for x being FinSequence of (QuotUnivAlg U1,(Cng f)) st x in dom o1 holds
(HomQuot f) . (o1 . x) = o2 . ((HomQuot f) * x)
A5:
(
len (signature U1) = len the
charact of
U1 &
len (signature (QuotUnivAlg U1,(Cng f))) = len the
charact of
(QuotUnivAlg U1,(Cng f)) )
by UNIALG_1:def 11;
A6:
(
dom the
charact of
(QuotUnivAlg U1,(Cng f)) = Seg (len the charact of (QuotUnivAlg U1,(Cng f))) &
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 5;
A7:
dom o1 =
(arity o1) -tuples_on the
carrier of
U1
by MARGREL1:58
.=
{ p where p is Element of the carrier of U1 * : len p = arity o1 }
by FINSEQ_2:def 4
;
let oq be
operation of
(QuotUnivAlg U1,(Cng f));
for o2 being operation of U2 st oq = the charact of (QuotUnivAlg U1,(Cng f)) . n & o2 = the charact of U2 . n holds
for x being FinSequence of (QuotUnivAlg U1,(Cng f)) st x in dom oq holds
(HomQuot f) . (oq . x) = o2 . ((HomQuot f) * x)let o2 be
operation of
U2;
( oq = the charact of (QuotUnivAlg U1,(Cng f)) . n & o2 = the charact of U2 . n implies for x being FinSequence of (QuotUnivAlg U1,(Cng f)) st x in dom oq holds
(HomQuot f) . (oq . x) = o2 . ((HomQuot f) * x) )
assume that A8:
oq = the
charact of
(QuotUnivAlg U1,(Cng f)) . n
and A9:
o2 = the
charact of
U2 . n
;
for x being FinSequence of (QuotUnivAlg U1,(Cng f)) st x in dom oq holds
(HomQuot f) . (oq . x) = o2 . ((HomQuot f) * x)
let x be
FinSequence of
(QuotUnivAlg U1,(Cng f));
( x in dom oq implies (HomQuot f) . (oq . x) = o2 . ((HomQuot f) * x) )
assume A10:
x in dom oq
;
(HomQuot f) . (oq . x) = o2 . ((HomQuot f) * x)
reconsider x1 =
x as
FinSequence of
Class (Cng f) ;
reconsider x1 =
x1 as
Element of
(Class (Cng f)) * by FINSEQ_1:def 11;
consider y being
FinSequence of
U1 such that A11:
y is_representatives_FS x1
by FINSEQ_3:131;
reconsider y =
y as
Element of the
carrier of
U1 * by FINSEQ_1:def 11;
A12:
len x1 = len y
by A11, FINSEQ_3:def 4;
then A13:
len ((HomQuot f) * x) = len y
by FINSEQ_3:129;
A14:
len y = len (f * y)
by FINSEQ_3:129;
A15:
now let m be
Nat;
( m in Seg (len y) implies ((HomQuot f) * x) . m = (f * y) . m )assume A16:
m in Seg (len y)
;
((HomQuot f) * x) . m = (f * y) . mthen A17:
m in dom ((HomQuot 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 the
carrier of
U1 by FINSEQ_2:13;
x1 . m = Class (Cng f),
(y . m)
by A11, A19, FINSEQ_3:def 4;
hence ((HomQuot f) * x) . m =
(HomQuot f) . (Class (Cng f),ym)
by A17, FINSEQ_3:129
.=
f . (y . m)
by A1, Def17
.=
(f * y) . m
by A18, FINSEQ_3:129
;
verum end;
dom ((HomQuot f) * x) = Seg (len y)
by A13, FINSEQ_1:def 3;
then A20:
o2 . ((HomQuot f) * x) = o2 . (f * y)
by A13, A14, A15, FINSEQ_2:10;
A21:
oq = QuotOp o1,
(Cng f)
by A4, A8, Def13;
then dom oq =
(arity o1) -tuples_on (Class (Cng f))
by Def12
.=
{ w where w is Element of (Class (Cng f)) * : len w = arity o1 }
by FINSEQ_2:def 4
;
then
ex
w being
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 5;
then reconsider o1y =
o1 . y as
Element of the
carrier of
U1 ;
(HomQuot f) . (oq . x) =
(HomQuot f) . (Class (Cng f),o1y)
by A10, A11, A21, Def12
.=
f . (o1 . y)
by A1, Def17
;
hence
(HomQuot f) . (oq . x) = o2 . ((HomQuot f) * x)
by A1, A3, A4, A9, A6, A5, A22, A20, Def1;
verum
end;
A23:
dom (HomQuot f) = the carrier of (QuotUnivAlg U1,(Cng f))
by FUNCT_2:def 1;
HomQuot f is one-to-one
proof
let x be
set ;
FUNCT_1:def 8 for b1 being set holds
( not x in proj1 (HomQuot f) or not b1 in proj1 (HomQuot f) or not (HomQuot f) . x = (HomQuot f) . b1 or x = b1 )let y be
set ;
( not x in proj1 (HomQuot f) or not y in proj1 (HomQuot f) or not (HomQuot f) . x = (HomQuot f) . y or x = y )
assume that A24:
x in dom (HomQuot f)
and A25:
y in dom (HomQuot f)
and A26:
(HomQuot f) . x = (HomQuot f) . y
;
x = y
reconsider x1 =
x,
y1 =
y as
Subset of the
carrier of
U1 by A23, A24, A25;
consider a being
set such that A27:
a in the
carrier of
U1
and A28:
x1 = Class (Cng f),
a
by A24, EQREL_1:def 5;
reconsider a =
a as
Element of the
carrier of
U1 by A27;
consider b being
set such that A29:
b in the
carrier of
U1
and A30:
y1 = Class (Cng f),
b
by A25, EQREL_1:def 5;
reconsider b =
b as
Element of the
carrier of
U1 by A29;
A31:
(HomQuot f) . y1 = f . b
by A1, A30, Def17;
(HomQuot f) . x1 = f . a
by A1, A28, Def17;
then
[a,b] in Cng f
by A1, A26, A31, Def16;
hence
x = y
by A28, A30, EQREL_1:44;
verum
end;
hence
HomQuot f is_monomorphism QuotUnivAlg U1,(Cng f),U2
by A2, Def2; verum