:: by Artur Korni{\l}owicz

::

:: Received April 22, 1994

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

Lm1: for G being strict Group

for H being Subgroup of G st ( for a, b being Element of G st b is Element of H holds

b |^ a in H ) holds

H is normal

proof end;

Lm2: for G being strict Group

for H being Subgroup of G st H is normal holds

for a, b being Element of G st b is Element of H holds

b |^ a in H

proof end;

theorem :: AUTGROUP:1

definition

let G be strict Group;

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

( ( for f being Element of b_{1} holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds

( h in b_{1} iff ( h is one-to-one & h is onto ) ) ) )

for b_{1}, b_{2} being FUNCTION_DOMAIN of the carrier of G, the carrier of G st ( for f being Element of b_{1} holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds

( h in b_{1} iff ( h is one-to-one & h is onto ) ) ) & ( for f being Element of b_{2} holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds

( h in b_{2} iff ( h is one-to-one & h is onto ) ) ) holds

b_{1} = b_{2}

end;
func Aut G -> FUNCTION_DOMAIN of the carrier of G, the carrier of G means :Def1: :: AUTGROUP:def 1

( ( for f being Element of it holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds

( h in it iff ( h is one-to-one & h is onto ) ) ) );

existence ( ( for f being Element of it holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds

( h in it iff ( h is one-to-one & h is onto ) ) ) );

ex b

( ( for f being Element of b

( h in b

proof end;

uniqueness for b

( h in b

( h in b

b

proof end;

:: deftheorem Def1 defines Aut AUTGROUP:def 1 :

for G being strict Group

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

( b_{2} = Aut G iff ( ( for f being Element of b_{2} holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds

( h in b_{2} iff ( h is one-to-one & h is onto ) ) ) ) );

for G being strict Group

for b

( b

( h in b

Lm3: for G being strict Group

for f being Element of Aut G holds

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

proof end;

definition

let G be strict Group;

ex b_{1} being BinOp of (Aut G) st

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

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

b_{1} = b_{2}

end;
func AutComp G -> BinOp of (Aut G) means :Def2: :: AUTGROUP:def 2

for x, y being Element of Aut G holds it . (x,y) = x * y;

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

ex b

for x, y being Element of Aut G holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines AutComp AUTGROUP:def 2 :

for G being strict Group

for b_{2} being BinOp of (Aut G) holds

( b_{2} = AutComp G iff for x, y being Element of Aut G holds b_{2} . (x,y) = x * y );

for G being strict Group

for b

( b

definition
end;

:: deftheorem defines AutGroup AUTGROUP:def 3 :

for G being strict Group holds AutGroup G = multMagma(# (Aut G),(AutComp G) #);

for G being strict Group holds AutGroup G = multMagma(# (Aut G),(AutComp G) #);

theorem :: AUTGROUP:8

theorem Th10: :: AUTGROUP:10

for G being strict Group

for f being Element of Aut G

for g being Element of (AutGroup G) st f = g holds

f " = g "

for f being Element of Aut G

for g being Element of (AutGroup G) st f = g holds

f " = g "

proof end;

definition

let G be strict Group;

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

for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in b_{1} iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a )

for b_{1}, b_{2} being FUNCTION_DOMAIN of the carrier of G, the carrier of G st ( for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in b_{1} iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) ) & ( for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in b_{2} iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) ) holds

b_{1} = b_{2}

end;
func InnAut G -> FUNCTION_DOMAIN of the carrier of G, the carrier of G means :Def4: :: AUTGROUP:def 4

for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in it iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a );

existence for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in it iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a );

ex b

for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in b

for x being Element of G holds f . x = x |^ a )

proof end;

uniqueness for b

( f in b

for x being Element of G holds f . x = x |^ a ) ) & ( for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in b

for x being Element of G holds f . x = x |^ a ) ) holds

b

proof end;

:: deftheorem Def4 defines InnAut AUTGROUP:def 4 :

for G being strict Group

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

( b_{2} = InnAut G iff for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in b_{2} iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) );

for G being strict Group

for b

( b

( f in b

for x being Element of G holds f . x = x |^ a ) );

definition

let G be strict Group;

ex b_{1} being strict normal Subgroup of AutGroup G st the carrier of b_{1} = InnAut G

for b_{1}, b_{2} being strict normal Subgroup of AutGroup G st the carrier of b_{1} = InnAut G & the carrier of b_{2} = InnAut G holds

b_{1} = b_{2}
by GROUP_2:59;

end;
func InnAutGroup G -> strict normal Subgroup of AutGroup G means :Def5: :: AUTGROUP:def 5

the carrier of it = InnAut G;

existence the carrier of it = InnAut G;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def5 defines InnAutGroup AUTGROUP:def 5 :

for G being strict Group

for b_{2} being strict normal Subgroup of AutGroup G holds

( b_{2} = InnAutGroup G iff the carrier of b_{2} = InnAut G );

for G being strict Group

for b

( b

theorem Th18: :: AUTGROUP:18

for G being strict Group

for x, y being Element of (InnAutGroup G)

for f, g being Element of InnAut G st x = f & y = g holds

x * y = f * g

for x, y being Element of (InnAutGroup G)

for f, g being Element of InnAut G st x = f & y = g holds

x * y = f * g

proof end;

theorem :: AUTGROUP:20

for G being strict Group

for f being Element of InnAut G

for g being Element of (InnAutGroup G) st f = g holds

f " = g "

for f being Element of InnAut G

for g being Element of (InnAutGroup G) st f = g holds

f " = g "

proof end;

definition

let G be strict Group;

let b be Element of G;

ex b_{1} being Element of InnAut G st

for a being Element of G holds b_{1} . a = a |^ b

for b_{1}, b_{2} being Element of InnAut G st ( for a being Element of G holds b_{1} . a = a |^ b ) & ( for a being Element of G holds b_{2} . a = a |^ b ) holds

b_{1} = b_{2}

end;
let b be Element of G;

func Conjugate b -> Element of InnAut G means :Def6: :: AUTGROUP:def 6

for a being Element of G holds it . a = a |^ b;

existence for a being Element of G holds it . a = a |^ b;

ex b

for a being Element of G holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines Conjugate AUTGROUP:def 6 :

for G being strict Group

for b being Element of G

for b_{3} being Element of InnAut G holds

( b_{3} = Conjugate b iff for a being Element of G holds b_{3} . a = a |^ b );

for G being strict Group

for b being Element of G

for b

( b

theorem Th21: :: AUTGROUP:21

for G being strict Group

for a, b being Element of G holds Conjugate (a * b) = (Conjugate b) * (Conjugate a)

for a, b being Element of G holds Conjugate (a * b) = (Conjugate b) * (Conjugate a)

proof end;

theorem :: AUTGROUP:24

for G being strict Group

for a being Element of G holds (Conjugate a) * (Conjugate (a ")) = Conjugate (1_ G)

for a being Element of G holds (Conjugate a) * (Conjugate (a ")) = Conjugate (1_ G)

proof end;

theorem Th25: :: AUTGROUP:25

for G being strict Group

for a being Element of G holds (Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G)

for a being Element of G holds (Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G)

proof end;

theorem :: AUTGROUP:27

for G being strict Group

for a being Element of G holds

( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a )

for a being Element of G holds

( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a )

proof end;

theorem :: AUTGROUP:28

for G being strict Group

for f being Element of InnAut G holds

( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f )

for f being Element of InnAut G holds

( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f )

proof end;

theorem :: AUTGROUP:30

for G being strict Group st G is commutative Group holds

for f being Element of (InnAutGroup G) holds f = 1_ (InnAutGroup G)

for f being Element of (InnAutGroup G) holds f = 1_ (InnAutGroup G)

proof end;