English
If a map f : G →* H × I satisfies surjectivity on both factors and the line condition, 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 monoid isomorphisms.
Let `f : G → H × I` be a homomorphism to a product of monoids. 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 monoid
isomorphism `f' : H ≃ I`. -/
@[to_additive /-- **Line test** for monoid isomorphisms.
Let `f : G → H × I` be a homomorphism to a product of monoids. 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
monoid isomorphism `f' : H ≃ I`. -/
]
theorem exists_mulEquiv_mrange_eq_mgraph {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, mrange f = e.toMonoidHom.mgraph :=
by
obtain ⟨e₁, he₁⟩ := f.exists_mrange_eq_mgraph hf₁ fun _ _ ↦ (hf _ _).1
obtain ⟨e₂, he₂⟩ := (MulEquiv.prodComm.toMonoidHom.comp f).exists_mrange_eq_mgraph (by simpa) <| by simp [hf]
have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
rw [SetLike.ext_iff] at he₁ he₂
aesop (add simp [Prod.swap_eq_iff_eq_swap])
exact
⟨{ toFun := e₁
map_mul' := e₁.map_mul'
invFun := e₂
left_inv := fun h ↦ by rw [← he₁₂]
right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩
