Re: [mizar] Mizar theorem GROUP_6:93

[Alex Nelson <thmprover@gmail.com>]

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 AM Victor Makarov viktmak _AT_ gmail.com <owner-mizar-forum@mizar.uwb.edu.pl> wrote:

Dear Forum:

I am trying to understand the statement of the theorem GROUP_6:93:

https://mx10.uwb.edu.pl/fmlurlsvc/?fewReq=:B:JVk/NDA9PyNzODcrNSNsYTg1ND81NCN2bGJrZHFwd2A4PWM1MzJjZDRjNmBmNzQ0ZmA9NmRkNzM0M2RkPWBjYDFmYGE3ZmcxNCNxODQyNTc1MTYwPDEjdGxhODZHPUF3QFBdNTc2MDY2KDZHPUF3QFBcNTc2MDY2I3dmdXE4aGx/ZHcoY2p3cGhFaGx/ZHcrcHJnK2BhcCt1aSNmODY8I21haTg1&url="">

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=:B:JVk/NDA9PyNzODcrNSNsYTg1ND81NCN2bGJrZHFwd2A4MWEwYTYyMTZkMz02NzIzZDdmM2Y0ZmBkPDAxPGQ0N2AyNjI3NTIxMSNxODQyNTc1MTYwPDEjdGxhODZHPUF3QFBdNTc2MDY2KDZHPUF3QFBcNTc2MDY2I3dmdXE4aGx/ZHcoY2p3cGhFaGx/ZHcrcHJnK2BhcCt1aSNmODY8I21haTg1&url="">

Theorem B (groups)

Let G be a group. Let S be a subgroup of G, and let N be a normal subgroup 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