English
If G ≤ H × I is a submonoid and the natural maps to both factors are bijective, then G is the graph of an isomorphism f : H ≃* I.
Русский
Если G ≤ H × I — подмонод, и естественные отображения в оба фактора являются биективными, то G является графом изоморфизма f : H ≃* I.
LaTeX
$$$\\exists e : H \\simeq^* I,\\; G = e.toMonoidHom.mgraph$$$
Lean4
/-- **Goursat's lemma** for monoid isomorphisms.
Let `G ≤ H × I` be a submonoid of a product of monoids. Assume that the natural maps from `G` to
both factors are bijective. Then `G` is the graph of some isomorphism `f : H ≃* I`. -/
@[to_additive /-- **Goursat's lemma** for additive monoid isomorphisms.
Let `G ≤ H × I` be a submonoid of a product of additive monoids. Assume that the natural maps from
`G` to both factors are bijective. Then `G` is the graph of some isomorphism `f : H ≃+ I`. -/
]
theorem exists_mulEquiv_eq_graph {G : Subgroup (H × I)} (hG₁ : Bijective (Prod.fst ∘ G.subtype))
(hG₂ : Bijective (Prod.snd ∘ G.subtype)) : ∃ e : H ≃* I, G = e.toMonoidHom.graph := by
simpa [SetLike.ext_iff] using Submonoid.exists_mulEquiv_eq_mgraph hG₁ hG₂
