English
If G ≤ H × I is a submonoid and the map G → H × I is bijective onto the first coordinate, then G is the graph of some monoid hom f : H →* I.
Русский
Если G ⊆ H × I — подмножество мономоидов и отображение G → H даёт биjektивную проекцию на первый координат, то G есть граф гомоморфизма f : H →* I.
LaTeX
$$$\\exists f : H \\to^* I,\\; G = f.mgraph$$$
Lean4
/-- **Vertical line test** for group homomorphisms.
Let `G ≤ H × I` be a subgroup of a product of monoids. Assume that `G` maps bijectively to the
first factor. Then `G` is the graph of some monoid homomorphism `f : H → I`. -/
@[to_additive /-- **Vertical line test** for additive monoid homomorphisms.
Let `G ≤ H × I` be a submonoid of a product of monoids. Assume that `G` surjects onto the first
factor and `G` intersects every "vertical line" `{(h, i) | i : I}` at most once. Then `G` is the
graph of some monoid homomorphism `f : H → I`. -/
]
theorem exists_eq_graph {G : Subgroup (H × I)} (hG₁ : Bijective (Prod.fst ∘ G.subtype)) : ∃ f : H →* I, G = f.graph :=
by simpa [SetLike.ext_iff] using Submonoid.exists_eq_mgraph hG₁
