English
Let f : G →* H × I be a monoid homomorphism. If the first projection is surjective and every vertical line intersects the image at most once, then the image is the graph of a monoid homomorphism f' : H →* I.
Русский
Пусть f : G →* H × I — гомоморфизм моноидов. Если проекция на первый фактор сюръективна и образ на каждой «вертикальной линии» пересекается не более чем в один элемент, то образ является графом гомоморфизма f' : H →* I.
LaTeX
$$$\\exists f' : H \\to^* I,\\; \\operatorname{mrange} f = f'.\\mathrm{mgraph}$$$
Lean4
/-- **Vertical line test** for monoid homomorphisms.
Let `f : G → H × I` be a homomorphism to a product of monoids. Assume that `f` is surjective on the
first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at most
once. Then the image of `f` is the graph of some monoid homomorphism `f' : H → I`. -/
@[to_additive /-- **Vertical line test** for monoid homomorphisms.
Let `f : G → H × I` be a homomorphism to a product of monoids. Assume that `f` is surjective on the
first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at most
once. Then the image of `f` is the graph of some monoid homomorphism `f' : H → I`. -/
]
theorem exists_mrange_eq_mgraph {f : G →* H × I} (hf₁ : Surjective (Prod.fst ∘ f))
(hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) : ∃ f' : H →* I, mrange f = f'.mgraph :=
by
obtain ⟨f', hf'⟩ := exists_range_eq_graphOn_univ hf₁ hf
simp only [Set.ext_iff, Set.mem_range, mem_graphOn, mem_univ, true_and, Prod.forall] at hf'
use {
toFun := f'
map_one' := (hf' _ _).1 ⟨1, map_one _⟩
map_mul' := by
simp_rw [hf₁.forall]
rintro g₁ g₂
exact (hf' _ _).1 ⟨g₁ * g₂, by simp [Prod.ext_iff, (hf' (f _).1 _).1 ⟨_, rfl⟩]⟩ }
simpa [SetLike.ext_iff] using hf'
