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


begin

theorem Th1: :: ALG_1:1
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
proofend;

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

theorem Th3: :: ALG_1:3
for U1 being Universal_Algebra
for a being FinSequence of U1 holds (id the carrier of U1) * a = a
proofend;

theorem Th4: :: ALG_1:4
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
proofend;

definition
let U1, U2 be Universal_Algebra;
let f be Function of U1,U2;
predf is_homomorphism U1,U2 means :Def1: :: ALG_1:def 1
( U1,U2 are_similar &amp; ( 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 &amp; 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_:_
 for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_homomorphism U1,U2 iff ( U1,U2 are_similar &amp; ( 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 &amp; 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) ) ) );

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

:: 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 &amp; 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 &amp; rng f = the carrier of U2 ) );

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

:: 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 &amp; f is_epimorphism U1,U2 ) );

definition
let U1, U2 be Universal_Algebra;
predU1,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_:_
 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 Th5: :: ALG_1:5
for U1 being Universal_Algebra holds id the carrier of U1 is_homomorphism U1,U1
proofend;

theorem Th6: :: ALG_1:6
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 &amp; h2 is_homomorphism U2,U3 holds
h2 * h1 is_homomorphism U1,U3
proofend;

theorem Th7: :: ALG_1:7
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 &amp; rng f = the carrier of U2 &amp; f is one-to-one ) )
proofend;

theorem Th8: :: ALG_1:8
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 &amp; rng f = the carrier of U2 )
proofend;

theorem Th9: :: ALG_1:9
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 &amp; h1 = h " holds
h1 is_homomorphism U2,U1
proofend;

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 &amp; h1 = h " holds
h1 is_isomorphism U2,U1
proofend;

theorem Th11: :: ALG_1:11
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 &amp; h1 is_isomorphism U2,U3 holds
h1 * h is_isomorphism U1,U3
proofend;

theorem :: ALG_1:12
for U1 being Universal_Algebra holds U1,U1 are_isomorphic
proofend;

theorem :: ALG_1:13
for U1, U2 being Universal_Algebra st U1,U2 are_isomorphic holds
U2,U1 are_isomorphic
proofend;

theorem :: ALG_1:14
for U1, U2, U3 being Universal_Algebra st U1,U2 are_isomorphic &amp; U2,U3 are_isomorphic holds
U1,U3 are_isomorphic
proofend;

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
 ex b1 being strict SubAlgebra of U2 st the carrier of b1 = f .: the carrier of U1
proofend;
uniqueness
 for b1, b2 being strict SubAlgebra of U2 st the carrier of b1 = f .: the carrier of U1 &amp; the carrier of b2 = f .: the carrier of U1 holds
b1 = b2
proofend;
end;

:: 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 :: ALG_1:15
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)
proofend;

theorem :: ALG_1:16
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 )
proofend;

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 be Universal_Algebra;
mode Congruence of U1 ->  Equivalence_Relation of U1 means :Def7: :: ALG_1:def 7
 for n being Element of NAT
for o1 being operation of U1 st n in dom the charact of U1 &amp; o1 = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o1 &amp; y in dom o1 &amp; [x,y] in ExtendRel it holds
[(o1 . x),(o1 . y)] in it;
existence
 ex b1 being Equivalence_Relation of U1 st
for n being Element of NAT
for o1 being operation of U1 st n in dom the charact of U1 &amp; o1 = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o1 &amp; y in dom o1 &amp; [x,y] in ExtendRel b1 holds
[(o1 . x),(o1 . y)] in b1
proofend;
end;

:: deftheorem Def7 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 &amp; o1 = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o1 &amp; y in dom o1 &amp; [x,y] in ExtendRel b2 holds
[(o1 . x),(o1 . y)] in b2 );

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 :Def8: :: ALG_1:def 8
( dom it = (arity o) -tuples_on (Class E) &amp; ( 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
 ex b1 being non empty homogeneous quasi_total PartFunc of ((Class E) *),(Class E) st
( dom b1 = (arity o) -tuples_on (Class E) &amp; ( for y being FinSequence of Class E st y in dom b1 holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
b1 . y = Class (E,(o . x)) ) )
proofend;
uniqueness
 for b1, b2 being non empty homogeneous quasi_total PartFunc of ((Class E) *),(Class E) st dom b1 = (arity o) -tuples_on (Class E) &amp; ( for y being FinSequence of Class E st y in dom b1 holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
b1 . y = Class (E,(o . x)) ) &amp; dom b2 = (arity o) -tuples_on (Class E) &amp; ( for y being FinSequence of Class E st y in dom b2 holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
b2 . y = Class (E,(o . x)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines QuotOp ALG_1:def_8_:_
 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) &amp; ( 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)) ) ) );

definition
let U1 be Universal_Algebra;
let E be Congruence of U1;
func QuotOpSeq (U1,E) ->  PFuncFinSequence of (Class E) means :Def9: :: ALG_1:def 9
( len it = len the charact of U1 &amp; ( 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
 ex b1 being PFuncFinSequence of (Class E) st
( len b1 = len the charact of U1 &amp; ( for n being Element of NAT st n in dom b1 holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
b1 . n = QuotOp (o1,E) ) )
proofend;
uniqueness
 for b1, b2 being PFuncFinSequence of (Class E) st len b1 = len the charact of U1 &amp; ( for n being Element of NAT st n in dom b1 holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
b1 . n = QuotOp (o1,E) ) &amp; len b2 = len the charact of U1 &amp; ( for n being Element of NAT st n in dom b2 holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
b2 . n = QuotOp (o1,E) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines QuotOpSeq ALG_1:def_9_:_
 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 &amp; ( 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) ) ) );

definition
let U1 be Universal_Algebra;
let E be Congruence of U1;
func QuotUnivAlg (U1,E) ->  strict Universal_Algebra equals :: ALG_1:def 10
 UAStr(# (Class E),(QuotOpSeq (U1,E)) #);
coherence
 UAStr(# (Class E),(QuotOpSeq (U1,E)) #) is strict Universal_Algebra
proofend;
end;

:: deftheorem  defines QuotUnivAlg ALG_1:def_10_:_
 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 :Def11: :: ALG_1:def 11
 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)
proofend;
uniqueness
 for b1, b2 being Function of U1,(QuotUnivAlg (U1,E)) st ( for u being Element of U1 holds b1 . u = Class (E,u) ) &amp; ( for u being Element of U1 holds b2 . u = Class (E,u) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines Nat_Hom ALG_1:def_11_:_
 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 Th17: :: ALG_1:17
for U1 being Universal_Algebra
for E being Congruence of U1 holds Nat_Hom (U1,E) is_homomorphism U1, QuotUnivAlg (U1,E)
proofend;

theorem :: ALG_1:18
for U1 being Universal_Algebra
for E being Congruence of U1 holds Nat_Hom (U1,E) is_epimorphism U1, QuotUnivAlg (U1,E)
proofend;

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 :Def12: :: ALG_1:def 12
 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 )
proofend;
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 ) ) &amp; ( for a, b being Element of U1 holds
( [a,b] in b2 iff f . a = f . b ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines Cng ALG_1:def_12_:_
 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 :Def13: :: ALG_1:def 13
 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
proofend;
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 ) &amp; ( for a being Element of U1 holds b2 . (Class ((Cng f),a)) = f . a ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines HomQuot ALG_1:def_13_:_
 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 Th19: :: ALG_1:19
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 &amp; HomQuot f is_monomorphism QuotUnivAlg (U1,(Cng f)),U2 )
proofend;

:: [WP: ] First_isomorphism_theorem_for_universal_algebras
theorem Th20: :: ALG_1:20
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
proofend;

theorem :: ALG_1:21
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
proofend;