Goursat's lemma for subgroups

This file 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'.

G' and H' can be explicitly constructed as Subgroup.goursatFst I and Subgroup.goursatSnd I respectively.

def Subgroup.goursatFst {G : Type u_1} {H : Type u_2} [Group G] [Group H] (I : Subgroup (G × H)) : Subgroup G

For I a subgroup of G × H, I.goursatFst is the kernel of the projection map I → H, considered as a subgroup of G.

This is the first subgroup appearing in Goursat's lemma. See Subgroup.goursat.

def AddSubgroup.goursatFst {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (I : AddSubgroup (G × H)) : AddSubgroup G

For I a subgroup of G × H, I.goursatFst is the kernel of the projection map I → H, considered as a subgroup of G.

This is the first subgroup appearing in Goursat's lemma. See AddSubgroup.goursat.

def Subgroup.goursatSnd {G : Type u_1} {H : Type u_2} [Group G] [Group H] (I : Subgroup (G × H)) : Subgroup H

For I a subgroup of G × H, I.goursatSnd is the kernel of the projection map I → G, considered as a subgroup of H.

This is the second subgroup appearing in Goursat's lemma. See Subgroup.goursat.

def AddSubgroup.goursatSnd {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (I : AddSubgroup (G × H)) : AddSubgroup H

For I a subgroup of G × H, I.goursatSnd is the kernel of the projection map I → G, considered as a subgroup of H.

This is the second subgroup appearing in Goursat's lemma. See AddSubgroup.goursat.

@[simp]

theorem Subgroup.mem_goursatFst {G : Type u_1} {H : Type u_2} [Group G] [Group H] {I : Subgroup (G × H)} {g : G} : g ∈ I.goursatFst ↔ (g, 1) ∈ I

@[simp]

theorem AddSubgroup.mem_goursatFst {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {I : AddSubgroup (G × H)} {g : G} : g ∈ I.goursatFst ↔ (g, 0) ∈ I

@[simp]

theorem Subgroup.mem_goursatSnd {G : Type u_1} {H : Type u_2} [Group G] [Group H] {I : Subgroup (G × H)} {h : H} : h ∈ I.goursatSnd ↔ (1, h) ∈ I

@[simp]

theorem AddSubgroup.mem_goursatSnd {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {I : AddSubgroup (G × H)} {h : H} : h ∈ I.goursatSnd ↔ (0, h) ∈ I

theorem Subgroup.normal_goursatFst {G : Type u_1} {H : Type u_2} [Group G] [Group H] {I : Subgroup (G × H)} (hI₁ : Function.Surjective (Prod.fst ∘ ⇑I.subtype)) : I.goursatFst.Normal

theorem AddSubgroup.normal_goursatFst {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {I : AddSubgroup (G × H)} (hI₁ : Function.Surjective (Prod.fst ∘ ⇑I.subtype)) : I.goursatFst.Normal

theorem Subgroup.normal_goursatSnd {G : Type u_1} {H : Type u_2} [Group G] [Group H] {I : Subgroup (G × H)} (hI₂ : Function.Surjective (Prod.snd ∘ ⇑I.subtype)) : I.goursatSnd.Normal

theorem AddSubgroup.normal_goursatSnd {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {I : AddSubgroup (G × H)} (hI₂ : Function.Surjective (Prod.snd ∘ ⇑I.subtype)) : I.goursatSnd.Normal

theorem Subgroup.mk_goursatFst_eq_iff_mk_goursatSnd_eq {G : Type u_1} {H : Type u_2} [Group G] [Group H] {I : Subgroup (G × H)} (hI₁ : Function.Surjective (Prod.fst ∘ ⇑I.subtype)) (hI₂ : Function.Surjective (Prod.snd ∘ ⇑I.subtype)) {x y : G × H} (hx : x ∈ I) (hy : y ∈ I) : ↑x.1 = ↑y.1 ↔ ↑x.2 = ↑y.2

theorem AddSubgroup.mk_goursatFst_eq_iff_mk_goursatSnd_eq {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {I : AddSubgroup (G × H)} (hI₁ : Function.Surjective (Prod.fst ∘ ⇑I.subtype)) (hI₂ : Function.Surjective (Prod.snd ∘ ⇑I.subtype)) {x y : G × H} (hx : x ∈ I) (hy : y ∈ I) : ↑x.1 = ↑y.1 ↔ ↑x.2 = ↑y.2

theorem Subgroup.goursatFst_prod_goursatSnd_le {G : Type u_1} {H : Type u_2} [Group G] [Group H] (I : Subgroup (G × H)) : I.goursatFst.prod I.goursatSnd ≤ I

theorem AddSubgroup.goursatFst_prod_goursatSnd_le {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (I : AddSubgroup (G × H)) : I.goursatFst.prod I.goursatSnd ≤ I

theorem Subgroup.goursat_surjective {G : Type u_1} {H : Type u_2} [Group G] [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 : G ⧸ I.goursatFst ≃* H ⧸ I.goursatSnd), (((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.

theorem AddSubgroup.goursat_surjective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {I : AddSubgroup (G × H)} (hI₁ : Function.Surjective (Prod.fst ∘ ⇑I.subtype)) (hI₂ : Function.Surjective (Prod.snd ∘ ⇑I.subtype)) : have this := ⋯; have this_1 := ⋯; ∃ (e : G ⧸ I.goursatFst ≃+ H ⧸ I.goursatSnd), (((QuotientAddGroup.mk' I.goursatFst).prodMap (QuotientAddGroup.mk' I.goursatSnd)).comp I.subtype).range = e.toAddMonoidHom.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.

theorem Subgroup.goursat {G : Type u_1} {H : Type u_2} [Group G] [Group H] {I : Subgroup (G × H)} : ∃ (G' : Subgroup G) (H' : Subgroup H) (M : Subgroup ↥G') (N : Subgroup ↥H') (x : M.Normal) (x_1 : N.Normal) (e : ↥G' ⧸ M ≃* ↥H' ⧸ N), I = map (G'.subtype.prodMap H'.subtype) (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)

Goursat's lemma for an arbitrary subgroup.

If I is a subgroup of G × H, then there exist subgroups G' ≤ G, H' ≤ H and normal subgroups M ⊴ G' and N ⊴ H' such that M × N ≤ I and the image of I in G' ⧸ M × H' ⧸ N is the graph of an isomorphism G' ⧸ M ≃ H' ⧸ N.

theorem AddSubgroup.goursat {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {I : AddSubgroup (G × H)} : ∃ (G' : AddSubgroup G) (H' : AddSubgroup H) (M : AddSubgroup ↥G') (N : AddSubgroup ↥H') (x : M.Normal) (x_1 : N.Normal) (e : ↥G' ⧸ M ≃+ ↥H' ⧸ N), I = map (G'.subtype.prodMap H'.subtype) (comap ((QuotientAddGroup.mk' M).prodMap (QuotientAddGroup.mk' N)) e.toAddMonoidHom.graph)

Goursat's lemma for an arbitrary subgroup.

If I is a subgroup of G × H, then there exist subgroups G' ≤ G, H' ≤ H and normal subgroups M ≤ G' and N ≤ H' such that M × N ≤ I and the image of I in G' ⧸ M × H' ⧸ N is the graph of an isomorphism G ⧸ G' ≃ H ⧸ H'.