:: On the Group of Inner Automorphisms
:: by Artur Korni{\l}owicz
::
:: Received April 22, 1994
:: Copyright (c) 1994-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, GROUP_1, GROUP_2, SUBSET_1, GROUP_6, NEWTON, PRE_TOPC,
RELAT_1, TARSKI, FUNCT_2, FUNCT_1, XBOOLE_0, BINOP_1, ALGSTR_0, ZFMISC_1,
REALSET1, GROUP_5, WELLORD1, AUTGROUP;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, ALGSTR_0, BINOP_1, GROUP_1,
GROUP_2, GROUP_3, GROUP_5, GROUP_6;
constructors BINOP_1, REALSET1, GROUP_5, GROUP_6, RELSET_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, STRUCT_0, GROUP_1,
GROUP_2, GROUP_3, GROUP_6, GR_CY_2;
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 onto;
end;
theorem :: AUTGROUP:2
Aut G c= Funcs (the carrier of G, the carrier of G);
theorem :: AUTGROUP:3
id the carrier of G is Element of Aut G;
theorem :: AUTGROUP:4
for h holds h in Aut G iff h is bijective;
theorem :: AUTGROUP:5
for f being Element of Aut G holds f" is Homomorphism of G, G;
theorem :: AUTGROUP:6
for f being Element of Aut G holds f" is Element of Aut G;
theorem :: AUTGROUP:7
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
multMagma (# Aut G, AutComp G #);
end;
theorem :: AUTGROUP:8
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:9
id the carrier of G = 1_AutGroup G;
theorem :: AUTGROUP:10
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:11
InnAut G c= Funcs (the carrier of G, the carrier of G);
theorem :: AUTGROUP:12
for f being Element of InnAut G holds f is Element of Aut G;
theorem :: AUTGROUP:13
InnAut G c= Aut G;
theorem :: AUTGROUP:14
for f, g being Element of InnAut G holds (AutComp G).(f, g) = f * g;
theorem :: AUTGROUP:15
id the carrier of G is Element of InnAut G;
theorem :: AUTGROUP:16
for f being Element of InnAut G holds f" is Element of InnAut G;
theorem :: AUTGROUP:17
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;
theorem :: AUTGROUP:18
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:19
id the carrier of G = 1_InnAutGroup G;
theorem :: AUTGROUP:20
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:21
for a, b holds Conjugate (a * b) = (Conjugate b) * (Conjugate a);
theorem :: AUTGROUP:22
Conjugate 1_G = id the carrier of G;
theorem :: AUTGROUP:23
for a holds (Conjugate 1_G).a = a;
theorem :: AUTGROUP:24
for a holds (Conjugate a) * (Conjugate a") = Conjugate 1_G;
theorem :: AUTGROUP:25
for a holds (Conjugate a") * (Conjugate a) = Conjugate 1_G;
theorem :: AUTGROUP:26
for a holds Conjugate a" = (Conjugate a)";
theorem :: AUTGROUP:27
for a holds (Conjugate a) * (Conjugate 1_G) = Conjugate a & (Conjugate
1_G) * (Conjugate a) = Conjugate a;
theorem :: AUTGROUP:28
for f being Element of InnAut G holds f * Conjugate 1_G = f & (
Conjugate 1_G) * f = f;
theorem :: AUTGROUP:29
for G holds InnAutGroup G, G./.center G are_isomorphic;
theorem :: AUTGROUP:30
for G holds ( G is commutative Group implies for f being Element of
InnAutGroup G holds f = 1_InnAutGroup G );