English
Line-test statement for monoid isomorphisms: If the image of f : G →* H × I is surjective on both coordinates and hits each vertical/horizontal line at most once, then the image is the graph of a monoid isomorphism e : H ≃* I.
Русский
Линейный тест графа для изоморфизмов: если образ f : G →* H × I сюръективен по обеим координатам и встречает каждую вертикальную и горизонтальную линию не более чем один раз, то образ есть граф изоморфизма e : H ≃* I.
LaTeX
$$$\\exists e : H \\simeq^* I,\\; \\operatorname{mrange} f = e.toMonoidHom.mgraph$$$
Lean4
/-- **Line test** for group isomorphisms.
Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on both
factors and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` and every
"horizontal line" `{(h, i) | h : H}` at most once. Then the image of `f` is the graph of some group
isomorphism `f' : H ≃ I`. -/
@[to_additive /-- **Line test** for monoid isomorphisms.
Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on both
factors and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` and every
"horizontal line" `{(h, i) | h : H}` at most once. Then the image of `f` is the graph of some
group isomorphism `f' : H ≃ I`. -/
]
theorem exists_mulEquiv_range_eq_graph {f : G →* H × I} (hf₁ : Surjective (Prod.fst ∘ f))
(hf₂ : Surjective (Prod.snd ∘ f)) (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) :
∃ e : H ≃* I, range f = e.toMonoidHom.graph := by
simpa [SetLike.ext_iff] using exists_mulEquiv_mrange_eq_mgraph hf₁ hf₂ hf
