Theorems · Theorem · group theory

Subgroup.goursat_surjective

∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {I : Subgroup (G × H)}
  (hI₁ : Function.Surjective (Prod.fst ∘ ⇑I.subtype)) (hI₂ : Function.Surjective (Prod.snd ∘ ⇑I.subtype)),
  have this := ⋯;
  have this_1 := ⋯;
  ∃ e,
    (((QuotientGroup.mk' I.goursatFst).prodMap (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph

Goursat's lemma for a subgroup of a product with surjective projections. If I is a subgroup of G × H which projects fully on both factors, then there exist normal subgroups M ≤ G and N ≤ H such that G' × H' ≤ I and the image of I in G ⧸ M × H ⧸ N is the graph of an isomorphism G ⧸ M ≃ H ⧸ N'. G' and H' can be explicitly constructed as I.goursatFst and I.goursatSnd respectively.

Defined in

Mathlib.GroupTheory.Goursat

Cited by

1 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupGroup