Re: Mizar theorem GROUP_6:93
Alex Nelson thmprover _AT_ gmail.com <[email protected]> Fri, 8 Dec 2023 06:46:19 -0800
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAA+9CX0W3bzRmLc=pNjXvdb2BGYbku57LtMbtT1_otXQOFx=_A@mail.gmail.com> |
--00000000000055961b060c00a673 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hello, So here's my understanding: suppose we have in Mizar a "N being normal Subgroup of G" and "H being Subgroup of G". We know that if `N` is a Subgroup of `H`, then `N` is a normal subgroup of H. However, Mizar does not know this. To communicate this to Mizar, we introduce this "hack", writing "(H,N)`*`" to say "Consider N as a normal Subgroup of H". This allows us to do things like write down "H./.(H,N)`*`" whereas in Mathematics we could write down H/N. Similarly, the group SN in Mizar is S "\/" N. Mathematics is actually quite sloppy in its notation here, since SN should *not* be confused with the *set* S*N. The group S "\/" N is defined in GROUP_4 as the lattice join of subgroups, i.e., the subgroup generated by S*N, or in Mizar code "gr ((carr S)*(carr N))". (See https://mizar.uwb.edu.pl/version/current/html/group_4.html#K8) Now, we see the two groups which are declared isomorphic are (B "\/" N)./.(B "\/" N,N)`*` --- which in "normal mathematics" is BN/N --- and B./.(B /\ N) --- which is "normal mathematics" is B/(B\cap N). I hope this helps, I just woke up and have yet to have my morning coffee, so I might have erred accidentally in my excitement to answer. Best, Alex On Fri, Dec 8, 2023 at 5:56=E2=80=AFAM Victor Makarov viktmak _AT_ gmail.co= m < [email protected]> wrote: > Dear Forum: > > I am trying to understand the statement of the theorem GROUP_6:93: > > > https://mx10.uwb.edu.pl/fmlurlsvc/?fewReq=3D:B:JVk/NDA9PyNzODcrNSNsYTg1ND= 81NCN2bGJrZHFwd2A4PWM1MzJjZDRjNmBmNzQ0ZmA9NmRkNzM0M2RkPWBjYDFmYGE3ZmcxNCNxO= DQyNTc1MTYwPDEjdGxhODZHPUF3QFBdNTc2MDY2KDZHPUF3QFBcNTc2MDY2I3dmdXE4aGx/ZHco= Y2p3cGhFaGx/ZHcrcHJnK2BhcCt1aSNmODY8I21haTg1&url=3Dhttp%3a%2f%2fmizar.org%2= fJFM%2fVol3%2fgroup_6.abs.html%23K2 > > theorem :: GROUP_6:93 > for N being strict normal Subgroup of G holds > (B "\/" N)./.(B "\/" N,N)`*`, B./.(B /\ N) are_isomorphic; > > What does mean (B "\/" N)" and (B "\/" N,N)`*` ? > > How is the theorem GROUP_6:93 related to the Second Isomorphism Theorem? > > Second Isomorphism Theorem: > (Theorem B in Wikipedia): > > https://mx10.uwb.edu.pl/fmlurlsvc/?fewReq=3D:B:JVk/NDA9PyNzODcrNSNsYTg1ND= 81NCN2bGJrZHFwd2A4MWEwYTYyMTZkMz02NzIzZDdmM2Y0ZmBkPDAxPGQ0N2AyNjI3NTIxMSNxO= DQyNTc1MTYwPDEjdGxhODZHPUF3QFBdNTc2MDY2KDZHPUF3QFBcNTc2MDY2I3dmdXE4aGx/ZHco= Y2p3cGhFaGx/ZHcrcHJnK2BhcCt1aSNmODY8I21haTg1&url=3Dhttps%3a%2f%2fen.wikiped= ia.org%2fwiki%2fIsomorphism_theorems > > Theorem B (groups) > > Let G be a group. Let S be a subgroup of G, and let N be a normal subgrou= p > of G. > Then the following hold: > > The product SN is a subgroup of G, > The subgroup N is a normal subgroup of SN}, > The intersection S/\N is a normal subgroup of S, and > The quotient groups (SN)/N and S/(S/\N)} are isomorphic. > (Wikipedia uses another symbol(\cap) for the intersection). > > Thanks in advance, > > Victor Makarov > > --00000000000055961b060c00a673 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable <html><body><div dir=3D"ltr"><div>Hello,<br><br></div><div>So here's = my understanding: suppose we have in Mizar a "N being normal Subgrou= p of G" and "H being Subgroup of G". We know that if `N` i= s a Subgroup of `H`, then `N` is a normal subgroup of H. However, Mizar d= oes not know this. To communicate this to Mizar, we introduce this "= hack", writing "(H,N)`*`" to say "Consider N as a nor= mal Subgroup of H".</div><div><br></div><div>This allows us to do th= ings like write down "H./.(H,N)`*`" whereas in Mathematics we c= ould write down H/N.</div><div><br></div><div>Similarly, the group SN in = Mizar is S "\/" N. Mathematics is actually quite sloppy in its = notation here, since SN should <b>not</b> be confused with the <i>set</i>= S*N. The group S "\/" N is defined in GROUP_4 as the lattice j= oin of subgroups, i.e., the subgroup generated by S*N, or in Mizar code &= quot;gr ((carr S)*(carr N))". (See <a href=3D"https://mizar.uwb.edu.= pl/version/current/html/group_4.html#K8">https://mizar.uwb.edu.pl/version= /current/html/group_4.html#K8</a>)</div><div><br></div><div>Now, we see t= he two groups which are declared isomorphic are (B "\/" N)./.(B= "\/" N,N)`*` --- which in "normal mathematics" is BN= /N --- and B./.(B /\ N) --- which is "normal mathematics" is B/= (B\cap N).<br><br></div><div>I hope this helps, I just woke up and have y= et to have my morning coffee, so I might have erred accidentally in my ex= citement to answer.<br><br></div><div>Best,<br></div><div>Alex<br></div><= /div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr"= >On Fri, Dec 8, 2023 at 5:56 AM Victor Makarov viktmak _AT_ <a hre= f=3D"https://mx11.uwb.edu.pl/fmlurlsvc/?fewReq=3D:B:JVo+NTE8PiJyOTYqNCJtY= Dk0NT40NSJ3bWNqZXBxdmE5MTdmPTU9Mj00MzBmPDc3ZTUxZTA2ZmZmYDJgPDFmMjNnMTZhZ2= EzPCJwOTUzNDY0MDI8MTUidW1gOTdGPEFoUmxDNDY2NDM3KTdGPEFoUmxMNDY2NDM3InZndHA= 5aW1+ZXYpYmt2cWlEaW1+ZXYqcXNmKmFgcSp0aCJnOTY3ImxgaDk0&url=3Dhttp%3a%2f%2f= gmail.com">gmail.com</a> <<a href=3D"mailto:[email protected]= b.edu.pl">[email protected]</a>> wrote:<br></div><blo= ckquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-le= ft:1px solid rgb(204,204,204);padding-left:1ex">Dear Forum:<br><br> I am trying to understand the statement of the theorem GROUP_6:93:<br><br= ><a href=3D"https://mx10.uwb.edu.pl/fmlurlsvc/?fewReq=3D:B:JVk/NDA9PyNzOD= crNSNsYTg1ND81NCN2bGJrZHFwd2A4PWM1MzJjZDRjNmBmNzQ0ZmA9NmRkNzM0M2RkPWBjYDF= mYGE3ZmcxNCNxODQyNTc1MTYwPDEjdGxhODZHPUF3QFBdNTc2MDY2KDZHPUF3QFBcNTc2MDY2= I3dmdXE4aGx/ZHcoY2p3cGhFaGx/ZHcrcHJnK2BhcCt1aSNmODY8I21haTg1&url=3Dht= tp%3a%2f%2fmizar.org%2fJFM%2fVol3%2fgroup_6.abs.html%23K2" rel=3D"norefer= rer">https://mx10.uwb.edu.pl/fmlurlsvc/?fewReq=3D:B:JVk/NDA9PyNzODcrNSNsY= Tg1ND81NCN2bGJrZHFwd2A4PWM1MzJjZDRjNmBmNzQ0ZmA9NmRkNzM0M2RkPWBjYDFmYGE3Zm= cxNCNxODQyNTc1MTYwPDEjdGxhODZHPUF3QFBdNTc2MDY2KDZHPUF3QFBcNTc2MDY2I3dmdXE= 4aGx/ZHcoY2p3cGhFaGx/ZHcrcHJnK2BhcCt1aSNmODY8I21haTg1&url=3Dhttp%3a%2= f%2fmizar.org%2fJFM%2fVol3%2fgroup_6.abs.html%23K2</a> <br><br> theorem :: GROUP_6:93<br> for N being strict normal Subgroup of G holds<br> (B "\/" N)./.(B "\/" N,N)`*`, B./.(B /\ N) are_= isomorphic;<br><br> What does mean (B "\/" N)" and (B "\/" N,N)`*` ?= <br><br> How is the theorem GROUP_6:93 related to the Second Isomorphism The= orem?<br><br> Second Isomorphism Theorem:<br> (Theorem B in Wikipedia):<br><a href=3D"https://mx10.uwb.edu.pl/fmlurlsvc= /?fewReq=3D:B:JVk/NDA9PyNzODcrNSNsYTg1ND81NCN2bGJrZHFwd2A4MWEwYTYyMTZkMz0= 2NzIzZDdmM2Y0ZmBkPDAxPGQ0N2AyNjI3NTIxMSNxODQyNTc1MTYwPDEjdGxhODZHPUF3QFBd= NTc2MDY2KDZHPUF3QFBcNTc2MDY2I3dmdXE4aGx/ZHcoY2p3cGhFaGx/ZHcrcHJnK2BhcCt1a= SNmODY8I21haTg1&url=3Dhttps%3a%2f%2fen.wikipedia.org%2fwiki%2fIsomorp= hism_theorems" rel=3D"noreferrer">https://mx10.uwb.edu.pl/fmlurlsvc/?fewR= eq=3D:B:JVk/NDA9PyNzODcrNSNsYTg1ND81NCN2bGJrZHFwd2A4MWEwYTYyMTZkMz02NzIzZ= DdmM2Y0ZmBkPDAxPGQ0N2AyNjI3NTIxMSNxODQyNTc1MTYwPDEjdGxhODZHPUF3QFBdNTc2MD= Y2KDZHPUF3QFBcNTc2MDY2I3dmdXE4aGx/ZHcoY2p3cGhFaGx/ZHcrcHJnK2BhcCt1aSNmODY= 8I21haTg1&url=3Dhttps%3a%2f%2fen.wikipedia.org%2fwiki%2fIsomorphism_t= heorems</a> <br><br> Theorem B (groups)<br><br> Let G be a group. Let S be a subgroup of G, and let N be a normal subgrou= p of G.<br> Then the following hold:<br><br> The product SN is a subgroup of G,<br> The subgroup N is a normal subgroup of SN},<br> The intersection S/\N is a normal subgroup of S, and<br> The quotient groups (SN)/N and S/(S/\N)} are isomorphic.<br> (Wikipedia uses another symbol(\cap) for the intersection).<br><br> Thanks in advance,<br><br> Victor Makarov<br><br></blockquote></div></body></html> --00000000000055961b060c00a673--