:: On the Lattice of Subgroups of a Group :: by Janusz Ganczarski :: :: Received May 23, 1995 :: Copyright (c) 1995-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 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;