:: Lattice of Subgroups of a Group. Frattini Subgroup
::  by Wojciech A. Trybulec
::
:: Received August 22, 1990
:: Copyright (c) 1990-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 NUMBERS, XBOOLE_0, FINSEQ_1, ARYTM_1, GROUP_1, STRUCT_0, GROUP_2,
      SETFAM_1, SUBSET_1, RELAT_1, INT_1, TARSKI, GROUP_3, QC_LANG1, NEWTON,
      ARYTM_3, CARD_1, XXREAL_0, COMPLEX1, ALGSTR_0, CARD_3, FINSOP_1, BINOP_1,
      ORDINAL4, SETWISEO, FINSEQ_2, NAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      ZFMISC_1, RLSUB_1, BVFUNC_2, EQREL_1, PRE_TOPC, RLSUB_2, LATTICES,
      GROUP_4;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, FINSOP_1, ORDINAL1,
      NUMBERS, INT_1, SETWISEO, SETFAM_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1,
      FINSEQ_2, FINSEQ_3, FINSEQ_4, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_2,
      GROUP_3, LATTICES, GROUP_1, DOMAIN_1, XXREAL_0, NAT_1, INT_2;
 constructors PARTFUN1, SETFAM_1, BINOP_1, SETWISEO, XXREAL_0, NAT_1, NAT_D,
      FINSEQ_3, FINSEQ_4, FINSOP_1, REALSET1, REAL_1, LATTICES, GROUP_3,
      RELSET_1, FINSEQ_2, BINOP_2;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, NUMBERS, XREAL_0, INT_1,
      FINSEQ_1, STRUCT_0, LATTICES, GROUP_1, GROUP_2, GROUP_3, ORDINAL1,
      CARD_1, FINSEQ_2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

definition
  let D be non empty set;
  let F be FinSequence of D;
  let X be set;
  redefine func F - X -> FinSequence of D;
end;

scheme :: GROUP_4:sch 1
  MeetSbgEx{G() -> Group, P[set]}: ex H being strict Subgroup of G() st the
carrier of H = meet{A where A is Subset of G() : ex K being strict Subgroup of
  G() st A = the carrier of K & P[K]}
provided
 ex H being strict Subgroup of G() st P[H];

reserve x,y,X,Y for set,
  k,l,n for Nat,
  i,i1,i2,i3,j for Integer,
  G for Group,
  a,b,c,d for Element of G,
  A,B,C for Subset of G,
  H,H1,H2, H3 for Subgroup of G,
  h for Element of H,
  F,F1,F2 for FinSequence of the carrier of G,
  I,I1,I2 for FinSequence of INT;

scheme :: GROUP_4:sch 2
  SubgrSep{G() -> Group,P[set]}:
 ex X st X c= Subgroups G() & for H being
  strict Subgroup of G() holds H in X iff P[H];

definition
  let i;

  func @i -> Element of INT equals
:: GROUP_4:def 1
  i;
end;

theorem :: GROUP_4:1
  a = h implies a |^ n = h |^ n;

theorem :: GROUP_4:2
  a = h implies a |^ i = h |^ i;

theorem :: GROUP_4:3
  a in H implies a |^ n in H;

theorem :: GROUP_4:4
  a in H implies a |^ i in H;

definition
  let G be non empty multMagma;
  let F be FinSequence of the carrier of G;
  func Product F -> Element of G equals
:: GROUP_4:def 2
  (the multF of G) "**" F;
end;

theorem :: GROUP_4:5
  for G being associative unital non empty multMagma,
     F1,F2 being FinSequence of the carrier of G holds
     Product(F1 ^ F2) = Product(F1) * Product(F2);

theorem :: GROUP_4:6
  for G being unital non empty multMagma, F being FinSequence of the
carrier of G, a being Element of G holds Product(F ^ <* a *>) = Product(F) * a;

theorem :: GROUP_4:7
  for G being associative unital non empty multMagma, F being
FinSequence of the carrier of G, a being Element of G holds Product(<* a *> ^ F
  ) = a * Product(F);

theorem :: GROUP_4:8
  for G being unital non empty multMagma holds Product <*> the
  carrier of G = 1_G;

theorem :: GROUP_4:9
  for G being non empty multMagma, a being Element of G holds Product<*
  a *> = a;

theorem :: GROUP_4:10
  for G being non empty multMagma, a,b being Element of G holds Product
  <* a,b *> = a * b;

theorem :: GROUP_4:11
  Product<* a,b,c *> = a * b * c & Product<* a,b,c *> = a * (b * c);

theorem :: GROUP_4:12
  Product(n |-> a) = a |^ n;

theorem :: GROUP_4:13
  Product(F - {1_G}) = Product(F);

theorem :: GROUP_4:14
  len F1 = len F2 & (for k st k in dom F1 holds F2.(len F1 - k + 1
  ) = (F1/.k)") implies Product(F1) = Product(F2)";

theorem :: GROUP_4:15
  G is commutative Group implies for P being Permutation of dom F1 st F2
  = F1 * P holds Product(F1) = Product(F2);

theorem :: GROUP_4:16
  G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1
  = rng F2 implies Product(F1) = Product(F2);

theorem :: GROUP_4:17
  G is commutative Group & len F = len F1 & len F = len F2 & (for k st k
  in dom F holds F.k = (F1/.k) * (F2/.k)) implies Product(F) = Product(F1) *
  Product(F2);

theorem :: GROUP_4:18
  rng F c= carr H implies Product(F) in H;

definition
  let G,I,F;
  func F |^ I -> FinSequence of the carrier of G means
:: GROUP_4:def 3

  len it = len F & for k st k in dom F holds it.k = (F/.k) |^ @(I/.k);
end;

theorem :: GROUP_4:19
  len F1 = len I1 & len F2 = len I2 implies (F1 ^ F2) |^ (I1 ^ I2)
  = (F1 |^ I1) ^ (F2 |^ I2);

theorem :: GROUP_4:20
  rng F c= carr H implies Product(F |^ I) in H;

theorem :: GROUP_4:21
  (<*> the carrier of G) |^ (<*> INT) = {};

theorem :: GROUP_4:22
  <* a *> |^ <* @i *> = <* a |^ i *>;

theorem :: GROUP_4:23
  <* a,b *> |^ <* @i,@j *> = <* a |^ i,b |^ j *>;

theorem :: GROUP_4:24
  <* a,b,c *> |^ <* @i1,@i2,@i3 *> = <* a |^ i1,b |^ i2,c |^ i3 *>;

theorem :: GROUP_4:25
  F |^ (len F |-> @(1)) = F;

theorem :: GROUP_4:26
  F |^ (len F |-> @(0)) = len F |-> 1_G;

theorem :: GROUP_4:27
  len I = n implies (n |-> 1_G) |^ I = n |-> 1_G;

definition
  let G,A;
  func gr A -> strict Subgroup of G means
:: GROUP_4:def 4

  A c= the carrier of it & for
H being strict Subgroup of G st A c= the carrier of H holds it is Subgroup of H
  ;
end;

theorem :: GROUP_4:28
  a in gr A iff ex F,I st len F = len I & rng F c= A & Product(F |^ I) = a;

theorem :: GROUP_4:29
  a in A implies a in gr A;

theorem :: GROUP_4:30
  gr {} the carrier of G = (1).G;

theorem :: GROUP_4:31
  for H being strict Subgroup of G holds gr carr H = H;

theorem :: GROUP_4:32
  A c= B implies gr A is Subgroup of gr B;

theorem :: GROUP_4:33
  gr(A /\ B) is Subgroup of gr A /\ gr B;

theorem :: GROUP_4:34
  the carrier of gr A = meet{B : ex H being strict Subgroup of G
  st B = the carrier of H & A c= carr H};

theorem :: GROUP_4:35
  gr A = gr(A \ {1_G});

definition
  let G,a;
  attr a is generating means
:: GROUP_4:def 5

  not for A st gr A = the multMagma of G
  holds gr(A \ {a}) = the multMagma of G;
end;

theorem :: GROUP_4:36
  1_G is non generating;

definition
  let G, H;
  attr H is maximal means
:: GROUP_4:def 6

  the multMagma of H <> the multMagma of G &
for K being strict Subgroup of G st the multMagma of H <> K & H is Subgroup of
  K holds K = the multMagma of G;
end;

theorem :: GROUP_4:37
  for G being strict Group, H being strict Subgroup of G, a being
  Element of G holds H is maximal & not a in H implies gr(carr H \/ {a}) = G;

::
::  Frattini subgroup.
::

definition
  let G be Group;
::$N Frattini subgroup
  func Phi(G) -> strict Subgroup of G means
:: GROUP_4:def 7

  the carrier of it = meet{A
where A is Subset of G : ex H being strict Subgroup of G st A = the carrier of
H & H is maximal} if ex H being strict Subgroup of G st H is maximal otherwise
  it = the multMagma of G;
end;

theorem :: GROUP_4:38
  for G being Group holds (ex H being strict Subgroup of G st H is
  maximal) implies (a in Phi(G) iff for H being strict Subgroup of G st H is
  maximal holds a in H);

theorem :: GROUP_4:39
  for G being Group, a being Element of G holds (for H being strict
  Subgroup of G holds H is not maximal) implies a in Phi(G);

theorem :: GROUP_4:40
  for G being Group, H being strict Subgroup of G holds H is
  maximal implies Phi(G) is Subgroup of H;

theorem :: GROUP_4:41
  for G being strict Group holds the carrier of Phi(G) = {a where
  a is Element of G: a is non generating};

theorem :: GROUP_4:42
  for G being strict Group, a being Element of G holds a in Phi(G) iff a
  is non generating;

definition
  let G,H1,H2;
  func H1 * H2 -> Subset of G equals
:: GROUP_4:def 8
  carr H1 * carr H2;
end;

theorem :: GROUP_4:43
  H1 * H2 = carr H1 * carr H2 & H1 * H2 = H1 * carr H2 & H1 * H2 = carr
  H1 * H2;

theorem :: GROUP_4:44
  H1 * H2 * H3 = H1 * (H2 * H3);

theorem :: GROUP_4:45
  a * H1 * H2 = a * (H1 * H2);

theorem :: GROUP_4:46
  H1 * H2 * a = H1 * (H2 * a);

theorem :: GROUP_4:47
  A * H1 * H2 = A * (H1 * H2);

theorem :: GROUP_4:48
  H1 * H2 * A = H1 * (H2 * A);

definition
  let G,H1,H2;
  func H1 "\/" H2 -> strict Subgroup of G equals
:: GROUP_4:def 9
  gr(carr H1 \/ carr H2);
end;

theorem :: GROUP_4:49
  a in H1 "\/" H2 iff ex F,I st len F = len I & rng F c= carr H1 \/ carr
  H2 & a = Product(F |^ I);

theorem :: GROUP_4:50
  H1 "\/" H2 = gr(H1 * H2);

theorem :: GROUP_4:51
  H1 * H2 = H2 * H1 implies the carrier of H1 "\/" H2 = H1 * H2;

theorem :: GROUP_4:52
  G is commutative Group implies the carrier of H1 "\/" H2 = H1 * H2;

theorem :: GROUP_4:53
  for N1,N2 being strict normal Subgroup of G holds the carrier of
  N1 "\/" N2 = N1 * N2;

theorem :: GROUP_4:54
  for N1,N2 being strict normal Subgroup of G holds N1 "\/" N2 is normal
  Subgroup of G;

theorem :: GROUP_4:55
  for H being strict Subgroup of G holds H "\/" H = H;

theorem :: GROUP_4:56
  H1 "\/" H2 = H2 "\/" H1;

theorem :: GROUP_4:57
  H1 "\/" H2 "\/" H3 = H1 "\/" (H2 "\/" H3);

theorem :: GROUP_4:58
  for H being strict Subgroup of G holds (1).G "\/" H = H & H "\/" (1).G = H;

theorem :: GROUP_4:59
  (Omega).G "\/" H = (Omega).G & H "\/" (Omega).G = (Omega).G;

theorem :: GROUP_4:60
  H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2;

theorem :: GROUP_4:61
  for H2 being strict Subgroup of G holds H1 is Subgroup of H2 iff
  H1 "\/" H2 = H2;

theorem :: GROUP_4:62
  H1 is Subgroup of H2 implies H1 is Subgroup of H2 "\/" H3;

theorem :: GROUP_4:63
  for H3 being strict Subgroup of G holds H1 is Subgroup of H3 & H2 is
  Subgroup of H3 implies H1 "\/" H2 is Subgroup of H3;

theorem :: GROUP_4:64
  for H3,H2 being strict Subgroup of G holds H1 is Subgroup of H2
  implies H1 "\/" H3 is Subgroup of H2 "\/" H3;

theorem :: GROUP_4:65
  H1 /\ H2 is Subgroup of H1 "\/" H2;

theorem :: GROUP_4:66
  for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2;

theorem :: GROUP_4:67
  for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1;

theorem :: GROUP_4:68
  for H1,H2 being strict Subgroup of G holds H1 "\/" H2 = H2 iff H1 /\ H2 = H1;

reserve S1,S2 for Element of Subgroups G;

definition
  let G;
  func SubJoin G -> BinOp of Subgroups G means
:: GROUP_4:def 10

  for H1,H2 being strict Subgroup of G holds it.(H1,H2) = H1 "\/" H2;
end;

definition
  let G;
  func SubMeet G -> BinOp of Subgroups G means
:: GROUP_4:def 11

  for H1,H2 being strict Subgroup of G holds it.(H1,H2) = H1 /\ H2;
end;

definition
  let G be Group;
  func lattice G -> strict Lattice equals
:: GROUP_4:def 12
  LattStr (# Subgroups G, SubJoin G,
    SubMeet G #);
end;

theorem :: GROUP_4:69
  the carrier of lattice G = Subgroups G;

theorem :: GROUP_4:70
  the L_join of lattice G = SubJoin G;

theorem :: GROUP_4:71
  the L_meet of lattice G = SubMeet G;

registration
  let G be Group;
  cluster lattice G -> lower-bounded upper-bounded;
end;

theorem :: GROUP_4:72
  Bottom lattice G = (1).G;

theorem :: GROUP_4:73
  Top lattice G = (Omega).G;