:: On the Group of Automorphisms of Universal Algebra & Many
:: Sorted Algebra
::  by Artur Korni{\l}owicz
::
:: Received December 13, 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 UNIALG_1, FUNCT_1, RELAT_1, STRUCT_0, MSUALG_3, FUNCT_2,
      SUBSET_1, XBOOLE_0, TARSKI, BINOP_1, GROUP_1, ALGSTR_0, PBOOLE, PZFMISC1,
      FUNCOP_1, MEMBER_1, MSUALG_1, CARD_3, CARD_1, MSUHOM_1, CQC_SIM1,
      GROUP_6, ZFMISC_1, WELLORD1, AUTALG_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE,
      PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, FUNCOP_1, STRUCT_0, ALGSTR_0,
      FINSEQ_1, BINOP_1, GROUP_1, GROUP_6, CARD_3, PZFMISC1, UNIALG_1,
      UNIALG_2, ALG_1, MSUALG_1, MSUALG_3, MSUHOM_1;
 constructors BINOP_1, CARD_3, PZFMISC1, GROUP_6, ALG_1, MSUALG_3, MSUHOM_1,
      RELSET_1, NUMBERS;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, FUNCOP_1, PBOOLE,
      STRUCT_0, MSUALG_1, SUBSET_1;
 requirements BOOLE, SUBSET;


begin

:: On the Group of Automorphisms of Universal Algebra

reserve UA for Universal_Algebra,
  f, g for Function of UA, UA;

theorem :: AUTALG_1:1
  id the carrier of UA is_isomorphism;

definition
  let UA;
  func UAAut UA -> FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
  means
:: AUTALG_1:def 1

  for h be Function of UA, UA holds h in it iff h is_isomorphism;
end;

theorem :: AUTALG_1:2
  UAAut UA c= Funcs (the carrier of UA, the carrier of UA);

theorem :: AUTALG_1:3
  id the carrier of UA in UAAut UA;

theorem :: AUTALG_1:4
  for f, g st f is Element of UAAut UA & g = f" holds g is_isomorphism;

theorem :: AUTALG_1:5
  for f be Element of UAAut UA holds f" in UAAut UA;

theorem :: AUTALG_1:6
  for f1, f2 be Element of UAAut UA holds f1 * f2 in UAAut UA;

definition
  let UA;
  func UAAutComp UA -> BinOp of UAAut UA means
:: AUTALG_1:def 2

  for x, y be Element of UAAut UA holds it.(x, y) = y * x;
end;

definition
  let UA;
  func UAAutGroup UA -> Group equals
:: AUTALG_1:def 3
  multMagma (# UAAut UA, UAAutComp UA #);
end;

registration
  let UA;
  cluster UAAutGroup UA -> strict;
end;

theorem :: AUTALG_1:7
  for x, y be Element of UAAutGroup UA for f, g be Element of UAAut UA
  st x = f & y = g holds x * y = g * f;

theorem :: AUTALG_1:8
  id the carrier of UA = 1_UAAutGroup UA;

theorem :: AUTALG_1:9
  for f be Element of UAAut UA for g be Element of UAAutGroup UA st f =
  g holds f" = g";

begin

:: Some properties of Many Sorted Functions

reserve I for set,
  A, B, C for ManySortedSet of I;

theorem :: AUTALG_1:10
  A is_transformable_to B & B is_transformable_to C implies A
  is_transformable_to C;

theorem :: AUTALG_1:11
  for x be set, A be ManySortedSet of {x} holds A = x .--> A.x;

theorem :: AUTALG_1:12
  for A, B be non-empty ManySortedSet of I for F be
  ManySortedFunction of A, B st F is "1-1" "onto" holds F"" is "1-1" "onto";

theorem :: AUTALG_1:13
  for A, B be non-empty ManySortedSet of I for F be ManySortedFunction
  of A, B st F is "1-1" "onto" holds (F"")"" = F;

theorem :: AUTALG_1:14
  for F, G being Function-yielding Function st F is "1-1" & G is
  "1-1" holds G ** F is "1-1";

theorem :: AUTALG_1:15
  for B, C be non-empty ManySortedSet of I for F be
ManySortedFunction of A, B for G be ManySortedFunction of B, C st F is "onto" &
  G is "onto" holds G ** F is "onto";

theorem :: AUTALG_1:16
  for A, B, C be non-empty ManySortedSet of I for F be
  ManySortedFunction of A, B for G be ManySortedFunction of B, C st F is "1-1"
  "onto" & G is "1-1" "onto" holds (G ** F)"" = (F"") ** (G"");

theorem :: AUTALG_1:17
  for A, B be non-empty ManySortedSet of I for F be
ManySortedFunction of A, B for G be ManySortedFunction of B, A st F is "1-1" &
  F is "onto" & G ** F = id A holds G = F"";

theorem :: AUTALG_1:18
  A is_transformable_to B implies (Funcs)(A,B) is non-empty;

definition
  let I, A, B;
  assume
 A is_transformable_to B;
  func MSFuncs(A,B) -> non empty set equals
:: AUTALG_1:def 4

  product (Funcs)(A,B);
end;

theorem :: AUTALG_1:19
  A is_transformable_to B implies
  for x be set st x in MSFuncs(A,B) holds
  x is ManySortedFunction of A,B;

theorem :: AUTALG_1:20
  A is_transformable_to B implies
  for g be ManySortedFunction of A, B holds g in MSFuncs(A,B);

registration
  let I, A;
  cluster (Funcs)(A,A) -> non-empty;
end;

definition
  let I be set;
  let D be ManySortedSet of I;
  let A be non empty Subset of MSFuncs(D,D);
  redefine mode Element of A -> ManySortedFunction of D,D;
end;

registration
  let I,A;
  cluster id A -> "onto";
  cluster id A -> "1-1";
end;

begin

:: On the Group of Automorphisms of Many Sorted Algebra

reserve S for non void non empty ManySortedSign,
  U1, U2 for non-empty MSAlgebra over S;

definition
  let S, U1, U2;
  mode MSFunctionSet of U1, U2 is
       non empty Subset of MSFuncs(the Sorts of U1, the Sorts of U2);
end;

theorem :: AUTALG_1:21
  id the Sorts of U1 in MSFuncs(the Sorts of U1, the Sorts of U1);

definition
  let S, U1;
  func MSAAut U1 -> MSFunctionSet of U1,U1 means
:: AUTALG_1:def 5

  for h be ManySortedFunction of U1, U1 holds h in it iff
  h is_isomorphism U1, U1;
end;

theorem :: AUTALG_1:22
  for f be Element of MSAAut U1 holds
  f in MSFuncs(the Sorts of U1, the Sorts of U1);

theorem :: AUTALG_1:23
  MSAAut U1 c= MSFuncs(the Sorts of U1, the Sorts of U1);

theorem :: AUTALG_1:24
  id the Sorts of U1 in MSAAut U1;

theorem :: AUTALG_1:25
  for f be Element of MSAAut U1 holds f"" in MSAAut U1;

theorem :: AUTALG_1:26
  for f1, f2 be Element of MSAAut U1 holds f1 ** f2 in MSAAut U1;

theorem :: AUTALG_1:27
  for F be ManySortedFunction of MSAlg UA, MSAlg UA
  for f be Element of UAAut UA st F = 0 .--> f holds F in MSAAut MSAlg UA;

definition
  let S, U1;
  func MSAAutComp U1 -> BinOp of MSAAut U1 means
:: AUTALG_1:def 6

  for x, y be Element of MSAAut U1 holds it.(x, y) = y ** x;
end;

definition
  let S, U1;
  func MSAAutGroup U1 -> Group equals
:: AUTALG_1:def 7
  multMagma (# MSAAut U1, MSAAutComp U1 #);
end;

registration
  let S, U1;
  cluster MSAAutGroup U1 -> strict;
end;

theorem :: AUTALG_1:28
  for x, y be Element of MSAAutGroup U1 for f, g be Element of MSAAut U1
  st x = f & y = g holds x * y = g ** f;

theorem :: AUTALG_1:29
  id the Sorts of U1 = 1_MSAAutGroup U1;

theorem :: AUTALG_1:30
  for f be Element of MSAAut U1 for g be Element of MSAAutGroup U1 st
  f = g holds f"" = g";

begin

:: On the Relationship of Automorphisms of 1-Sorted and Many Sorted Algebras

theorem :: AUTALG_1:31
  for UA1, UA2 be Universal_Algebra st UA1, UA2 are_similar
  for F be ManySortedFunction of MSAlg UA1, (MSAlg UA2 Over MSSign UA1) holds
  F.0 is Function of UA1, UA2;

theorem :: AUTALG_1:32
  for f be Element of UAAut UA holds
  0 .--> f is ManySortedFunction of MSAlg UA, MSAlg UA;

theorem :: AUTALG_1:33
  for h be Function st (dom h = UAAut UA & for x be object st x in
  UAAut UA holds h.x = 0 .--> x) holds h is Homomorphism of UAAutGroup UA,
  MSAAutGroup (MSAlg UA);

theorem :: AUTALG_1:34
  for h be Homomorphism of UAAutGroup UA, MSAAutGroup (MSAlg UA)
  st for x be object st x in UAAut UA holds h.x = 0 .--> x
  holds h is bijective;

theorem :: AUTALG_1:35
  UAAutGroup UA, MSAAutGroup (MSAlg UA) are_isomorphic;