Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### On the Group of Inner Automorphisms

by
Artur Kornilowicz

MML identifier: AUTGROUP
[ Mizar article, MML identifier index ]

```environ

vocabulary REALSET1, GROUP_2, GROUP_6, GROUP_1, GROUP_3, RELAT_1, FRAENKEL,
FUNCT_1, FUNCT_2, BINOP_1, VECTSP_1, GROUP_5, WELLORD1, AUTGROUP;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, RELAT_1, FUNCT_1,
PARTFUN1, FUNCT_2, STRUCT_0, BINOP_1, FRAENKEL, RLVECT_1, VECTSP_1,
GROUP_1, GROUP_2, GROUP_3, GROUP_5, GROUP_6;
constructors REALSET1, FUNCSDOM, GROUP_5, GROUP_6, PARTFUN1, MEMBERED,
RELAT_2, XBOOLE_0;
clusters FUNCT_1, FRAENKEL, GROUP_1, GROUP_2, GROUP_3, GROUP_6, STRUCT_0,
GR_CY_2, RELSET_1, MEMBERED, ZFMISC_1, PARTFUN1, FUNCT_2, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

reserve G for strict Group;
reserve H for Subgroup of G;
reserve a, b, c, x, y for Element of G;
reserve h for Homomorphism of G, G;
reserve q, q1 for set;

theorem :: AUTGROUP:1
(for a, b st b is Element of H holds b |^ a in
H) iff H is normal;

definition
let G;
func Aut G -> FUNCTION_DOMAIN of the carrier of G, the carrier of G means
:: AUTGROUP:def 1
( for f being Element of it
holds f is Homomorphism of G, G ) &
for h holds h in it iff h is one-to-one & h is_epimorphism;
end;

canceled;

theorem :: AUTGROUP:3
Aut G c= Funcs (the carrier of G, the carrier of G);

theorem :: AUTGROUP:4
id the carrier of G is Element of Aut G;

theorem :: AUTGROUP:5
for h holds h in Aut G iff h is_isomorphism;

theorem :: AUTGROUP:6
for f being Element of Aut G holds f" is Homomorphism of G, G;

theorem :: AUTGROUP:7
for f being Element of Aut G
holds f" is Element of Aut G;

theorem :: AUTGROUP:8
for f1, f2 being Element of Aut G
holds f1 * f2 is Element of Aut G;

definition
let G;
func AutComp G -> BinOp of Aut G means
:: AUTGROUP:def 2
for x, y being Element of Aut G holds it.(x,y) = x * y;
end;

definition
let G;
func AutGroup G -> strict Group equals
:: AUTGROUP:def 3
HGrStr (# Aut G, AutComp G #);
end;

theorem :: AUTGROUP:9
for x, y being Element of AutGroup G
for f, g being Element of Aut G st x = f & y = g
holds x * y = f * g;

theorem :: AUTGROUP:10
id the carrier of G = 1.AutGroup G;

theorem :: AUTGROUP:11
for f being Element of Aut G
for g being Element of AutGroup G st f = g holds f" = g";

definition
let G;
func InnAut G -> FUNCTION_DOMAIN of the carrier of G,the carrier of G means
:: AUTGROUP:def 4
for f being Element of Funcs (the carrier of G, the carrier of G)
holds f in it iff ex a st for x holds f.x = x |^ a;
end;

theorem :: AUTGROUP:12
InnAut G c= Funcs (the carrier of G, the carrier of G);

theorem :: AUTGROUP:13
for f being Element of InnAut G
holds f is Element of Aut G;

theorem :: AUTGROUP:14
InnAut G c= Aut G;

theorem :: AUTGROUP:15
for f, g being Element of InnAut G
holds (AutComp G).(f, g) = f * g;

theorem :: AUTGROUP:16
id the carrier of G is Element of InnAut G;

theorem :: AUTGROUP:17
for f being Element of InnAut G
holds f" is Element of InnAut G;

theorem :: AUTGROUP:18
for f, g being Element of InnAut G
holds f * g is Element of InnAut G;

definition
let G;
func InnAutGroup G -> normal strict Subgroup of AutGroup G means
:: AUTGROUP:def 5
the carrier of it = InnAut G;
end;

canceled;

theorem :: AUTGROUP:20
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;

theorem :: AUTGROUP:21
id the carrier of G = 1.InnAutGroup G;

theorem :: AUTGROUP:22
for f being Element of InnAut G
for g being Element of InnAutGroup G st f = g holds f" = g";

definition
let G, b;
func Conjugate b -> Element of InnAut G means
:: AUTGROUP:def 6
for a holds it.a = a |^ b;
end;

theorem :: AUTGROUP:23
for a, b holds Conjugate (a * b) = (Conjugate b) * (Conjugate a);

theorem :: AUTGROUP:24
Conjugate 1.G = id the carrier of G;

theorem :: AUTGROUP:25
for a holds (Conjugate 1.G).a = a;

theorem :: AUTGROUP:26
for a holds (Conjugate a) * (Conjugate a") = Conjugate 1.G;

theorem :: AUTGROUP:27
for a holds (Conjugate a") * (Conjugate a) = Conjugate 1.G;

theorem :: AUTGROUP:28
for a holds Conjugate a" = (Conjugate a)";

theorem :: AUTGROUP:29
for a holds ( (Conjugate a) * (Conjugate 1.G) = Conjugate a ) &
( (Conjugate 1.G) * (Conjugate a) = Conjugate a );

theorem :: AUTGROUP:30
for f being Element of InnAut G holds
f * Conjugate 1.G = f & (Conjugate 1.G) * f = f;

theorem :: AUTGROUP:31
for G holds InnAutGroup G, G./.center G are_isomorphic;

theorem :: AUTGROUP:32
for G holds ( G is commutative Group implies
for f being Element of InnAutGroup G
holds f = 1.InnAutGroup G );

```