begin
theorem
canceled;
theorem Th2:
theorem
theorem Th4:
theorem Th5:
:: deftheorem Def1 defines is_homomorphism ALG_1:def 1 :
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_homomorphism U1,U2 iff ( U1,U2 are_similar & ( for n being Element of NAT st n in dom the charact of U1 holds
for o1 being operation of U1
for o2 being operation of U2 st o1 = the charact of U1 . n & o2 = the charact of U2 . n holds
for x being FinSequence of U1 st x in dom o1 holds
f . (o1 . x) = o2 . (f * x) ) ) );
:: deftheorem Def2 defines is_monomorphism ALG_1:def 2 :
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_monomorphism U1,U2 iff ( f is_homomorphism U1,U2 & f is one-to-one ) );
:: deftheorem Def3 defines is_epimorphism ALG_1:def 3 :
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_epimorphism U1,U2 iff ( f is_homomorphism U1,U2 & rng f = the carrier of U2 ) );
:: deftheorem Def4 defines is_isomorphism ALG_1:def 4 :
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_isomorphism U1,U2 iff ( f is_monomorphism U1,U2 & f is_epimorphism U1,U2 ) );
:: deftheorem Def5 defines are_isomorphic ALG_1:def 5 :
for U1, U2 being Universal_Algebra holds
( U1,U2 are_isomorphic iff ex f being Function of U1,U2 st f is_isomorphism U1,U2 );
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem
theorem
:: deftheorem Def6 defines Image ALG_1:def 6 :
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism U1,U2 holds
for b4 being strict SubAlgebra of U2 holds
( b4 = Image f iff the carrier of b4 = f .: the carrier of U1 );
theorem
theorem
begin
:: deftheorem Def10 defines Congruence ALG_1:def 7 :
for U1 being Universal_Algebra
for b2 being Equivalence_Relation of U1 holds
( b2 is Congruence of U1 iff for n being Element of NAT
for o1 being operation of U1 st n in dom the charact of U1 & o1 = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o1 & y in dom o1 & [x,y] in ExtendRel b2 holds
[(o1 . x),(o1 . y)] in b2 );
:: deftheorem ALG_1:def 8 :
canceled;
:: deftheorem ALG_1:def 9 :
canceled;
:: deftheorem ALG_1:def 10 :
canceled;
:: deftheorem ALG_1:def 11 :
canceled;
:: deftheorem Def12 defines QuotOp ALG_1:def 12 :
for U1 being Universal_Algebra
for E being Congruence of U1
for o being operation of U1
for b4 being non empty homogeneous quasi_total PartFunc of ((Class E) * ),(Class E) holds
( b4 = QuotOp o,E iff ( dom b4 = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom b4 holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
b4 . y = Class E,(o . x) ) ) );
:: deftheorem Def13 defines QuotOpSeq ALG_1:def 13 :
for U1 being Universal_Algebra
for E being Congruence of U1
for b3 being PFuncFinSequence of (Class E) holds
( b3 = QuotOpSeq U1,E iff ( len b3 = len the charact of U1 & ( for n being Element of NAT st n in dom b3 holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
b3 . n = QuotOp o1,E ) ) );
:: deftheorem defines QuotUnivAlg ALG_1:def 14 :
for U1 being Universal_Algebra
for E being Congruence of U1 holds QuotUnivAlg U1,E = UAStr(# (Class E),(QuotOpSeq U1,E) #);
definition
let U1 be
Universal_Algebra;
let E be
Congruence of
U1;
func Nat_Hom U1,
E -> Function of
U1,
(QuotUnivAlg U1,E) means :
Def15:
for
u being
Element of
U1 holds
it . u = Class E,
u;
existence
ex b1 being Function of U1,(QuotUnivAlg U1,E) st
for u being Element of U1 holds b1 . u = Class E,u
uniqueness
for b1, b2 being Function of U1,(QuotUnivAlg U1,E) st ( for u being Element of U1 holds b1 . u = Class E,u ) & ( for u being Element of U1 holds b2 . u = Class E,u ) holds
b1 = b2
end;
:: deftheorem Def15 defines Nat_Hom ALG_1:def 15 :
for U1 being Universal_Algebra
for E being Congruence of U1
for b3 being Function of U1,(QuotUnivAlg U1,E) holds
( b3 = Nat_Hom U1,E iff for u being Element of U1 holds b3 . u = Class E,u );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th21:
theorem
definition
let U1,
U2 be
Universal_Algebra;
let f be
Function of
U1,
U2;
assume A1:
f is_homomorphism U1,
U2
;
func Cng f -> Congruence of
U1 means :
Def16:
for
a,
b being
Element of
U1 holds
(
[a,b] in it iff
f . a = f . b );
existence
ex b1 being Congruence of U1 st
for a, b being Element of U1 holds
( [a,b] in b1 iff f . a = f . b )
uniqueness
for b1, b2 being Congruence of U1 st ( for a, b being Element of U1 holds
( [a,b] in b1 iff f . a = f . b ) ) & ( for a, b being Element of U1 holds
( [a,b] in b2 iff f . a = f . b ) ) holds
b1 = b2
end;
:: deftheorem Def16 defines Cng ALG_1:def 16 :
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism U1,U2 holds
for b4 being Congruence of U1 holds
( b4 = Cng f iff for a, b being Element of U1 holds
( [a,b] in b4 iff f . a = f . b ) );
definition
let U1,
U2 be
Universal_Algebra;
let f be
Function of
U1,
U2;
assume A1:
f is_homomorphism U1,
U2
;
func HomQuot f -> Function of
(QuotUnivAlg U1,(Cng f)),
U2 means :
Def17:
for
a being
Element of
U1 holds
it . (Class (Cng f),a) = f . a;
existence
ex b1 being Function of (QuotUnivAlg U1,(Cng f)),U2 st
for a being Element of U1 holds b1 . (Class (Cng f),a) = f . a
uniqueness
for b1, b2 being Function of (QuotUnivAlg U1,(Cng f)),U2 st ( for a being Element of U1 holds b1 . (Class (Cng f),a) = f . a ) & ( for a being Element of U1 holds b2 . (Class (Cng f),a) = f . a ) holds
b1 = b2
end;
:: deftheorem Def17 defines HomQuot ALG_1:def 17 :
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism U1,U2 holds
for b4 being Function of (QuotUnivAlg U1,(Cng f)),U2 holds
( b4 = HomQuot f iff for a being Element of U1 holds b4 . (Class (Cng f),a) = f . a );
theorem Th23:
theorem Th24:
theorem