:: 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 );