:: On the Lattice of Subgroups of a Group
:: by Janusz Ganczarski
::
:: Received May 23, 1995
:: Copyright (c) 1995-2019 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 GROUP_1, GROUP_2, STRUCT_0, XBOOLE_0, GROUP_3, SUBSET_1, GROUP_4,
EQREL_1, TARSKI, GROUP_6, RELAT_1, FUNCT_1, ZFMISC_1, SETFAM_1, RLSUB_2,
LATTICES, PBOOLE, REWRITE1, LATTICE3, VECTSP_8;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, SETFAM_1, RELAT_1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, ALGSTR_0, LATTICES, GROUP_1,
GROUP_2, GROUP_3, GROUP_4, GROUP_6, LATTICE3, LATTICE4, VECTSP_8;
constructors BINOP_1, REALSET1, GROUP_4, GROUP_6, LATTICE3, LATTICE4,
VECTSP_8, RELSET_1;
registrations SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES, GROUP_3,
GROUP_4, RELSET_1;
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;
theorem :: LATSUBGR:8
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:9
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:10
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:11
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:12
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;
theorem :: LATSUBGR:13
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:14
for G being Group for H being strict Subgroup of G holds 1_G in carr G .H;
theorem :: LATSUBGR:15
for G being Group for H being strict Subgroup of G holds carr G.H <>
{};
theorem :: LATSUBGR:16
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:17
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:18
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:19
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:20
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:21
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:22
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:23
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:24
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:25
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:26
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:27
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:28
for G being Group holds FuncLatt id the carrier of G = id the carrier
of lattice G;
theorem :: LATSUBGR:29
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:30
for G1, G2 being Group for f being Homomorphism of G1, G2 holds (
FuncLatt f).(1).G1 = (1).G2;
theorem :: LATSUBGR:31
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:32
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:33
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;