Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

### On the Lattice of Subgroups of a Group

by
Janusz Ganczarski

MML identifier: LATSUBGR
[ Mizar article, MML identifier index ]

```environ

vocabulary REALSET1, GROUP_2, BOOLE, GROUP_3, GROUP_4, LATTICES, GROUP_6,
RELAT_1, FUNCT_1, GROUP_1, SETFAM_1, RLSUB_2, BHSP_3, LATTICE3, VECTSP_8;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELAT_1, SETFAM_1,
PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, LATTICES, RLVECT_1, VECTSP_1,
GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_6, LATTICE3, LATTICE4,
VECTSP_8;
constructors DOMAIN_1, BINOP_1, GROUP_4, GROUP_6, LATTICE3, LATTICE4,
VECTSP_8;
clusters STRUCT_0, GROUP_1, GROUP_3, RELSET_1, SUBSET_1, GROUP_4, FUNCT_2,
PARTFUN1, XBOOLE_0;
requirements BOOLE, SUBSET;

begin

theorem :: LATSUBGR:1
for G being Group
for H1, H2 being Subgroup of G holds
the carrier of H1 /\ H2 = (the carrier of H1) /\ the carrier of H2;

theorem :: LATSUBGR:2
for G being Group
for h being set holds
h in Subgroups G iff ex H being strict Subgroup of G st h = H;

theorem :: LATSUBGR:3
for G being Group
for A being Subset of G
for H being strict Subgroup of G st
A = the carrier of H holds gr A = H;

theorem :: LATSUBGR:4
for G being Group
for H1, H2 being Subgroup of G
for A being Subset of G st
A = (the carrier of H1) \/ the carrier of H2 holds
H1 "\/" H2 = gr A;

theorem :: LATSUBGR:5
for G being Group
for H1, H2 being Subgroup of G
for g being Element of G holds
g in H1 or g in H2 implies g in H1 "\/" H2;

theorem :: LATSUBGR:6
for G1, G2 being Group
for f being Homomorphism of G1, G2
for H1 being Subgroup of G1 holds
ex H2 being strict Subgroup of G2 st
the carrier of H2 = f.:the carrier of H1;

theorem :: LATSUBGR:7
for G1, G2 being Group
for f being Homomorphism of G1, G2
for H2 being Subgroup of G2
ex H1 being strict Subgroup of G1 st
the carrier of H1 = f"the carrier of H2;

canceled 2;

theorem :: LATSUBGR:10
for G1, G2 being Group
for f being Homomorphism of G1, G2
for H1, H2 being Subgroup of G1
for H3, H4 being Subgroup of G2 st
the carrier of H3 = f.:the carrier of H1 &
the carrier of H4 = f.:the carrier of H2 holds
H1 is Subgroup of H2 implies H3 is Subgroup of H4;

theorem :: LATSUBGR:11
for G1, G2 being Group
for f being Homomorphism of G1, G2
for H1, H2 being Subgroup of G2
for H3, H4 being Subgroup of G1 st
the carrier of H3 = f"the carrier of H1 &
the carrier of H4 = f"the carrier of H2 holds
H1 is Subgroup of H2 implies H3 is Subgroup of H4;

theorem :: LATSUBGR:12
for G1, G2 being Group
for f being Function of the carrier of G1, the carrier of G2
for A being Subset of G1 holds
f.:A c= f.:the carrier of gr A;

theorem :: LATSUBGR:13
for G1, G2 being Group
for H1, H2 being Subgroup of G1
for f being Function of the carrier of G1, the carrier of G2
for A being Subset of G1 st
A = (the carrier of H1) \/ the carrier of H2 holds
f.:the carrier of H1 "\/" H2 = f.:the carrier of gr A;

theorem :: LATSUBGR:14
for G being Group
for A being Subset of G st
A = {1.G} holds gr A = (1).G;

definition
let G be Group;
func carr G -> Function of Subgroups G, bool the carrier of G means
:: LATSUBGR:def 1
for H being strict Subgroup of G holds it.H = the carrier of H;
end;

canceled 3;

theorem :: LATSUBGR:18
for G being Group
for H being strict Subgroup of G
for x being Element of G holds
x in carr G.H iff x in H;

theorem :: LATSUBGR:19
for G being Group
for H being strict Subgroup of G holds
1.G in carr G.H;

theorem :: LATSUBGR:20
for G being Group
for H being strict Subgroup of G holds
carr G.H <> {};

theorem :: LATSUBGR:21
for G being Group
for H being strict Subgroup of G
for g1, g2 being Element of G holds
g1 in carr G.H & g2 in carr G.H implies
g1 * g2 in carr G.H;

theorem :: LATSUBGR:22
for G being Group
for H being strict Subgroup of G
for g being Element of G holds
g in carr G.H implies g" in carr G.H;

theorem :: LATSUBGR:23
for G being Group
for H1, H2 being strict Subgroup of G holds
the carrier of H1 /\ H2 = carr G.H1 /\ carr G.H2;

theorem :: LATSUBGR:24
for G being Group
for H1, H2 being strict Subgroup of G holds
carr G.(H1 /\ H2) = carr G.H1 /\ carr G.H2;

definition
let G be Group;
let F be non empty Subset of Subgroups G;
func meet F -> strict Subgroup of G means
:: LATSUBGR:def 2
the carrier of it = meet (carr G.:F);
end;

theorem :: LATSUBGR:25
for G being Group
for F being non empty Subset of Subgroups G holds
(1).G in F implies meet F = (1).G;

theorem :: LATSUBGR:26
for G being Group
for h being Element of Subgroups G
for F being non empty Subset of Subgroups G st
F = { h } holds meet F = h;

theorem :: LATSUBGR:27
for G being Group
for H1, H2 being Subgroup of G
for h1, h2 being Element of lattice G st
h1 = H1 & h2 = H2 holds
h1 "\/" h2 = H1 "\/" H2;

theorem :: LATSUBGR:28
for G being Group
for H1, H2 being Subgroup of G
for h1, h2 being Element of lattice G st
h1 = H1 & h2 = H2 holds
h1 "/\" h2 = H1 /\ H2;

theorem :: LATSUBGR:29
for G being Group
for p being Element of lattice G
for H being Subgroup of G st p = H holds
H is strict Subgroup of G;

theorem :: LATSUBGR:30
for G being Group
for H1, H2 being Subgroup of G
for p, q being Element of lattice G st
p = H1 & q = H2 holds
p [= q iff the carrier of H1 c= the carrier of H2;

theorem :: LATSUBGR:31
for G being Group
for H1, H2 being Subgroup of G
for p, q being Element of lattice G st
p = H1 & q = H2 holds
p [= q iff H1 is Subgroup of H2;

theorem :: LATSUBGR:32
for G being Group holds lattice G is complete;

definition
let G1, G2 be Group;
let f be Function of the carrier of G1, the carrier of G2;
func FuncLatt f -> Function of the carrier of lattice G1,
the carrier of lattice G2 means
:: LATSUBGR:def 3
for H being strict Subgroup of G1, A being Subset of G2
st A = f.:the carrier of H holds it.H = gr A;
end;

theorem :: LATSUBGR:33
for G being Group holds
FuncLatt id the carrier of G = id the carrier of lattice G;

theorem :: LATSUBGR:34
for G1, G2 being Group
for f being Homomorphism of G1, G2 st f is one-to-one holds
FuncLatt f is one-to-one;

theorem :: LATSUBGR:35
for G1, G2 being Group
for f being Homomorphism of G1, G2 holds
(FuncLatt f).(1).G1 = (1).G2;

theorem :: LATSUBGR:36
for G1, G2 being Group
for f being Homomorphism of G1, G2 st f is one-to-one holds
FuncLatt f is Semilattice-Homomorphism of lattice G1, lattice G2;

theorem :: LATSUBGR:37
for G1, G2 being Group
for f being Homomorphism of G1, G2 holds
FuncLatt f is sup-Semilattice-Homomorphism of lattice G1, lattice G2;

theorem :: LATSUBGR:38
for G1, G2 being Group
for f being Homomorphism of G1, G2 st f is one-to-one holds
FuncLatt f is Homomorphism of lattice G1, lattice G2;
```