:: On the Group of Automorphisms of Universal Algebra & Many Sorted Algebra
:: by Artur Korni{\l}owicz
::
:: Received December 13, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

theorem Th1: :: AUTALG_1:1
for UA being Universal_Algebra holds id the carrier of UA is_isomorphism UA,UA
proofend;

definition
let UA be Universal_Algebra;
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
 ex b1 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st
for h being Function of UA,UA holds
( h in b1 iff h is_isomorphism UA,UA )
proofend;
uniqueness
 for b1, b2 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st ( for h being Function of UA,UA holds
( h in b1 iff h is_isomorphism UA,UA ) ) & ( for h being Function of UA,UA holds
( h in b2 iff h is_isomorphism UA,UA ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines UAAut AUTALG_1:def_1_:_
 for UA being Universal_Algebra
for b2 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA holds
( b2 = UAAut UA iff for h being Function of UA,UA holds
( h in b2 iff h is_isomorphism UA,UA ) );

theorem :: AUTALG_1:2
for UA being Universal_Algebra holds UAAut UA c= Funcs ( the carrier of UA, the carrier of UA)
proofend;

theorem Th3: :: AUTALG_1:3
for UA being Universal_Algebra holds id the carrier of UA in UAAut UA
proofend;

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
proofend;

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
proofend;

theorem Th5: :: AUTALG_1:5
for UA being Universal_Algebra
for f being Element of UAAut UA holds f " in UAAut UA
proofend;

theorem Th6: :: AUTALG_1:6
for UA being Universal_Algebra
for f1, f2 being Element of UAAut UA holds f1 * f2 in UAAut UA
proofend;

definition
let UA be Universal_Algebra;
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
 ex b1 being BinOp of (UAAut UA) st
for x, y being Element of UAAut UA holds b1 . (x,y) = y * x
proofend;
uniqueness
 for b1, b2 being BinOp of (UAAut UA) st ( for x, y being Element of UAAut UA holds b1 . (x,y) = y * x ) & ( for x, y being Element of UAAut UA holds b2 . (x,y) = y * x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines UAAutComp AUTALG_1:def_2_:_
 for UA being Universal_Algebra
for b2 being BinOp of (UAAut UA) holds
( b2 = UAAutComp UA iff for x, y being Element of UAAut UA holds b2 . (x,y) = y * x );

definition
let UA be Universal_Algebra;
func UAAutGroup UA ->  Group equals :: AUTALG_1:def 3
 multMagma(# (UAAut UA),(UAAutComp UA) #);
coherence
 multMagma(# (UAAut UA),(UAAutComp UA) #) is Group
proofend;
end;

:: deftheorem  defines UAAutGroup AUTALG_1:def_3_:_
 for UA being Universal_Algebra holds UAAutGroup UA = multMagma(# (UAAut UA),(UAAutComp UA) #);

registration
let UA be Universal_Algebra;
cluster UAAutGroup UA ->  strict ;
coherence
 UAAutGroup UA is strict ;
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 )
proofend;

theorem :: AUTALG_1:7
for UA being Universal_Algebra
for x, y being Element of (UAAutGroup UA)
for f, g being Element of UAAut UA st x = f & y = g holds
x * y = g * f by Def2;

theorem Th8: :: AUTALG_1:8
for UA being Universal_Algebra holds id the carrier of UA = 1_ (UAAutGroup UA)
proofend;

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 "
proofend;

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
proofend;

theorem Th11: :: AUTALG_1:11
for x being set
for A being ManySortedSet of {x} holds A = x .--> (A . x)
proofend;

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" )
proofend;

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
proofend;

theorem Th14: :: AUTALG_1:14
for F, G being Function-yielding Function st F is "1-1" & G is "1-1" holds
G ** F is "1-1"
proofend;

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"
proofend;

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 "")
proofend;

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 ""
proofend;

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()
proofend;

definition
let I be set ;
let A, B be ManySortedSet of I;
assume A1: A is_transformable_to B ;
func MSFuncs (A,B) ->  non empty set  equals :Def4: :: AUTALG_1:def 4
 product ((Funcs) (A,B));
coherence
 product ((Funcs) (A,B)) is non empty set
proofend;
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));

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
proofend;

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)
proofend;

registration
let I be set ;
let A be ManySortedSet of I;
cluster (Funcs) (A,A) -> V2() ;
coherence
 (Funcs) (A,A) is non-empty
proofend;
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 b1 being Element of A holds b1 is ManySortedFunction of D,D
proofend;
end;

registration
let I be set ;
let A be ManySortedSet of I;
cluster id A ->  "onto" ;
coherence
 id A is "onto"
proofend;
cluster id A ->  "1-1" ;
coherence
 id A is "1-1"
proofend;
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;

theorem :: AUTALG_1:21
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSFuncs ( the Sorts of U1, the Sorts of U1) by Th20;

definition
let S be non empty non void ManySortedSign ;
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
 ex b1 being MSFunctionSet of U1,U1 st
for h being ManySortedFunction of U1,U1 holds
( h in b1 iff h is_isomorphism U1,U1 )
proofend;
uniqueness
 for b1, b2 being MSFunctionSet of U1,U1 st ( for h being ManySortedFunction of U1,U1 holds
( h in b1 iff h is_isomorphism U1,U1 ) ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b2 iff h is_isomorphism U1,U1 ) ) holds
b1 = b2
proofend;
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 b3 being MSFunctionSet of U1,U1 holds
( b3 = MSAAut U1 iff for h being ManySortedFunction of U1,U1 holds
( h in b3 iff h is_isomorphism U1,U1 ) );

theorem :: AUTALG_1:22
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 MSFuncs ( the Sorts of U1, the Sorts of U1) by Th20;

theorem :: AUTALG_1:23
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds MSAAut U1 c= MSFuncs ( the Sorts of U1, the Sorts of U1) ;

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" )
proofend;

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
proofend;

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
proofend;

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
proofend;

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)
proofend;

definition
let S be non empty non void ManySortedSign ;
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
 ex b1 being BinOp of (MSAAut U1) st
for x, y being Element of MSAAut U1 holds b1 . (x,y) = y ** x
proofend;
uniqueness
 for b1, b2 being BinOp of (MSAAut U1) st ( for x, y being Element of MSAAut U1 holds b1 . (x,y) = y ** x ) & ( for x, y being Element of MSAAut U1 holds b2 . (x,y) = y ** x ) holds
b1 = b2
proofend;
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 b3 being BinOp of (MSAAut U1) holds
( b3 = MSAAutComp U1 iff for x, y being Element of MSAAut U1 holds b3 . (x,y) = y ** x );

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
func MSAAutGroup U1 ->  Group equals :: AUTALG_1:def 7
 multMagma(# (MSAAut U1),(MSAAutComp U1) #);
coherence
 multMagma(# (MSAAut U1),(MSAAutComp U1) #) is Group
proofend;
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) #);

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
cluster MSAAutGroup U1 ->  strict ;
coherence
 MSAAutGroup U1 is strict ;
end;

theorem :: AUTALG_1:28
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for x, y being Element of (MSAAutGroup U1)
for f, g being Element of MSAAut U1 st x = f & y = g holds
x * y = g ** f by Def6;

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)
proofend;

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 "
proofend;

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
proofend;

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)
proofend;

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)
proofend;

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))
proofend;

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
proofend;

theorem :: AUTALG_1:35
for UA being Universal_Algebra holds UAAutGroup UA, MSAAutGroup (MSAlg UA) are_isomorphic
proofend;