English
Let G ⊆ H × I be a submonoid whose projection to H is bijective. Then G is the graph of a monoid hom f : H →* I.
Русский
Пусть G ⊆ H × I — подмножество моноидов, проекция на H — биекция. Тогда G — граф гомоморфизма f : H →* I.
LaTeX
$$$\\exists f : H \\to^* I,\, G = f.mgraph$$$
Lean4
/-- **Vertical line test** for monoid homomorphisms.
Let `G ≤ H × I` be a submonoid 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_mgraph {G : Submonoid (H × I)} (hG₁ : Bijective (Prod.fst ∘ G.subtype)) :
∃ f : H →* I, G = f.mgraph := by
simpa using
MonoidHom.exists_mrange_eq_mgraph hG₁.surjective fun a b h ↦ congr_arg (Prod.snd ∘ G.subtype) (hG₁.injective h)
