English
If a submonoid G ⊆ H × I projects bijectively to both factors, then G is the graph of a monoid isomorphism e : H ≃* I.
Русский
Если подмножество G ⊆ H × I проецируется биективно на оба фактора, то G есть граф мономорфизма-изоморфизма e : 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_mgraph {G : Submonoid (H × I)} (hG₁ : Bijective (Prod.fst ∘ G.subtype))
(hG₂ : Bijective (Prod.snd ∘ G.subtype)) : ∃ e : H ≃* I, G = e.toMonoidHom.mgraph := by
simpa using
MonoidHom.exists_mulEquiv_mrange_eq_mgraph hG₁.surjective hG₂.surjective fun _ _ ↦
hG₁.injective.eq_iff.trans hG₂.injective.eq_iff.symm
