ALG_1: Homomorphisms of algebras. Quotient Universal Algebra

:: Homomorphisms of algebras. Quotient Universal Algebra
:: by Ma{\l}gorzata Korolkiewicz
::
:: Received October 12, 1993
:: Copyright (c) 1993 Association of Mizar Users

theorem Th1: :: ALG_1:1

for D1, D2 being non empty set
for p being FinSequence of D1
for f being Function of D1,D2 holds
( dom (f * p) = dom p & len (f * p) = len p & ( for n being Nat st n in dom (f * p) holds
(f * p) . n = f . (p . n) ) )

proof end;

theorem Th2: :: ALG_1:2

for U1 being Universal_Algebra
for B being non empty Subset of U1 st B = the carrier of U1 holds
Opers U1,B = the charact of U1

proof end;

theorem :: ALG_1:3

for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds f * (<*> the carrier of U1) = <*> the carrier of U2 ;

theorem Th4: :: ALG_1:4

for U1 being Universal_Algebra
for a being FinSequence of U1 holds (id the carrier of U1) * a = a

proof end;

theorem Th5: :: ALG_1:5

for U1, U2, U3 being Universal_Algebra
for h1 being Function of U1,U2
for h2 being Function of U2,U3
for a being FinSequence of U1 holds h2 * (h1 * a) = (h2 * h1) * a

proof end;

definition

let U1, U2 be Universal_Algebra;
let f be Function of U1,U2;
pred f is_homomorphism U1,U2 means :Def1: :: ALG_1:def 1
( 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) ) );

end;

:: deftheorem Def1 defines is_homomorphism ALG_1:def 1 :

definition

let U1, U2 be Universal_Algebra;
let f be Function of U1,U2;
pred f is_monomorphism U1,U2 means :Def2: :: ALG_1:def 2
( f is_homomorphism U1,U2 & f is one-to-one );
pred f is_epimorphism U1,U2 means :Def3: :: ALG_1:def 3
( f is_homomorphism U1,U2 & rng f = the carrier of U2 );

end;

:: deftheorem Def2 defines is_monomorphism ALG_1:def 2 :

:: deftheorem Def3 defines is_epimorphism ALG_1:def 3 :

definition

let U1, U2 be Universal_Algebra;
let f be Function of U1,U2;
pred f is_isomorphism U1,U2 means :Def4: :: ALG_1:def 4
( f is_monomorphism U1,U2 & f is_epimorphism U1,U2 );

end;

:: deftheorem Def4 defines is_isomorphism ALG_1:def 4 :

definition

let U1, U2 be Universal_Algebra;
pred U1,U2 are_isomorphic means :Def5: :: ALG_1:def 5
ex f being Function of U1,U2 st f is_isomorphism U1,U2;

end;

:: deftheorem Def5 defines are_isomorphic ALG_1:def 5 :

theorem Th6: :: ALG_1:6

for U1 being Universal_Algebra holds id the carrier of U1 is_homomorphism U1,U1

proof end;

theorem Th7: :: ALG_1:7

for U1, U2, U3 being Universal_Algebra
for h1 being Function of U1,U2
for h2 being Function of U2,U3 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U2,U3 holds
h2 * h1 is_homomorphism U1,U3

proof end;

theorem Th8: :: ALG_1:8

for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_isomorphism U1,U2 iff ( f is_homomorphism U1,U2 & rng f = the carrier of U2 & f is one-to-one ) )

proof end;

theorem Th9: :: ALG_1:9

for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_isomorphism U1,U2 holds
( dom f = the carrier of U1 & rng f = the carrier of U2 )

proof end;

theorem Th10: :: ALG_1:10

for U1, U2 being Universal_Algebra
for h being Function of U1,U2
for h1 being Function of U2,U1 st h is_isomorphism U1,U2 & h1 = h " holds
h1 is_homomorphism U2,U1

proof end;

theorem Th11: :: ALG_1:11

for U1, U2 being Universal_Algebra
for h being Function of U1,U2
for h1 being Function of U2,U1 st h is_isomorphism U1,U2 & h1 = h " holds
h1 is_isomorphism U2,U1

proof end;

theorem Th12: :: ALG_1:12

for U1, U2, U3 being Universal_Algebra
for h being Function of U1,U2
for h1 being Function of U2,U3 st h is_isomorphism U1,U2 & h1 is_isomorphism U2,U3 holds
h1 * h is_isomorphism U1,U3

proof end;

theorem :: ALG_1:13

for U1 being Universal_Algebra holds U1,U1 are_isomorphic

proof end;

theorem :: ALG_1:14

for U1, U2 being Universal_Algebra st U1,U2 are_isomorphic holds
U2,U1 are_isomorphic

proof end;

theorem :: ALG_1:15

for U1, U2, U3 being Universal_Algebra st U1,U2 are_isomorphic & U2,U3 are_isomorphic holds
U1,U3 are_isomorphic

proof end;

definition

let U1, U2 be Universal_Algebra;
let f be Function of U1,U2;
assume A1: f is_homomorphism U1,U2 ;
func Image f -> strict SubAlgebra of U2 means :Def6: :: ALG_1:def 6
the carrier of it = f .: the carrier of U1;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Image ALG_1:def 6 :

theorem :: ALG_1:16

for U1, U2 being Universal_Algebra
for h being Function of U1,U2 st h is_homomorphism U1,U2 holds
rng h = the carrier of (Image h)

proof end;

theorem :: ALG_1:17

for U1 being Universal_Algebra
for U2 being strict Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism U1,U2 holds
( f is_epimorphism U1,U2 iff Image f = U2 )

proof end;

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 D be non empty set ;
let R be Relation of D;
canceled;
canceled;
func ExtendRel R -> Relation of D * means :Def9: :: ALG_1:def 9
for x, y being FinSequence of D holds
( [x,y] in it iff ( len x = len y & ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem ALG_1:def 7 :

:: deftheorem ALG_1:def 8 :

:: deftheorem Def9 defines ExtendRel ALG_1:def 9 :

theorem Th18: :: ALG_1:18

for D being non empty set holds ExtendRel (id D) = id (D * )

proof end;

definition

let U1 be Universal_Algebra;
mode Congruence of U1 -> Equivalence_Relation of U1 means :Def10: :: ALG_1:def 10
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 it holds
[(o1 . x),(o1 . y)] in it;
existence

proof end;

end;

:: deftheorem Def10 defines Congruence ALG_1:def 10 :

definition

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

end;

:: deftheorem Def11 defines is_representatives_FS ALG_1:def 11 :

theorem Th19: :: ALG_1:19

for D being non empty set
for R being Equivalence_Relation of D
for y being FinSequence of Class R ex x being FinSequence of D st x is_representatives_FS y

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines QuotOp ALG_1:def 12 :

definition

let U1 be Universal_Algebra;
let E be Congruence of U1;
func QuotOpSeq U1,E -> PFuncFinSequence of (Class E) means :Def13: :: ALG_1:def 13
( len it = len the charact of U1 & ( for n being Element of NAT st n in dom it holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
it . n = QuotOp o1,E ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines QuotOpSeq ALG_1:def 13 :

theorem Th20: :: ALG_1:20

for U1 being Universal_Algebra
for E being Congruence of U1 holds UAStr(# (Class E),(QuotOpSeq U1,E) #) is strict Universal_Algebra

proof end;

definition

let U1 be Universal_Algebra;
let E be Congruence of U1;
func QuotUnivAlg U1,E -> strict Universal_Algebra equals :: ALG_1:def 14
UAStr(# (Class E),(QuotOpSeq U1,E) #);
coherence by Th20;

end;

:: deftheorem defines QuotUnivAlg ALG_1:def 14 :

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: :: ALG_1:def 15
for u being Element of U1 holds it . u = Class E,u;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines Nat_Hom ALG_1:def 15 :

theorem Th21: :: ALG_1:21

for U1 being Universal_Algebra
for E being Congruence of U1 holds Nat_Hom U1,E is_homomorphism U1, QuotUnivAlg U1,E

proof end;

theorem :: ALG_1:22

for U1 being Universal_Algebra
for E being Congruence of U1 holds Nat_Hom U1,E is_epimorphism U1, QuotUnivAlg U1,E

proof end;

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: :: ALG_1:def 16
for a, b being Element of U1 holds
( [a,b] in it iff f . a = f . b );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines Cng ALG_1:def 16 :

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: :: ALG_1:def 17
for a being Element of U1 holds it . (Class (Cng f),a) = f . a;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines HomQuot ALG_1:def 17 :

theorem Th23: :: ALG_1:23

for U1, U2 being 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 )

proof end;

theorem Th24: :: ALG_1:24

for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_epimorphism U1,U2 holds
HomQuot f is_isomorphism QuotUnivAlg U1,(Cng f),U2

proof end;

theorem :: ALG_1:25

for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_epimorphism U1,U2 holds
QuotUnivAlg U1,(Cng f),U2 are_isomorphic

proof end;