English
Given surjectivity of the projections, there exists an isomorphism e between the quotients G / I.goursatFst and H / I.goursatSnd whose range is the graph of e.
Русский
При заданной сюръективности проекций существует изоморфизм e между частями G / I.goursatFst и H / I.goursatSnd, граф которого описывает образ I.
LaTeX
$$$ \\exists e : (G / I.goursatFst) \\to_* (H / I.goursatSnd),\\; (((QuotientGroup.mk' _).prodMap (QuotientGroup.mk' _)).comp I.subtype).range = e.toMonoidHom.graph $$$
Lean4
/-- **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. -/
@[to_additive /-- **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 goursat_surjective :
have := normal_goursatFst hI₁
have := normal_goursatSnd hI₂
∃ e : G ⧸ I.goursatFst ≃* H ⧸ I.goursatSnd,
(((QuotientGroup.mk' _).prodMap (QuotientGroup.mk' _)).comp I.subtype).range = e.toMonoidHom.graph :=
by
have := normal_goursatFst hI₁
have := normal_goursatSnd hI₂
exact
(((QuotientGroup.mk' I.goursatFst).prodMap (QuotientGroup.mk' I.goursatSnd)).comp
I.subtype).exists_mulEquiv_range_eq_graph
((QuotientGroup.mk'_surjective _).comp hI₁) ((QuotientGroup.mk'_surjective _).comp hI₂) fun ⟨x, hx⟩ ⟨y, hy⟩ ↦
mk_goursatFst_eq_iff_mk_goursatSnd_eq hI₁ hI₂ hx hy
