let U1, U2 be Universal_Algebra; for f being Function of U1,U2 st f is_homomorphism holds
( HomQuot f is_homomorphism & HomQuot f is_monomorphism )
let f be Function of U1,U2; ( f is_homomorphism implies ( HomQuot f is_homomorphism & HomQuot f is_monomorphism ) )
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
; ( HomQuot f is_homomorphism & HomQuot f is_monomorphism )
thus A2:
HomQuot f is_homomorphism
HomQuot f is_monomorphism proof
Nat_Hom (
U1,
(Cng f))
is_homomorphism
by Th17;
then
U1,
QuotUnivAlg (
U1,
(Cng f))
are_similar
;
then A3:
signature U1 = signature (QuotUnivAlg (U1,(Cng f)))
;
U1,
U2 are_similar
by A1;
then
signature U2 = signature (QuotUnivAlg (U1,(Cng f)))
by A3;
hence
QuotUnivAlg (
U1,
(Cng f)),
U2 are_similar
;
ALG_1:def 1 for n being 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
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 4;
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 3;
A7:
dom o1 =
(arity o1) -tuples_on the
carrier of
U1
by MARGREL1:22
.=
{ 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:122;
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:120;
A14:
len y = len (f * y)
by FINSEQ_3:120;
A15:
now for m being Nat st m in Seg (len y) holds
((HomQuot f) * x) . m = (f * y) . mlet 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:11;
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:120
.=
f . (y . m)
by A1, Def13
.=
(f * y) . m
by A18, FINSEQ_3:120
;
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: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 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 3;
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, Def8
.=
f . (o1 . y)
by A1, Def13
;
hence
(HomQuot f) . (oq . x) = o2 . ((HomQuot f) * x)
by A1, A3, A4, A9, A6, A5, A22, A20;
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,
y be
object ;
FUNCT_1:def 4 ( not x in dom (HomQuot f) or not y in dom (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
object such that A27:
a in the
carrier of
U1
and A28:
x1 = Class (
(Cng f),
a)
by A24, EQREL_1:def 3;
reconsider a =
a as
Element of the
carrier of
U1 by A27;
consider b being
object such that A29:
b in the
carrier of
U1
and A30:
y1 = Class (
(Cng f),
b)
by A25, EQREL_1:def 3;
reconsider b =
b as
Element of the
carrier of
U1 by A29;
A31:
(HomQuot f) . y1 = f . b
by A1, A30, Def13;
(HomQuot f) . x1 = f . a
by A1, A28, Def13;
then
[a,b] in Cng f
by A1, A26, A31, Def12;
hence
x = y
by A28, A30, EQREL_1:35;
verum
end;
hence
HomQuot f is_monomorphism
by A2; verum