Commit 2024-11-28 16:12 e71723be
View on Github →feat: Goursat's lemma for subgroups (#18823)
Proves Goursat's lemma for subgroups.
If I
is a subgroup of G × H
which projects fully on both factors, then there exist normal
subgroups G' ≤ G
and H' ≤ H
such that G' × H' ≤ I
and the image of I
in G ⧸ G' × H ⧸ H'
is the graph of an
isomorphism G ⧸ G' ≃ H ⧸ H'
.
We construct G'
and H'
as explicit subgroups.