Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

### The abstract of the Mizar article:

### On the Group of Inner Automorphisms

**by****Artur Kornilowicz**- Received April 22, 1994
- 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 );

Back to top