:: by Ma{\l}gorzata Korolkiewicz

::

:: Received October 12, 1993

:: Copyright (c) 1993-2021 Association of Mizar Users

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

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:2

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

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;

end;
let f be Function of U1,U2;

pred f is_homomorphism means :: ALG_1:def 1

( U1,U2 are_similar & ( for n being 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) ) );

( U1,U2 are_similar & ( for n being 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 defines is_homomorphism ALG_1:def 1 :

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 holds

( f is_homomorphism iff ( U1,U2 are_similar & ( for n being 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) ) ) );

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 holds

( f is_homomorphism iff ( U1,U2 are_similar & ( for n being 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 defines is_monomorphism ALG_1:def 2 :

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 holds

( f is_monomorphism iff ( f is_homomorphism & f is one-to-one ) );

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 holds

( f is_monomorphism iff ( f is_homomorphism & f is one-to-one ) );

:: deftheorem defines is_epimorphism ALG_1:def 3 :

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 holds

( f is_epimorphism iff ( f is_homomorphism & rng f = the carrier of U2 ) );

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 holds

( f is_epimorphism iff ( f is_homomorphism & rng f = the carrier of U2 ) );

:: deftheorem defines is_isomorphism ALG_1:def 4 :

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 holds

( f is_isomorphism iff ( f is_monomorphism & f is_epimorphism ) );

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 holds

( f is_isomorphism iff ( f is_monomorphism & f is_epimorphism ) );

:: deftheorem 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 );

for U1, U2 being Universal_Algebra holds

( U1,U2 are_isomorphic iff ex f being Function of U1,U2 st f is_isomorphism );

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 & h2 is_homomorphism holds

h2 * h1 is_homomorphism

for h1 being Function of U1,U2

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

h2 * h1 is_homomorphism

proof end;

theorem Th7: :: ALG_1:7

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 holds

( f is_isomorphism iff ( f is_homomorphism & rng f = the carrier of U2 & f is one-to-one ) )

for f being Function of U1,U2 holds

( f is_isomorphism iff ( f is_homomorphism & rng f = the carrier of U2 & f is one-to-one ) )

proof end;

theorem Th8: :: ALG_1:8

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 st f is_isomorphism holds

( dom f = the carrier of U1 & rng f = the carrier of U2 )

for f being Function of U1,U2 st f is_isomorphism holds

( dom f = the carrier of U1 & rng f = the carrier of U2 )

proof end;

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 & h1 = h " holds

h1 is_homomorphism

for h being Function of U1,U2

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

h1 is_homomorphism

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 & h1 = h " holds

h1 is_isomorphism

for h being Function of U1,U2

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

h1 is_isomorphism

proof end;

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 & h1 is_isomorphism holds

h1 * h is_isomorphism

for h being Function of U1,U2

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

h1 * h is_isomorphism

proof end;

theorem :: ALG_1:14

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

U1,U3 are_isomorphic

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 ;

ex b_{1} being strict SubAlgebra of U2 st the carrier of b_{1} = f .: the carrier of U1

for b_{1}, b_{2} being strict SubAlgebra of U2 st the carrier of b_{1} = f .: the carrier of U1 & the carrier of b_{2} = f .: the carrier of U1 holds

b_{1} = b_{2}

end;
let f be Function of U1,U2;

assume A1: f is_homomorphism ;

func Image f -> strict SubAlgebra of U2 means :Def6: :: ALG_1:def 6

the carrier of it = f .: the carrier of U1;

existence the carrier of it = f .: the carrier of U1;

ex b

proof end;

uniqueness for b

b

proof 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 holds

for b_{4} being strict SubAlgebra of U2 holds

( b_{4} = Image f iff the carrier of b_{4} = f .: the carrier of U1 );

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 st f is_homomorphism holds

for b

( b

theorem :: ALG_1:15

for U1, U2 being Universal_Algebra

for h being Function of U1,U2 st h is_homomorphism holds

rng h = the carrier of (Image h)

for h being Function of U1,U2 st h is_homomorphism holds

rng h = the carrier of (Image h)

proof end;

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 holds

( f is_epimorphism iff Image f = U2 )

for U2 being strict Universal_Algebra

for f being Function of U1,U2 st f is_homomorphism holds

( f is_epimorphism 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;
mode Relation of U1 is Relation of the carrier of U1;

mode Equivalence_Relation of U1 is Equivalence_Relation of the carrier of U1;

definition

let U1 be Universal_Algebra;

ex b_{1} being Equivalence_Relation of U1 st

for n being 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 b_{1} holds

[(o1 . x),(o1 . y)] in b_{1}

end;
mode Congruence of U1 -> Equivalence_Relation of U1 means :Def7: :: ALG_1:def 7

for n being 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 for n being 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;

ex b

for n being 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 b

[(o1 . x),(o1 . y)] in b

proof end;

:: deftheorem Def7 defines Congruence ALG_1:def 7 :

for U1 being Universal_Algebra

for b_{2} being Equivalence_Relation of U1 holds

( b_{2} is Congruence of U1 iff for n being 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 b_{2} holds

[(o1 . x),(o1 . y)] in b_{2} );

for U1 being Universal_Algebra

for b

( b

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 b

[(o1 . x),(o1 . y)] in b

definition

let U1 be Universal_Algebra;

let E be Congruence of U1;

let o be operation of U1;

ex b_{1} being non empty homogeneous quasi_total PartFunc of ((Class E) *),(Class E) st

( dom b_{1} = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom b_{1} holds

for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds

b_{1} . y = Class (E,(o . x)) ) )

for b_{1}, b_{2} being non empty homogeneous quasi_total PartFunc of ((Class E) *),(Class E) st dom b_{1} = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom b_{1} holds

for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds

b_{1} . y = Class (E,(o . x)) ) & dom b_{2} = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom b_{2} holds

for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds

b_{2} . y = Class (E,(o . x)) ) holds

b_{1} = b_{2}

end;
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) & ( 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 ( 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)) ) );

ex b

( dom b

for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds

b

proof end;

uniqueness for b

for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds

b

for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds

b

b

proof 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 b_{4} being non empty homogeneous quasi_total PartFunc of ((Class E) *),(Class E) holds

( b_{4} = QuotOp (o,E) iff ( dom b_{4} = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom b_{4} holds

for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds

b_{4} . y = Class (E,(o . x)) ) ) );

for U1 being Universal_Algebra

for E being Congruence of U1

for o being operation of U1

for b

( b

for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds

b

definition

let U1 be Universal_Algebra;

let E be Congruence of U1;

ex b_{1} being PFuncFinSequence of (Class E) st

( len b_{1} = len the charact of U1 & ( for n being Nat st n in dom b_{1} holds

for o1 being operation of U1 st the charact of U1 . n = o1 holds

b_{1} . n = QuotOp (o1,E) ) )

for b_{1}, b_{2} being PFuncFinSequence of (Class E) st len b_{1} = len the charact of U1 & ( for n being Nat st n in dom b_{1} holds

for o1 being operation of U1 st the charact of U1 . n = o1 holds

b_{1} . n = QuotOp (o1,E) ) & len b_{2} = len the charact of U1 & ( for n being Nat st n in dom b_{2} holds

for o1 being operation of U1 st the charact of U1 . n = o1 holds

b_{2} . n = QuotOp (o1,E) ) holds

b_{1} = b_{2}

end;
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 & ( for n being 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 ( len it = len the charact of U1 & ( for n being 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) ) );

ex b

( len b

for o1 being operation of U1 st the charact of U1 . n = o1 holds

b

proof end;

uniqueness for b

for o1 being operation of U1 st the charact of U1 . n = o1 holds

b

for o1 being operation of U1 st the charact of U1 . n = o1 holds

b

b

proof end;

:: deftheorem Def9 defines QuotOpSeq ALG_1:def 9 :

for U1 being Universal_Algebra

for E being Congruence of U1

for b_{3} being PFuncFinSequence of (Class E) holds

( b_{3} = QuotOpSeq (U1,E) iff ( len b_{3} = len the charact of U1 & ( for n being Nat st n in dom b_{3} holds

for o1 being operation of U1 st the charact of U1 . n = o1 holds

b_{3} . n = QuotOp (o1,E) ) ) );

for U1 being Universal_Algebra

for E being Congruence of U1

for b

( b

for o1 being operation of U1 st the charact of U1 . n = o1 holds

b

definition

let U1 be Universal_Algebra;

let E be Congruence of U1;

UAStr(# (Class E),(QuotOpSeq (U1,E)) #) is strict Universal_Algebra

end;
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)) #);

UAStr(# (Class E),(QuotOpSeq (U1,E)) #) is strict Universal_Algebra

proof 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)) #);

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;

ex b_{1} being Function of U1,(QuotUnivAlg (U1,E)) st

for u being Element of U1 holds b_{1} . u = Class (E,u)

for b_{1}, b_{2} being Function of U1,(QuotUnivAlg (U1,E)) st ( for u being Element of U1 holds b_{1} . u = Class (E,u) ) & ( for u being Element of U1 holds b_{2} . u = Class (E,u) ) holds

b_{1} = b_{2}

end;
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 for u being Element of U1 holds it . u = Class (E,u);

ex b

for u being Element of U1 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines Nat_Hom ALG_1:def 11 :

for U1 being Universal_Algebra

for E being Congruence of U1

for b_{3} being Function of U1,(QuotUnivAlg (U1,E)) holds

( b_{3} = Nat_Hom (U1,E) iff for u being Element of U1 holds b_{3} . u = Class (E,u) );

for U1 being Universal_Algebra

for E being Congruence of U1

for b

( b

definition

let U1, U2 be Universal_Algebra;

let f be Function of U1,U2;

assume A1: f is_homomorphism ;

ex b_{1} being Congruence of U1 st

for a, b being Element of U1 holds

( [a,b] in b_{1} iff f . a = f . b )

for b_{1}, b_{2} being Congruence of U1 st ( for a, b being Element of U1 holds

( [a,b] in b_{1} iff f . a = f . b ) ) & ( for a, b being Element of U1 holds

( [a,b] in b_{2} iff f . a = f . b ) ) holds

b_{1} = b_{2}

end;
let f be Function of U1,U2;

assume A1: f is_homomorphism ;

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 for a, b being Element of U1 holds

( [a,b] in it iff f . a = f . b );

ex b

for a, b being Element of U1 holds

( [a,b] in b

proof end;

uniqueness for b

( [a,b] in b

( [a,b] in b

b

proof 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 holds

for b_{4} being Congruence of U1 holds

( b_{4} = Cng f iff for a, b being Element of U1 holds

( [a,b] in b_{4} iff f . a = f . b ) );

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 st f is_homomorphism holds

for b

( b

( [a,b] in b

definition

let U1, U2 be Universal_Algebra;

let f be Function of U1,U2;

assume A1: f is_homomorphism ;

ex b_{1} being Function of (QuotUnivAlg (U1,(Cng f))),U2 st

for a being Element of U1 holds b_{1} . (Class ((Cng f),a)) = f . a

for b_{1}, b_{2} being Function of (QuotUnivAlg (U1,(Cng f))),U2 st ( for a being Element of U1 holds b_{1} . (Class ((Cng f),a)) = f . a ) & ( for a being Element of U1 holds b_{2} . (Class ((Cng f),a)) = f . a ) holds

b_{1} = b_{2}

end;
let f be Function of U1,U2;

assume A1: f is_homomorphism ;

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

ex b

for a being Element of U1 holds b

proof end;

uniqueness for b

b

proof 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 holds

for b_{4} being Function of (QuotUnivAlg (U1,(Cng f))),U2 holds

( b_{4} = HomQuot f iff for a being Element of U1 holds b_{4} . (Class ((Cng f),a)) = f . a );

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 st f is_homomorphism holds

for b

( b

theorem Th19: :: ALG_1:19

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 st f is_homomorphism holds

( HomQuot f is_homomorphism & HomQuot f is_monomorphism )

for f being Function of U1,U2 st f is_homomorphism holds

( HomQuot f is_homomorphism & HomQuot f is_monomorphism )

proof end;

:: 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 holds

HomQuot f is_isomorphism

for f being Function of U1,U2 st f is_epimorphism holds

HomQuot f is_isomorphism

proof end;

theorem :: ALG_1:21

for U1, U2 being Universal_Algebra

for f being Function of U1,U2 st f is_epimorphism holds

QuotUnivAlg (U1,(Cng f)),U2 are_isomorphic

for f being Function of U1,U2 st f is_epimorphism holds

QuotUnivAlg (U1,(Cng f)),U2 are_isomorphic

proof end;