:: Equivalent Expressions of Direct Sum Decomposition of Groups
::  by Kazuhisa Nakasho , Hiroyuki Okazaki , Hiroshi Yamazaki and Yasunari Shidama
::
:: Received February 26, 2015
:: Copyright (c) 2015-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 FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI, BINOP_1,
      GROUP_1, XXREAL_0, GROUP_2, CARD_1, NUMBERS, FUNCT_4, GROUP_6, FUNCOP_1,
      GROUP_12, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0, STRUCT_0, NAT_1,
      ORDINAL4, PRE_TOPC, ARYTM_1, ARYTM_3, FINSET_1, NEWTON, GROUP_4,
      PRE_POLY, UPROOTS, GROUP_19, SEMI_AF1, QC_LANG1, VECTMETR, GROUP_20;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
      PARTFUN1, FUNCT_2, DOMAIN_1, FUNCT_3, FUNCOP_1, FUNCT_4, FINSET_1,
      CARD_1, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, FINSEQ_1, FUNCT_7, STRUCT_0,
      ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_6, PRALG_1, GRSOLV_1,
      GROUP_7, GROUP_12, GROUP_19;
 constructors REALSET1, FUNCT_4, MONOID_0, PRALG_1, GROUP_4, FUNCT_7, RELSET_1,
      INT_7, FUNCT_3, GROUP_17, GRSOLV_1, GROUP_19;
 registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1,
      FUNCT_2, FUNCOP_1, CARD_1, GROUP_7, GROUP_3, RELSET_1, SUBSET_1, INT_1,
      FINSET_1, RELAT_1, FUNCT_1, NUMBERS, GROUP_12, GROUP_6, GROUP_19;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: 1. Internal Direct Sum Decomposition into Normal Subgroups

definition
  let I be set, G be Group;
  mode Subgroup-Family of I,G -> Group-Family of I means
:: GROUP_20:def 1
  for i being object st i in I holds it.i is Subgroup of G;
end;

definition
  let I be set, G be Group, F be Subgroup-Family of I,G;
  attr F is component-commutative means
:: GROUP_20:def 2
  for i,j be object, gi,gj be Element of G
  st i in I & j in I & i <> j
  ex Fi,Fj being Subgroup of G st Fi = F.i & Fj = F.j &
  (gi in Fi & gj in Fj implies gi * gj = gj * gi);
end;

definition
  let I be non empty set, G be Group, F be Subgroup-Family of I,G;
  redefine attr F is component-commutative means
:: GROUP_20:def 3
  for i,j be Element of I, gi,gj be Element of G
  st i <> j & gi in F.i & gj in F.j
  holds gi * gj = gj * gi;
end;

registration
  let I be non empty set, G be Group;
  cluster component-commutative for Subgroup-Family of I,G;
end;

theorem :: GROUP_20:1
  for G be Group, H be normal Subgroup of G, x,y be Element of G st y in H
  holds x * y * x" in H & x * (y * x") in H;

theorem :: GROUP_20:2
  for I be non empty set,
      G be Group,
      F be Group-Family of I,
      x be Function of I,G
  st x in product F
  holds x is Function of I,Union(Carrier F);

theorem :: GROUP_20:3
  for I be non empty set,
      G be Group,
      H be Subgroup of G,
      x be Function of I,G,
      y be Function of I,H
  st x = y
  holds support x = support y;

theorem :: GROUP_20:4
  for I be non empty set,
      G be Group,
      H be Subgroup of G,
      y be finite-support Function of I,H
  holds y is finite-support Function of I,G;

theorem :: GROUP_20:5
  for I be non empty set,
      G be Group,
      H be Subgroup of G,
      x be finite-support Function of I,G
  st rng x c= [#]H
  holds x is finite-support Function of I,H;

theorem :: GROUP_20:6
  for I be non empty set,
      G be Group,
      H be Subgroup of G,
      x be finite-support Function of I,G,
      y be finite-support Function of I,H
  st x = y
  holds Product x = Product y;

theorem :: GROUP_20:7
  for f be Function, i,x be set
  holds f = f +* (i,x) +* (i,f.i);

theorem :: GROUP_20:8
  for I be non empty set, G be Group,
      F be component-commutative Subgroup-Family of I,G,
      x,y be finite-support Function of I,G,
      i be Element of I
  st y = x +* (i,1_F.i) & x in product F
  holds Product x = Product(y) * x.i = x.i * Product(y);

theorem :: GROUP_20:9
  for I be non empty set, G be Group,
      F be component-commutative Subgroup-Family of I,G,
      UF be Subset of G
  holds
    for i be Element of I, x,y be finite-support Function of I,gr UF
    st y = x +* (i,1_F.i) & x in product F
    holds Product x = Product(y) * x.i = x.i * Product(y);

theorem :: GROUP_20:10
  for I be non empty set, G be Group,
      F be component-commutative Subgroup-Family of I,G,
      UF be Subset of G
  holds
    for y be finite-support Function of I,gr UF,
        i be Element of I, g be Element of gr UF
    st y in product F & y.i = 1_F.i & g in F.i
    holds Product(y) * g = g * Product(y);

theorem :: GROUP_20:11
  for I be non empty set, G be Group,
      F be component-commutative Subgroup-Family of I,G,
      UF be Subset of G
  st UF = Union Carrier F
  holds
    for g be Element of G,
        H be FinSequence of G,
        K be FinSequence of INT
    st len H = len K & rng H c= UF & Product(H|^K) = g
    holds
      ex f be finite-support Function of I,G
      st f in product F & g = Product f;

theorem :: GROUP_20:12
  for I be non empty set,
      G be Group,
      F be Subgroup-Family of I,G,
      h,h0 be finite-support Function of I,G,
      i be Element of I,
      UFi be Subset of G
  st UFi = Union((Carrier F) | (I \ {i}))
   & h0 = h +* (i, 1_F.i)
   & h in product F
  holds Product h0 in gr UFi;

theorem :: GROUP_20:13
  for I be non empty set, G be Group,
      F be component-commutative Subgroup-Family of I,G,
      UF be Subset of G
  st UF = Union Carrier F
  holds
    for g be Element of G st g in gr UF holds
    ex f be finite-support Function of I,gr UF
    st f in sum F & g = Product f;

theorem :: GROUP_20:14
  for I be non empty set, G be Group,
      F be component-commutative Subgroup-Family of I,G,
      UF be Subset of G
  st UF = Union Carrier F
  holds
    for i be Element of I holds F.i is normal Subgroup of gr UF;

theorem :: GROUP_20:15
  for I be non empty set,
      G be Group,
      F be component-commutative Subgroup-Family of I,G
  st for i be Element of I holds
     ex UFi be Subset of G
     st UFi = Union((Carrier F) | (I \ {i}))
      & [#]gr(UFi) /\ [#](F.i) = {1_G}
  holds
    for x1,x2 be finite-support Function of I,G
    st x1 in sum F & x2 in sum F & Product x1 = Product x2
    holds x1 = x2;

theorem :: GROUP_20:16
  for I be non empty set,
      G be strict Group,
      F be Group-Family of I
  holds
    F is internal DirectSumComponents of G,I
  iff
      (for i be Element of I holds F.i is normal Subgroup of G)
    & (ex UF be Subset of G st UF = Union Carrier F & gr(UF) = G)
    & for i be Element of I holds
      ex UFi be Subset of G
      st UFi = Union((Carrier F) | (I \ {i}))
       & [#](gr(UFi)) /\ [#](F.i) = {1_G};

begin :: 2. Internal Direct Sum Decomposition for Commutative Group

theorem :: GROUP_20:17
  for I be non empty set,
      G be commutative Group,
      F be Group-Family of I
  holds
    F is internal DirectSumComponents of G,I
  iff
    (for i be Element of I holds F.i is Subgroup of G)
   &(for i,j be Element of I st i <> j holds
     [#] (F.i) /\ [#] (F.j) = {1_G})
   &(for y be Element of G
     ex x be finite-support Function of I,G
     st x in sum F & y = Product(x))
   &(for x1,x2 be finite-support Function of I,G
     st x1 in sum F & x2 in sum F & Product(x1) = Product(x2)
     holds x1 = x2);

begin :: 3. Equivalence between Internal and External Direct Sum

theorem :: GROUP_20:18
  for I be non empty set,
      G be Group,
      F be Subgroup-Family of I,G,
      h be Homomorphism of sum F,G,
      a be finite-support Function of I,G
  st a in sum F
   & for i be Element of I, x be Element of F.i
     holds h.(1ProdHom(F,i).x) = x
  holds h.a = Product a;

theorem :: GROUP_20:19
  for I be non empty set,
      G be Group,
      M be DirectSumComponents of G,I
  holds
  ex f be Homomorphism of sum M,G,
     N be internal DirectSumComponents of G,I
  st f is bijective
   & for i be Element of I holds
     ex qi be Homomorphism of M.i,N.i
     st qi = f * 1ProdHom(M,i)
      & qi is bijective;