:: by Artur Korni{\l}owicz

::

:: Received December 13, 1994

:: Copyright (c) 1994-2012 Association of Mizar Users

begin

definition

let UA be Universal_Algebra;

ex b_{1} being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st

for h being Function of UA,UA holds

( h in b_{1} iff h is_isomorphism UA,UA )

for b_{1}, b_{2} being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st ( for h being Function of UA,UA holds

( h in b_{1} iff h is_isomorphism UA,UA ) ) & ( for h being Function of UA,UA holds

( h in b_{2} iff h is_isomorphism UA,UA ) ) holds

b_{1} = b_{2}

end;
func UAAut UA -> FUNCTION_DOMAIN of the carrier of UA, the carrier of UA means :Def1: :: AUTALG_1:def 1

for h being Function of UA,UA holds

( h in it iff h is_isomorphism UA,UA );

existence for h being Function of UA,UA holds

( h in it iff h is_isomorphism UA,UA );

ex b

for h being Function of UA,UA holds

( h in b

proof end;

uniqueness for b

( h in b

( h in b

b

proof end;

:: deftheorem Def1 defines UAAut AUTALG_1:def 1 :

for UA being Universal_Algebra

for b_{2} being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA holds

( b_{2} = UAAut UA iff for h being Function of UA,UA holds

( h in b_{2} iff h is_isomorphism UA,UA ) );

for UA being Universal_Algebra

for b

( b

( h in b

theorem :: AUTALG_1:4

for UA being Universal_Algebra

for f, g being Function of UA,UA st f is Element of UAAut UA & g = f " holds

g is_isomorphism UA,UA

for f, g being Function of UA,UA st f is Element of UAAut UA & g = f " holds

g is_isomorphism UA,UA

proof end;

Lm1: for UA being Universal_Algebra

for f being Function of UA,UA st f is_isomorphism UA,UA holds

f " is Function of UA,UA

proof end;

definition

let UA be Universal_Algebra;

ex b_{1} being BinOp of (UAAut UA) st

for x, y being Element of UAAut UA holds b_{1} . (x,y) = y * x

for b_{1}, b_{2} being BinOp of (UAAut UA) st ( for x, y being Element of UAAut UA holds b_{1} . (x,y) = y * x ) & ( for x, y being Element of UAAut UA holds b_{2} . (x,y) = y * x ) holds

b_{1} = b_{2}

end;
func UAAutComp UA -> BinOp of (UAAut UA) means :Def2: :: AUTALG_1:def 2

for x, y being Element of UAAut UA holds it . (x,y) = y * x;

existence for x, y being Element of UAAut UA holds it . (x,y) = y * x;

ex b

for x, y being Element of UAAut UA holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines UAAutComp AUTALG_1:def 2 :

for UA being Universal_Algebra

for b_{2} being BinOp of (UAAut UA) holds

( b_{2} = UAAutComp UA iff for x, y being Element of UAAut UA holds b_{2} . (x,y) = y * x );

for UA being Universal_Algebra

for b

( b

definition
end;

:: deftheorem defines UAAutGroup AUTALG_1:def 3 :

for UA being Universal_Algebra holds UAAutGroup UA = multMagma(# (UAAut UA),(UAAutComp UA) #);

for UA being Universal_Algebra holds UAAutGroup UA = multMagma(# (UAAut UA),(UAAutComp UA) #);

registration
end;

Lm2: for UA being Universal_Algebra

for f being Element of UAAut UA holds

( dom f = rng f & dom f = the carrier of UA )

proof end;

theorem :: AUTALG_1:7

theorem :: AUTALG_1:9

for UA being Universal_Algebra

for f being Element of UAAut UA

for g being Element of (UAAutGroup UA) st f = g holds

f " = g "

for f being Element of UAAut UA

for g being Element of (UAAutGroup UA) st f = g holds

f " = g "

proof end;

begin

theorem :: AUTALG_1:10

for I being set

for A, B, C being ManySortedSet of I st A is_transformable_to B & B is_transformable_to C holds

A is_transformable_to C

for A, B, C being ManySortedSet of I st A is_transformable_to B & B is_transformable_to C holds

A is_transformable_to C

proof end;

theorem Th12: :: AUTALG_1:12

for I being set

for A, B being V2() ManySortedSet of I

for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds

( F "" is "1-1" & F "" is "onto" )

for A, B being V2() ManySortedSet of I

for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds

( F "" is "1-1" & F "" is "onto" )

proof end;

theorem :: AUTALG_1:13

for I being set

for A, B being V2() ManySortedSet of I

for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds

(F "") "" = F

for A, B being V2() ManySortedSet of I

for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds

(F "") "" = F

proof end;

theorem Th15: :: AUTALG_1:15

for I being set

for A being ManySortedSet of I

for B, C being V2() ManySortedSet of I

for F being ManySortedFunction of A,B

for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds

G ** F is "onto"

for A being ManySortedSet of I

for B, C being V2() ManySortedSet of I

for F being ManySortedFunction of A,B

for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds

G ** F is "onto"

proof end;

theorem :: AUTALG_1:16

for I being set

for A, B, C being V2() ManySortedSet of I

for F being ManySortedFunction of A,B

for G being ManySortedFunction of B,C st F is "1-1" & F is "onto" & G is "1-1" & G is "onto" holds

(G ** F) "" = (F "") ** (G "")

for A, B, C being V2() ManySortedSet of I

for F being ManySortedFunction of A,B

for G being ManySortedFunction of B,C st F is "1-1" & F is "onto" & G is "1-1" & G is "onto" holds

(G ** F) "" = (F "") ** (G "")

proof end;

theorem Th17: :: AUTALG_1:17

for I being set

for A, B being V2() ManySortedSet of I

for F being ManySortedFunction of A,B

for G being ManySortedFunction of B,A st F is "1-1" & F is "onto" & G ** F = id A holds

G = F ""

for A, B being V2() ManySortedSet of I

for F being ManySortedFunction of A,B

for G being ManySortedFunction of B,A st F is "1-1" & F is "onto" & G ** F = id A holds

G = F ""

proof end;

theorem Th18: :: AUTALG_1:18

for I being set

for A, B being ManySortedSet of I st A is_transformable_to B holds

(Funcs) (A,B) is V2()

for A, B being ManySortedSet of I st A is_transformable_to B holds

(Funcs) (A,B) is V2()

proof end;

definition

let I be set ;

let A, B be ManySortedSet of I;

assume A1: A is_transformable_to B ;

coherence

product ((Funcs) (A,B)) is non empty set

end;
let A, B be ManySortedSet of I;

assume A1: A is_transformable_to B ;

coherence

product ((Funcs) (A,B)) is non empty set

proof end;

:: deftheorem Def4 defines MSFuncs AUTALG_1:def 4 :

for I being set

for A, B being ManySortedSet of I st A is_transformable_to B holds

MSFuncs (A,B) = product ((Funcs) (A,B));

for I being set

for A, B being ManySortedSet of I st A is_transformable_to B holds

MSFuncs (A,B) = product ((Funcs) (A,B));

theorem Th19: :: AUTALG_1:19

for I being set

for A, B being ManySortedSet of I st A is_transformable_to B holds

for x being set st x in MSFuncs (A,B) holds

x is ManySortedFunction of A,B

for A, B being ManySortedSet of I st A is_transformable_to B holds

for x being set st x in MSFuncs (A,B) holds

x is ManySortedFunction of A,B

proof end;

theorem Th20: :: AUTALG_1:20

for I being set

for A, B being ManySortedSet of I st A is_transformable_to B holds

for g being ManySortedFunction of A,B holds g in MSFuncs (A,B)

for A, B being ManySortedSet of I st A is_transformable_to B holds

for g being ManySortedFunction of A,B holds g in MSFuncs (A,B)

proof end;

registration
end;

definition

let I be set ;

let D be ManySortedSet of I;

let A be non empty Subset of (MSFuncs (D,D));

:: original: Element

redefine mode Element of A -> ManySortedFunction of D,D;

coherence

for b_{1} being Element of A holds b_{1} is ManySortedFunction of D,D

end;
let D be ManySortedSet of I;

let A be non empty Subset of (MSFuncs (D,D));

:: original: Element

redefine mode Element of A -> ManySortedFunction of D,D;

coherence

for b

proof end;

registration

let I be set ;

let A be ManySortedSet of I;

coherence

id A is "onto"

id A is "1-1"

end;
let A be ManySortedSet of I;

coherence

id A is "onto"

proof end;

coherence id A is "1-1"

proof end;

begin

definition

let S be non empty non void ManySortedSign ;

let U1, U2 be non-empty MSAlgebra over S;

mode MSFunctionSet of U1,U2 is non empty Subset of (MSFuncs ( the Sorts of U1, the Sorts of U2));

end;
let U1, U2 be non-empty MSAlgebra over S;

mode MSFunctionSet of U1,U2 is non empty Subset of (MSFuncs ( the Sorts of U1, the Sorts of U2));

theorem :: AUTALG_1:21

definition

let S be non empty non void ManySortedSign ;

let U1 be non-empty MSAlgebra over S;

set T = the Sorts of U1;

ex b_{1} being MSFunctionSet of U1,U1 st

for h being ManySortedFunction of U1,U1 holds

( h in b_{1} iff h is_isomorphism U1,U1 )

for b_{1}, b_{2} being MSFunctionSet of U1,U1 st ( for h being ManySortedFunction of U1,U1 holds

( h in b_{1} iff h is_isomorphism U1,U1 ) ) & ( for h being ManySortedFunction of U1,U1 holds

( h in b_{2} iff h is_isomorphism U1,U1 ) ) holds

b_{1} = b_{2}

end;
let U1 be non-empty MSAlgebra over S;

set T = the Sorts of U1;

func MSAAut U1 -> MSFunctionSet of U1,U1 means :Def5: :: AUTALG_1:def 5

for h being ManySortedFunction of U1,U1 holds

( h in it iff h is_isomorphism U1,U1 );

existence for h being ManySortedFunction of U1,U1 holds

( h in it iff h is_isomorphism U1,U1 );

ex b

for h being ManySortedFunction of U1,U1 holds

( h in b

proof end;

uniqueness for b

( h in b

( h in b

b

proof end;

:: deftheorem Def5 defines MSAAut AUTALG_1:def 5 :

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for b_{3} being MSFunctionSet of U1,U1 holds

( b_{3} = MSAAut U1 iff for h being ManySortedFunction of U1,U1 holds

( h in b_{3} iff h is_isomorphism U1,U1 ) );

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for b

( b

( h in b

theorem :: AUTALG_1:22

theorem :: AUTALG_1:23

Lm3: for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for f being Element of MSAAut U1 holds

( f is "1-1" & f is "onto" )

proof end;

theorem Th24: :: AUTALG_1:24

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSAAut U1

for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSAAut U1

proof end;

theorem Th25: :: AUTALG_1:25

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for f being Element of MSAAut U1 holds f "" in MSAAut U1

for U1 being non-empty MSAlgebra over S

for f being Element of MSAAut U1 holds f "" in MSAAut U1

proof end;

theorem Th26: :: AUTALG_1:26

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for f1, f2 being Element of MSAAut U1 holds f1 ** f2 in MSAAut U1

for U1 being non-empty MSAlgebra over S

for f1, f2 being Element of MSAAut U1 holds f1 ** f2 in MSAAut U1

proof end;

theorem Th27: :: AUTALG_1:27

for UA being Universal_Algebra

for F being ManySortedFunction of (MSAlg UA),(MSAlg UA)

for f being Element of UAAut UA st F = 0 .--> f holds

F in MSAAut (MSAlg UA)

for F being ManySortedFunction of (MSAlg UA),(MSAlg UA)

for f being Element of UAAut UA st F = 0 .--> f holds

F in MSAAut (MSAlg UA)

proof end;

definition

let S be non empty non void ManySortedSign ;

let U1 be non-empty MSAlgebra over S;

ex b_{1} being BinOp of (MSAAut U1) st

for x, y being Element of MSAAut U1 holds b_{1} . (x,y) = y ** x

for b_{1}, b_{2} being BinOp of (MSAAut U1) st ( for x, y being Element of MSAAut U1 holds b_{1} . (x,y) = y ** x ) & ( for x, y being Element of MSAAut U1 holds b_{2} . (x,y) = y ** x ) holds

b_{1} = b_{2}

end;
let U1 be non-empty MSAlgebra over S;

func MSAAutComp U1 -> BinOp of (MSAAut U1) means :Def6: :: AUTALG_1:def 6

for x, y being Element of MSAAut U1 holds it . (x,y) = y ** x;

existence for x, y being Element of MSAAut U1 holds it . (x,y) = y ** x;

ex b

for x, y being Element of MSAAut U1 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines MSAAutComp AUTALG_1:def 6 :

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for b_{3} being BinOp of (MSAAut U1) holds

( b_{3} = MSAAutComp U1 iff for x, y being Element of MSAAut U1 holds b_{3} . (x,y) = y ** x );

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for b

( b

definition

let S be non empty non void ManySortedSign ;

let U1 be non-empty MSAlgebra over S;

coherence

multMagma(# (MSAAut U1),(MSAAutComp U1) #) is Group

end;
let U1 be non-empty MSAlgebra over S;

coherence

multMagma(# (MSAAut U1),(MSAAutComp U1) #) is Group

proof end;

:: deftheorem defines MSAAutGroup AUTALG_1:def 7 :

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S holds MSAAutGroup U1 = multMagma(# (MSAAut U1),(MSAAutComp U1) #);

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S holds MSAAutGroup U1 = multMagma(# (MSAAut U1),(MSAAutComp U1) #);

registration

let S be non empty non void ManySortedSign ;

let U1 be non-empty MSAlgebra over S;

coherence

MSAAutGroup U1 is strict ;

end;
let U1 be non-empty MSAlgebra over S;

coherence

MSAAutGroup U1 is strict ;

theorem :: AUTALG_1:28

theorem Th29: :: AUTALG_1:29

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 = 1_ (MSAAutGroup U1)

for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 = 1_ (MSAAutGroup U1)

proof end;

theorem :: AUTALG_1:30

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for f being Element of MSAAut U1

for g being Element of (MSAAutGroup U1) st f = g holds

f "" = g "

for U1 being non-empty MSAlgebra over S

for f being Element of MSAAut U1

for g being Element of (MSAAutGroup U1) st f = g holds

f "" = g "

proof end;

begin

:: On the Relationship of Automorphisms of 1-Sorted and Many Sorted Algebras

theorem Th31: :: AUTALG_1:31

for UA1, UA2 being Universal_Algebra st UA1,UA2 are_similar holds

for F being ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)) holds F . 0 is Function of UA1,UA2

for F being ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)) holds F . 0 is Function of UA1,UA2

proof end;

theorem Th32: :: AUTALG_1:32

for UA being Universal_Algebra

for f being Element of UAAut UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA)

for f being Element of UAAut UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA)

proof end;

Lm4: for UA being Universal_Algebra

for h being Function st dom h = UAAut UA & ( for x being set st x in UAAut UA holds

h . x = 0 .--> x ) holds

rng h = MSAAut (MSAlg UA)

proof end;

theorem Th33: :: AUTALG_1:33

for UA being Universal_Algebra

for h being Function st dom h = UAAut UA & ( for x being set st x in UAAut UA holds

h . x = 0 .--> x ) holds

h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA))

for h being Function st dom h = UAAut UA & ( for x being set st x in UAAut UA holds

h . x = 0 .--> x ) holds

h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA))

proof end;

theorem Th34: :: AUTALG_1:34

for UA being Universal_Algebra

for h being Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) st ( for x being set st x in UAAut UA holds

h . x = 0 .--> x ) holds

h is bijective

for h being Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) st ( for x being set st x in UAAut UA holds

h . x = 0 .--> x ) holds

h is bijective

proof end;