:: On the Group of Inner Automorphisms
:: by Artur Korni{\l}owicz
::
:: Received April 22, 1994
:: Copyright (c) 1994-2026 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, MSSUBFAM, MONOID_0;
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, MONOID_0;
constructors BINOP_1, REALSET1, GROUP_5, GROUP_6, RELSET_1, MONOID_0;
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;
definitions FUNCT_1, TARSKI, FUNCT_2;
equalities BINOP_1, REALSET1, GROUP_2, GROUP_3, ALGSTR_0;
expansions BINOP_1, FUNCT_2;
theorems FUNCT_1, FUNCT_2, GROUP_1, GROUP_2, GROUP_3, GROUP_5, GROUP_6,
REALSET1, RELAT_1, ZFMISC_1, XBOOLE_0, STRUCT_0, MONOID_0;
schemes BINOP_1, FUNCT_2;
begin
reserve G for 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;
Lm1: (for a,b st b is Element of H holds b |^ a in H) implies H is normal
proof
assume
A1: for a, b st b is Element of H holds b |^ a in H;
now
let a;
thus H * a c= a * H
proof
set A = carr H;
let q be object;
assume q in H * a;
then consider b such that
A2: q = b * a and
A3: b in H by GROUP_2:104;
b is Element of H by A3,STRUCT_0:def 5;
then b |^ a in H by A1;
then b |^ a in A by STRUCT_0:def 5;
then a * (a" * b * a) in a * A by GROUP_2:27;
then a * (a" * (b * a)) in a * A by GROUP_1:def 3;
then (a * a") * (b * a) in a * A by GROUP_1:def 3;
then a * a" * b * a in a * A by GROUP_1:def 3;
then 1_G * b * a in a * A by GROUP_1:def 5;
hence thesis by A2,GROUP_1:def 4;
end;
end;
hence thesis by GROUP_3:119;
end;
Lm2: H is normal implies for a,b st b is Element of H holds b |^ a in H
proof
assume
A1: H is normal;
set A = carr H;
let a, b;
H * a = a * H by A1,GROUP_3:117;
then a" * H * a = a" * (a * H) by GROUP_2:106;
then a" * H * a = a" * a * H by GROUP_2:105;
then a" * H * a = 1_G * H by GROUP_1:def 5;
then a" * H * a = A by GROUP_2:109;
then the carrier of H |^ a = A by GROUP_3:59;
then
A2: A |^ a = A by GROUP_3:def 6;
assume b is Element of H;
then a" * b in a" * A by GROUP_2:27;
then a" * b * a in a" * A * a by GROUP_2:28;
then b |^ a in A by A2,GROUP_3:50;
hence thesis by STRUCT_0:def 5;
end;
theorem
(for a, b st b is Element of H holds b |^ a in H) iff H is normal by Lm1,Lm2;
definition
let G be Group;
func Aut G -> FUNCTION_DOMAIN of the carrier of G, the carrier of G means
:
Def1: ( 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
proof
set X = { x where x is Element of Funcs (the carrier of G,the carrier of G
) : ex h being Homomorphism of G,G
st x = h & h is one-to-one & h is onto };
A1: id the carrier of G in X
proof
set I = id the carrier of G;
A2: I in Funcs (the carrier of G, the carrier of G) by FUNCT_2:8;
reconsider I as Homomorphism of G, G by GROUP_6:38;
rng I = the carrier of G by RELAT_1:45;
then I is onto;
hence thesis by A2;
end;
reconsider X as set;
X is functional
proof
let q be object;
assume q in X;
then
ex x be Element of Funcs (the carrier of G, the carrier of G) st
q = x & ex h being Homomorphism of G, G st
h = x & h is one-to-one & h is onto;
hence thesis;
end;
then reconsider X as functional non empty set by A1;
X is FUNCTION_DOMAIN of the carrier of G, the carrier of G
proof
let a be Element of X;
a in X;
then ex x be Element of Funcs (the carrier of G, the carrier of G ) st a
= x & ex h being Homomorphism of G, G st
h = x & h is one-to-one & h is onto;
hence thesis;
end;
then reconsider
X as FUNCTION_DOMAIN of the carrier of G, the carrier of G;
take X;
hereby
let f be Element of X;
f in X;
then
ex x being Element of Funcs (the carrier of G, the carrier of G) st
f = x & ex h being Homomorphism of G, G st
h = x & h is one-to-one & h is onto;
hence f is Homomorphism of G, G;
end;
let x be Homomorphism of G, G;
hereby
assume x in X;
then
ex f being Element of Funcs (the carrier of G, the carrier of G) st
f = x & ex h being Homomorphism of G, G st
h = f & h is one-to-one & h is onto;
hence x is one-to-one & x is onto;
end;
A3: x is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:8;
assume x is one-to-one & x is onto;
hence thesis by A3;
end;
uniqueness
proof
let F1, F2 be FUNCTION_DOMAIN of the carrier of G, the carrier of G such
that
A4: for f being Element of F1 holds f is Homomorphism of G, G and
A5: for h being Homomorphism of G, G holds
h in F1 iff h is one-to-one & h is onto and
A6: for f being Element of F2 holds f is Homomorphism of G, G and
A7: for h being Homomorphism of G, G holds
h in F2 iff h is one-to-one & h is onto;
A8: F2 c= F1
proof
let q be object;
assume
A9: q in F2;
then reconsider h1 = q as Homomorphism of G, G by A6;
h1 is one-to-one & h1 is onto by A7,A9;
hence thesis by A5;
end;
F1 c= F2
proof
let q be object;
assume
A10: q in F1;
then reconsider h1 = q as Homomorphism of G, G by A4;
h1 is one-to-one & h1 is onto by A5,A10;
hence thesis by A7;
end;
hence thesis by A8,XBOOLE_0:def 10;
end;
end;
theorem
Aut G c= Funcs (the carrier of G, the carrier of G)
proof
let q be object;
assume q in Aut G;
then ex f be Element of Aut G st f = q;
hence thesis by FUNCT_2:9;
end;
theorem Th3:
id the carrier of G is Element of Aut G
proof
id the carrier of G is Homomorphism of G, G by GROUP_6:38;
then consider h such that
A1: h = id the carrier of G;
rng h = the carrier of G by A1,RELAT_1:45;
then h is onto;
hence thesis by A1,Def1;
end;
theorem Th4:
for h holds h in Aut G iff h is bijective by Def1;
Lm3: for f being Element of Aut G holds
dom f = rng f & dom f = the carrier of G
proof
let f be Element of Aut G;
reconsider f as Homomorphism of G, G by Def1;
A1: f is bijective by Th4;
then dom f = the carrier of G by GROUP_6:61;
hence thesis by A1,GROUP_6:61;
end;
theorem Th5:
for f being Element of Aut G holds f" is Homomorphism of G, G
proof
let f be Element of Aut G;
reconsider f as Homomorphism of G, G by Def1;
f is bijective by Th4;
hence thesis by GROUP_6:62;
end;
theorem Th6:
for f being Element of Aut G holds f" is Element of Aut G
proof
let f be Element of Aut G;
reconsider f as Homomorphism of G, G by Def1;
reconsider A = f" as Homomorphism of G, G by Th5;
f is bijective by Th4;
then A is bijective by GROUP_6:63;
hence thesis by Def1;
end;
theorem Th7:
for f1, f2 being Element of Aut G holds f1 * f2 is Element of Aut G
proof
let f1, f2 be Element of Aut G;
reconsider f1, f2 as Homomorphism of G, G by Def1;
f1 is bijective & f2 is bijective by Th4;
then f1 * f2 is bijective;
hence thesis by Th4;
end;
definition
let G;
func AutComp G -> BinOp of Aut G means
:Def2:
for x, y being Element of Aut G holds it.(x,y) = x * y;
existence
proof
defpred P[Element of Aut G,Element of Aut G,set] means $3 = $1 * $2;
A1: for x, y being Element of Aut G ex m being Element of Aut G st P[x,y,m ]
proof
let x, y be Element of Aut G;
reconsider xx = x, yy = y as Homomorphism of G, G by Def1;
reconsider m = xx * yy as Element of Aut G by Th7;
take m;
thus thesis;
end;
thus ex M being BinOp of Aut G st for x, y being Element of Aut G holds P[
x,y,M.(x,y)] from BINOP_1:sch 3 (A1);
end;
uniqueness
proof
let b1, b2 be BinOp of Aut G such that
A2: for x, y be Element of Aut G holds b1.(x,y) = x * y and
A3: for x, y be Element of Aut G holds b2.(x,y) = x * y;
for x, y be Element of Aut G holds b1.(x,y) = b2.(x,y)
proof
let x, y be Element of Aut G;
thus b1.(x,y) = x * y by A2
.= b2.(x,y) by A3;
end;
hence thesis;
end;
end;
definition
let G;
func AutGroup G -> strict Group equals
multMagma (# Aut G, AutComp G #);
coherence
proof
set H = multMagma (# Aut G, AutComp G #);
A1: ex e being Element of H st for h being Element of H holds h * e = h &
e * h = h & ex g being Element of H st h * g = e & g * h = e
proof
reconsider e = id the carrier of G as Element of H by Th3;
take e;
let h be Element of H;
consider A be Element of Aut G such that
A2: A = h;
h * e = A * id the carrier of G by A2,Def2
.= A by FUNCT_2:17;
hence h * e = h by A2;
e * h = (id the carrier of G) * A by A2,Def2
.= A by FUNCT_2:17;
hence e * h = h by A2;
reconsider g = A" as Element of H by Th6;
take g;
reconsider A as Homomorphism of G, G by Def1;
A3: A is one-to-one by Def1;
A is onto by Def1;
then
A4: rng A = the carrier of G;
thus h * g = A * A" by A2,Def2
.= e by A3,A4,FUNCT_2:29;
thus g * h = A" * A by A2,Def2
.= e by A3,A4,FUNCT_2:29;
end;
for f, g, h being Element of H holds (f * g) * h = f * (g * h)
proof
let f,g,h be Element of H;
reconsider A = f, B = g, C = h as Element of Aut G;
A5: g * h = B * C by Def2;
f * g = A * B by Def2;
hence (f * g) * h = A * B * C by Def2
.= A * (B * C) by RELAT_1:36
.= f * (g * h) by A5,Def2;
end;
hence thesis by A1,GROUP_1:def 2,def 3;
end;
end;
theorem
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 by Def2;
theorem Th9:
id the carrier of G = 1_AutGroup G
proof
set f = the Element of AutGroup G;
reconsider g = id the carrier of G as Element of AutGroup G by Th3;
consider g1 be Function of the carrier of G, the carrier of G such that
A1: g1 = g;
f is Homomorphism of G, G by Def1;
then consider f1 be Function of the carrier of G, the carrier of G such that
A2: f1 = f;
f1 = f & g1 = g implies f1 * g1 = f * g by Def2;
hence thesis by A1,A2,FUNCT_2:17,GROUP_1:7;
end;
theorem Th10:
for f being Element of Aut G for g being Element of AutGroup G
st f = g holds f" = g"
proof
let f be Element of Aut G;
let g be Element of AutGroup G;
consider g1 be Element of Aut G such that
A1: g1 = g";
assume f = g;
then g1 * f = g" * g by A1,Def2;
then g1 * f = 1_AutGroup G by GROUP_1:def 5;
then
A2: g1 * f = id the carrier of G by Th9;
f is Homomorphism of G, G by Def1;
then
A3: f is one-to-one by Def1;
rng f = dom f by Lm3
.= the carrier of G by Lm3;
hence thesis by A1,A3,A2,FUNCT_2:30;
end;
definition
let G;
func InnAut G -> FUNCTION_DOMAIN of the carrier of G,the carrier of G means
:Def4:
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;
existence
proof
set I = id the carrier of G;
set X = { f where f is Element of Funcs (the carrier of G,the carrier of G
) : ex a st for x holds f.x = x |^ a };
A1: ex a st for x holds I.x = x |^ a
proof
take a = 1_G;
let x;
A2: a" = 1_G by GROUP_1:8;
thus I.x = x
.= x * a by GROUP_1:def 4
.= x |^ a by A2,GROUP_1:def 4;
end;
I is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:8;
then
A3: I in X by A1;
X is functional
proof
let h be object;
assume h in X;
then
ex f being Element of Funcs (the carrier of G,the carrier of G) st f
= h & ex a st for x holds f.x = x |^ a;
hence thesis;
end;
then reconsider X as functional non empty set by A3;
X is FUNCTION_DOMAIN of the carrier of G, the carrier of G
proof
let h be Element of X;
h in X;
then ex f being Element of Funcs (the carrier of G,the carrier of G) st
f = h & ex a st for x holds f.x = x |^ a;
hence thesis;
end;
then reconsider
X as FUNCTION_DOMAIN of the carrier of G, the carrier of G;
take X;
let f be Element of Funcs (the carrier of G, the carrier of G);
hereby
assume f in X;
then
ex f1 being Element of Funcs (the carrier of G,the carrier of G) st
f1 = f & ex a st for x holds f1.x = x |^ a;
hence ex a st for x holds f.x = x |^ a;
end;
thus thesis;
end;
uniqueness
proof
let F1, F2 be FUNCTION_DOMAIN of the carrier of G, the carrier of G such
that
A4: for f being Element of Funcs (the carrier of G, the carrier of G)
holds f in F1 iff ex a st for x holds f.x = x |^ a and
A5: for f being Element of Funcs (the carrier of G, the carrier of G)
holds f in F2 iff ex a st for x holds f.x = x |^ a;
A6: F2 c= F1
proof
let q be object;
assume
A7: q in F2;
then q is Function of the carrier of G, the carrier of G by
FUNCT_2:def 12;
then reconsider
b1 = q as Element of Funcs (the carrier of G,the carrier of G
) by FUNCT_2:9;
ex a st for x holds b1.x = x |^ a by A5,A7;
hence thesis by A4;
end;
F1 c= F2
proof
let q be object;
assume
A8: q in F1;
then q is Function of the carrier of G, the carrier of G by
FUNCT_2:def 12;
then reconsider
b1 = q as Element of Funcs (the carrier of G,the carrier of G
) by FUNCT_2:9;
ex a st for x holds b1.x = x |^ a by A4,A8;
hence thesis by A5;
end;
hence thesis by A6,XBOOLE_0:def 10;
end;
end;
theorem
InnAut G c= Funcs (the carrier of G, the carrier of G)
proof
let q be object;
assume q in InnAut G;
then ex f be Element of InnAut G st f = q;
hence thesis by FUNCT_2:9;
end;
theorem Th12:
for f being Element of InnAut G holds f is Element of Aut G
proof
let f be Element of InnAut G;
A1: f is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:9;
now
let x,y;
consider a such that
A2: for x holds f.x = x |^ a by A1,Def4;
thus f.(x * y) = (x * y) |^ a by A2
.= a" * x * y * a by GROUP_1:def 3
.= (a" * x) * (y * a) by GROUP_1:def 3
.= (a" * x) * 1_G * (y * a) by GROUP_1:def 4
.= a" * x * (a * a") * (y * a) by GROUP_1:def 5
.= a" * x * a * a" * (y * a) by GROUP_1:def 3
.= (a" * x * a) * a" * y * a by GROUP_1:def 3
.= (a" * x * a) * (a" * y) * a by GROUP_1:def 3
.= (x |^ a) * (y |^ a) by GROUP_1:def 3
.= f.x * (y |^ a) by A2
.= f.x * f.y by A2;
end;
then reconsider f as Homomorphism of G, G by GROUP_6:def 6;
A3: f is one-to-one
proof
let q,q1 be object;
assume that
A4: q in dom f & q1 in dom f and
A5: f.q = f.q1;
consider x, y such that
A6: x = q & y = q1 by A4;
consider a such that
A7: for x holds f.x = x |^ a by A1,Def4;
f.x = y |^ a by A7,A5,A6;
then x |^ a = y |^ a by A7;
then a * (a" * (x * a)) = a * (a" * y * a) by GROUP_1:def 3;
then (a * a") * (x * a) = a * (a" * y * a) by GROUP_1:def 3;
then (a * a") * (x * a) = a * (a" * (y * a)) by GROUP_1:def 3;
then (a * a") * (x * a) = (a * a") * (y * a) by GROUP_1:def 3;
then 1_G * (x * a) = (a * a") * (y * a) by GROUP_1:def 5;
then 1_G * (x * a) = 1_G * (y * a) by GROUP_1:def 5;
then x * a = 1_G * (y * a) by GROUP_1:def 4;
then x * a * a" = y * a * a" by GROUP_1:def 4;
then x * (a * a") = y * a * a" by GROUP_1:def 3;
then x * (a * a") = y * (a * a") by GROUP_1:def 3;
then x * 1_G = y * (a * a") by GROUP_1:def 5;
then x * 1_G = y * 1_G by GROUP_1:def 5;
then x = y * 1_G by GROUP_1:def 4;
hence thesis by A6,GROUP_1:def 4;
end;
for q being object st q in the carrier of G
ex q1 being object st q1 in dom f & q=f.q1
proof
let q be object;
assume q in the carrier of G;
then consider y such that
A8: y = q;
consider a such that
A9: for x holds f.x = x |^ a by A1,Def4;
take q1 = a * y * a";
ex f1 being Function st f = f1 & dom f1 = the carrier of G & rng f1
c= the carrier of G by A1,FUNCT_2:def 2;
hence q1 in dom f;
y = 1_G * y by GROUP_1:def 4
.= 1_G * y * 1_G by GROUP_1:def 4
.= a" * a * y * 1_G by GROUP_1:def 5
.= a" * a * y * (a" * a) by GROUP_1:def 5
.= (a" * a * y) * a" * a by GROUP_1:def 3
.= (a" * a * (y * a")) * a by GROUP_1:def 3
.= a" * (a * (y * a")) * a by GROUP_1:def 3
.= q1 |^ a by GROUP_1:def 3
.= f.q1 by A9;
hence thesis by A8;
end;
then the carrier of G c= rng f by FUNCT_1:9;
then rng f = the carrier of G by XBOOLE_0:def 10;
then f is onto;
hence thesis by A3,Def1;
end;
theorem Th13:
InnAut G c= Aut G
proof
let q be object;
assume q in InnAut G;
then consider f be Element of InnAut G such that
A1: f = q;
f is Element of Aut G by Th12;
hence q in Aut G by A1;
end;
theorem Th14:
for f, g being Element of InnAut G holds (AutComp G).(f, g) = f * g
proof
let f, g be Element of InnAut G;
f is Element of Aut G & g is Element of Aut G by Th12;
hence thesis by Def2;
end;
theorem Th15:
id the carrier of G is Element of InnAut G
proof
set I = id the carrier of G;
A1: ex a st for x holds I.x = x |^ a
proof
take a = 1_G;
let x;
A2: a" = 1_G by GROUP_1:8;
thus I.x = x
.= x * a by GROUP_1:def 4
.= x |^ a by A2,GROUP_1:def 4;
end;
I is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:8;
hence thesis by A1,Def4;
end;
theorem Th16:
for f being Element of InnAut G holds f" is Element of InnAut G
proof
let f be Element of InnAut G;
reconsider f1 = f as Element of Funcs (the carrier of G, the carrier of G)
by FUNCT_2:9;
f1 = f;
then consider
f1 be Element of Funcs (the carrier of G, the carrier of G) such
that
A1: f1 = f;
A2: ex a st for x holds f".x = x |^ a
proof
consider b such that
A3: for y holds f1.y = y |^ b by A1,Def4;
take a = b";
let x;
A4: f1 is Element of Aut G by A1,Th12;
then reconsider f1 as Homomorphism of G, G by Def1;
A5: f1 is bijective by A4,Th4;
then consider y1 be Element of G such that
A6: x = f1.y1 by GROUP_6:58;
f1".x = y1 by A5,A6,FUNCT_2:26
.= 1_G * y1 by GROUP_1:def 4
.= 1_G * y1 * 1_G by GROUP_1:def 4
.= b * b" * y1 * 1_G by GROUP_1:def 5
.= b * b" * y1 * (b * b") by GROUP_1:def 5
.= (b * b" * y1) * b * b" by GROUP_1:def 3
.= (b * b" * (y1 * b)) * b" by GROUP_1:def 3
.= b * (b" * (y1 * b)) * b" by GROUP_1:def 3
.= b * (y1 |^ b) * b" by GROUP_1:def 3
.= b * x * b" by A3,A6
.= a" * x * a;
hence thesis by A1;
end;
A7: f is Element of Aut G by Th12;
then reconsider f2 = f as Homomorphism of G, G by Def1;
f2 = f;
then consider f2 be Homomorphism of G, G such that
A8: f2 = f;
f2 is onto by A7,A8,Def1;
then
A9: rng f2 = the carrier of G;
f2 is one-to-one by A7,A8,Def1;
then f" is Function of the carrier of G, the carrier of G by A8,A9,FUNCT_2:25
;
then f" is Element of Funcs(the carrier of G, the carrier of G) by FUNCT_2:9;
hence thesis by A2,Def4;
end;
theorem Th17:
for f, g being Element of InnAut G holds f * g is Element of InnAut G
proof
let f, g be Element of InnAut G;
A1: g is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:9;
A2: f is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:9;
A3: ex a st for x holds (f * g).x = x |^ a
proof
consider c such that
A4: for x2 being Element of G holds g.x2 = x2 |^ c by A1,Def4;
consider b such that
A5: for x1 being Element of G holds f.x1 = x1 |^ b by A2,Def4;
take a = c * b;
let x;
(f * g).x = f.(g.x) by FUNCT_2:15
.= f.(x |^ c) by A4
.= (c" * x * c) |^ b by A5
.= b" * (c" * x * c * b) by GROUP_1:def 3
.= b" * (c" * (x * c) * b) by GROUP_1:def 3
.= b" * (c" * (x * c * b)) by GROUP_1:def 3
.= (b" * c") * (x * c * b) by GROUP_1:def 3
.= (b" * c") * (x * (c * b)) by GROUP_1:def 3
.= (b" * c") * x * (c * b) by GROUP_1:def 3
.= x |^ a by GROUP_1:17;
hence thesis;
end;
f * g is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:9;
hence thesis by A3,Def4;
end;
definition
let G;
func InnAutGroup G -> normal strict Subgroup of AutGroup G means
:Def5:
the carrier of it = InnAut G;
existence
proof
reconsider K1 = Aut G as set;
reconsider K2 = InnAut G as Subset of K1 by Th13;
for q holds q in [:K2,K2:] implies (AutComp G).q in K2
proof
let q;
assume q in [:K2,K2:];
then consider x, y be object such that
A1: x in K2 & y in K2 and
A2: q = [x, y] by ZFMISC_1:def 2;
reconsider x, y as Element of InnAut G by A1;
A3: x * y is Element of InnAut G by Th17;
(AutComp G).q = (AutComp G).(x, y) by A2
.= x * y by Th14;
hence thesis by A3;
end;
then AutComp G is Presv of K1, K2 by REALSET1:def 4;
then reconsider op = (AutComp G)||InnAut G as BinOp of InnAut G by
REALSET1:6;
set IG = multMagma (# InnAut G, op #);
A4: now
let x,y be Element of IG, f,g be Element of InnAut G;
A5: [f, g] in [:InnAut G, InnAut G:] by ZFMISC_1:def 2;
assume x = f & y = g;
hence x * y = (AutComp G).(f,g) by A5,FUNCT_1:49
.= f * g by Th14;
end;
A6: for f,g,h being Element of IG holds (f * g) * h = f * (g * h)
proof
let f,g,h be Element of IG;
reconsider A = f, B = g, C = h as Element of InnAut G;
A7: g * h = B * C by A4;
f * g = A * B by A4;
hence (f * g) * h = A * B * C by A4
.= A * (B * C) by RELAT_1:36
.= f * (g * h) by A4,A7;
end;
ex e being Element of IG st for h being Element of IG holds h * e = h
& e * h = h & ex g being Element of IG st h * g = e & g * h = e
proof
reconsider e = id the carrier of G as Element of IG by Th15;
take e;
let h be Element of IG;
consider A be Element of InnAut G such that
A8: A = h;
h * e = A * id the carrier of G by A4,A8
.= A by FUNCT_2:17;
hence h * e = h by A8;
e * h = (id the carrier of G) * A by A4,A8
.= A by FUNCT_2:17;
hence e * h = h by A8;
reconsider g = A" as Element of IG by Th16;
take g;
reconsider A as Element of Aut G by Th12;
reconsider A as Homomorphism of G, G by Def1;
A9: A is one-to-one by Def1;
A is onto by Def1;
then
A10: rng A = the carrier of G;
thus h * g = A * A" by A4,A8
.= e by A9,A10,FUNCT_2:29;
thus g * h = A" * A by A4,A8
.= e by A9,A10,FUNCT_2:29;
end;
then reconsider IG as Group by A6,GROUP_1:def 2,def 3;
the carrier of IG c= the carrier of AutGroup G by Th13;
then reconsider IG as strict Subgroup of AutGroup G by GROUP_2:def 5;
for f, k being Element of AutGroup G st k is Element of IG holds k |^
f in IG
proof
let f, k be Element of AutGroup G;
consider f1 be Element of Aut G such that
A11: f1 = f;
assume k is Element of IG;
then consider g be Element of InnAut G such that
A12: g = k;
reconsider D = g as Element of Aut G by Th12;
g is Element of Aut G by Th12;
then consider g1 be Element of Aut G such that
A13: g1 = g;
g1 is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:8;
then consider a such that
A14: for x holds g1.x = x |^ a by A13,Def4;
f1" * g1 * f1 is Element of InnAut G
proof
f1 is Homomorphism of G, G by Def1;
then
A15: f1 is one-to-one by Def1;
A16: rng f1 = dom f1 by Lm3
.= the carrier of G by Lm3;
then f1" is Function of the carrier of G, the carrier of G by A15,
FUNCT_2:25;
then
f1" * g1 is Function of the carrier of G, the carrier of G by FUNCT_2:13;
then f1" * g1 * f1 is Function of the carrier of G, the carrier of G
by FUNCT_2:13;
then
A17: f1" * g1 * f1 is Element of Funcs (the carrier of G, the carrier
of G) by FUNCT_2:8;
f1" is Element of Aut G by Th6;
then f1" is Homomorphism of G, G by Def1;
then consider A be Homomorphism of G, G such that
A18: A = f1";
A19: A * f1 = id the carrier of G by A15,A16,A18,FUNCT_2:29;
now
let y;
thus (f1" * g1 * f1).y = (f1" * (g1 * f1)).y by RELAT_1:36
.= f1".((g1 * f1).y) by FUNCT_2:15
.= f1".(g1.(f1.y)) by FUNCT_2:15
.= f1".(f1.y |^ a) by A14
.= A.(a" * f1.y) * A.a by A18,GROUP_6:def 6
.= A.a" * A.(f1.y) * A.a by GROUP_6:def 6
.= A.a" * (A * f1).y * A.a by FUNCT_2:15
.= A.a" * y * A.a by A19
.= y |^ A.a by GROUP_6:32;
end;
hence thesis by A17,Def4;
end;
then
A20: f1" * g * f1 in InnAut G by A13;
reconsider C = f1" as Element of Aut G by Th6;
consider q such that
A21: q = f" * k * f;
f1" = f" by A11,Th10;
then C * D = f" * k by A12,Def2;
then q in carr IG by A11,A20,A21,Def2;
hence thesis by A21,STRUCT_0:def 5;
end;
then reconsider IG as normal strict Subgroup of AutGroup G by Lm1;
take IG;
thus thesis;
end;
uniqueness by GROUP_2:59;
end;
theorem Th18:
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
let x,y be Element of InnAutGroup G;
let f,g be Element of InnAut G;
x is Element of AutGroup G & y is Element of AutGroup G by GROUP_2:42;
then consider x1, y1 be Element of AutGroup G such that
A1: x1 = x & y1 = y;
f is Element of Aut G & g is Element of Aut G by Th12;
then consider f1, g1 be Element of Aut G such that
A2: f1 = f & g1 = g;
assume x = f & y = g;
then x1 * y1 = f1 * g1 by A2,A1,Def2;
hence thesis by A2,A1,GROUP_2:43;
end;
theorem Th19:
id the carrier of G = 1_InnAutGroup G
proof
id the carrier of G = 1_AutGroup G by Th9;
hence thesis by GROUP_2:44;
end;
theorem
for f being Element of InnAut G for g being Element of InnAutGroup G
st f = g holds f" = g"
proof
let f be Element of InnAut G;
let g be Element of InnAutGroup G;
g is Element of AutGroup G by GROUP_2:42;
then consider g1 be Element of AutGroup G such that
A1: g1 = g;
f is Element of Aut G by Th12;
then consider f1 be Element of Aut G such that
A2: f1 = f;
assume f = g;
then f1" = g1" by A2,A1,Th10;
hence thesis by A2,A1,GROUP_2:48;
end;
definition
let G, b;
func Conjugate b -> Element of InnAut G means
:Def6:
for a holds it.a = a |^ b;
existence
proof
deffunc F(Element of G) = ($1) |^ b;
consider g be Function of the carrier of G, the carrier of G such that
A1: for a holds g.a = F(a) from FUNCT_2:sch 4;
g is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:8;
then reconsider g as Element of InnAut G by A1,Def4;
take g;
let a;
thus thesis by A1;
end;
uniqueness
proof
let f1, f2 be Element of InnAut G such that
A2: for a holds f1.a = a |^ b and
A3: for a holds f2.a = a |^ b;
for a holds f1.a = f2.a
proof
let a;
thus f1.a = a |^ b by A2
.= f2.a by A3;
end;
hence f1 = f2;
end;
end;
theorem Th21:
for a, b holds Conjugate (a * b) = (Conjugate b) * (Conjugate a)
proof
let a, b;
set f1 = Conjugate (a * b);
set f2 = ((Conjugate b) * (Conjugate a));
A1: for c holds f1.c = c |^ a |^ b
proof
let c;
c |^ (a * b) = c |^ a |^ b by GROUP_3:24;
hence thesis by Def6;
end;
A2: for c holds f1.c = (Conjugate b).(c |^ a)
proof
let c;
c |^ a |^ b = (Conjugate b).(c |^ a) by Def6;
hence thesis by A1;
end;
A3: for c holds f1.c = (Conjugate b).((Conjugate a).c)
proof
let c;
(Conjugate b).(c |^ a) = (Conjugate b).((Conjugate a).c) by Def6;
hence thesis by A2;
end;
for c holds f1.c = f2.c
proof
let c;
(Conjugate b).((Conjugate a).c) = f2.c by FUNCT_2:15;
hence thesis by A3;
end;
hence thesis;
end;
theorem Th22:
Conjugate 1_G = id the carrier of G
proof
for a holds (Conjugate 1_G).a = a
proof
let a;
a |^ 1_G = a by GROUP_3:19;
hence thesis by Def6;
end; then
for q being object st q in the carrier of G holds (Conjugate 1_G).q = q;
hence thesis;
end;
theorem Th23:
for a holds (Conjugate 1_G).a = a
proof
let a;
thus (Conjugate 1_G).a = a |^ 1_G by Def6
.= a by GROUP_3:19;
end;
theorem
for a holds (Conjugate a) * (Conjugate a") = Conjugate 1_G
proof
let a;
set f1 = (Conjugate a) * (Conjugate a");
set f2 = Conjugate 1_G;
A1: for b holds f1.b = b
proof
let b;
(Conjugate a).((Conjugate a").b) = (Conjugate a).(b |^ a") by Def6
.= b |^ a" |^ a by Def6
.= b by GROUP_3:25;
hence thesis by FUNCT_2:15;
end;
for b holds f1.b = f2.b
proof
let b;
thus f1.b = b by A1
.= f2.b by Th23;
end;
hence thesis;
end;
theorem Th25:
for a holds (Conjugate a") * (Conjugate a) = Conjugate 1_G
proof
let a;
set f1 = (Conjugate a") * (Conjugate a);
set f2 = Conjugate 1_G;
A1: for b holds f1.b = b
proof
let b;
(Conjugate a").((Conjugate a).b) = (Conjugate a").(b |^ a) by Def6
.= b |^ a |^ a" by Def6
.= b by GROUP_3:25;
hence thesis by FUNCT_2:15;
end;
for b holds f1.b = f2.b
proof
let b;
thus f1.b = b by A1
.= f2.b by Th23;
end;
hence thesis;
end;
theorem
for a holds Conjugate a" = (Conjugate a)"
proof
let a;
set f = Conjugate a;
set g = Conjugate a";
A1: g * f = Conjugate 1_G by Th25
.= id the carrier of G by Th22;
A2: f is Element of Aut G by Th12;
then f is Homomorphism of G, G by Def1;
then
A3: f is one-to-one by A2,Def1;
rng f = dom f by A2,Lm3
.= the carrier of G by A2,Lm3;
hence thesis by A1,A3,FUNCT_2:30;
end;
theorem
for a holds (Conjugate a) * (Conjugate 1_G) = Conjugate a &
(Conjugate 1_G) * (Conjugate a) = Conjugate a
proof
let a;
Conjugate 1_G = id the carrier of G by Th22;
hence thesis by FUNCT_2:17;
end;
theorem
for f being Element of InnAut G holds
f * Conjugate 1_G = f & (Conjugate 1_G) * f = f
proof
let f be Element of InnAut G;
Conjugate 1_G = id the carrier of G by Th22;
hence thesis by FUNCT_2:17;
end;
theorem
for G holds InnAutGroup G, G./.center G are_isomorphic
proof
let G;
deffunc F(Element of G) = Conjugate ($1)";
consider f be Function of the carrier of G, InnAut G such that
A1: for a holds f.a = F(a) from FUNCT_2:sch 4;
reconsider f as Function of the carrier of G, the carrier of InnAutGroup G
by Def5;
now
let a,b;
A2: f.(a * b) = Conjugate (a * b)" by A1
.= Conjugate (b" * a") by GROUP_1:17
.= (Conjugate a") * (Conjugate b") by Th21;
now
let A, B be Element of InnAutGroup G;
assume
A3: A = f.a & B = f.b;
then A = Conjugate a" & B = Conjugate b" by A1;
hence f.(a * b) = f.a * f.b by A2,A3,Th18;
end;
hence f.(a * b) = f.a * f.b;
end;
then reconsider f1 = f as Homomorphism of G, InnAutGroup G by GROUP_6:def 6;
A4: Ker f1 = center G
proof
set C = { a : for b holds a * b = b * a };
set KER = the carrier of Ker f1;
A5: KER = { a : f1.a = 1_InnAutGroup G } by GROUP_6:def 9;
A6: KER c= C
proof
let q be object;
assume
A7: q in KER;
1_InnAutGroup G = id the carrier of G by Th19;
then consider x such that
A8: q = x and
A9: f1.x = id the carrier of G by A5,A7;
A10: for b holds (Conjugate x").b = b
proof
let b;
(id the carrier of G).b = b;
hence thesis by A1,A9;
end;
A11: for b holds b |^ x" = b
proof
let b;
(Conjugate x").b = b |^ x" by Def6;
hence thesis by A10;
end;
for b holds x * b = b * x
proof
let b;
b |^ x" = x * b * x";
then x * b * x" * x = b * x by A11;
then x * b * (x" * x) = b * x by GROUP_1:def 3;
then x * b * 1_G = b * x by GROUP_1:def 5;
hence thesis by GROUP_1:def 4;
end;
hence thesis by A8;
end;
C c= KER
proof
let q be object;
assume q in C;
then consider x such that
A12: x = q and
A13: for b holds x * b = b * x;
consider g be Function of the carrier of G, the carrier of G such that
A14: g = Conjugate x";
A15: for b holds b = (Conjugate x").b
proof
let b;
x * b * x" = b * x * x" by A13;
then x * b * x" = b * (x * x") by GROUP_1:def 3;
then x * b * x" = b * 1_G by GROUP_1:def 5;
then b = b |^ x" by GROUP_1:def 4;
hence thesis by Def6;
end;
for b holds (id the carrier of G).b = g.b
by A15,A14;
then g = id the carrier of G;
then Conjugate x" = 1_InnAutGroup G by A14,Th19;
then f1.x = 1_InnAutGroup G by A1;
hence thesis by A5,A12;
end;
then KER = C by A6,XBOOLE_0:def 10;
hence thesis by GROUP_5:def 10;
end;
A16: the carrier of InnAutGroup G = InnAut G by Def5;
for q being object st q in the carrier of InnAutGroup G
ex q1 being object st q1 in the carrier
of G & q = f1.q1
proof
let q be object;
assume
A17: q in the carrier of InnAutGroup G;
then
A18: q is Element of InnAut G by Def5;
then consider
y1 be Function of the carrier of G, the carrier of G such that
A19: y1 = q;
y1 is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:9;
then consider b such that
A20: for a holds y1.a = a |^ b by A16,A17,A19,Def4;
take q1 = b";
thus q1 in the carrier of G;
f1.q1 = Conjugate b"" by A1
.= Conjugate b;
hence thesis by A18,A19,A20,Def6;
end;
then rng f1 = the carrier of InnAutGroup G by FUNCT_2:10;
then f1 is onto;
then InnAutGroup G = Image f1 by GROUP_6:57;
hence thesis by A4,GROUP_6:78;
end;
theorem
G is commutative Group implies
for f being Element of InnAutGroup G holds f = 1_InnAutGroup G
proof
assume
A1: G is commutative Group;
let f be Element of InnAutGroup G;
the carrier of InnAutGroup G = InnAut G by Def5;
then consider f1 be Element of InnAut G such that
A2: f1 = f;
f1 is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:8;
then consider a such that
A3: for x holds f1.x = x |^ a by Def4;
A4: for x holds f1.x = x
proof
let x;
thus f1.x = x |^ a by A3
.= x by A1,GROUP_3:29;
end;
for x holds f1.x = (id the carrier of G).x by A4;
then f1 = id the carrier of G;
hence thesis by A2,Th19;
end;
registration
let G be strict Group;
cluster -> multiplicative for Element of Aut G;
correctness by Def1;
end;
registration
let G be Group;
cluster AutGroup G -> non empty constituted-Functions;
coherence by MONOID_0:80;
end;