English
If there is a pair of surjections onto β and γ and a compatibility condition, then there exists an equivalence e : β ≃ γ with range f = graphOn e over the universe.
Русский
При наличии сюръекции на β и γ и совместимости, существует эквивалентность e: β ≃ γ такая, что range f = graphOn e на вселенной.
LaTeX
$$$\exists e : β \simeq γ, \operatorname{range}(f) = \operatorname{graphOn}(e, \mathsf{univ})$$$
Lean4
/-- **Line test** for equivalences.
Let `f : α → β × γ` 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" `{(b, c) | c : γ}` and every
"horizontal line" `{(b, c) | b : β}` at most once. Then the image of `f` is the graph of some
equivalence `f' : β ≃ γ`. -/
theorem exists_equiv_range_eq_graphOn_univ {f : α → β × γ} (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 : β ≃ γ, range f = univ.graphOn e :=
by
obtain ⟨e₁, he₁⟩ := exists_range_eq_graphOn_univ hf₁ fun _ _ ↦ (hf _ _).1
obtain ⟨e₂, he₂⟩ := exists_range_eq_graphOn_univ (f := Equiv.prodComm _ _ ∘ f) (by simpa) <| by simp [hf]
have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
rw [Set.ext_iff] at he₁ he₂
aesop (add simp [Prod.swap_eq_iff_eq_swap])
exact
⟨{ toFun := e₁
invFun := e₂
left_inv := fun h ↦ by rw [← he₁₂]
right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩
