English
A relation is an isomorphism in RelCat if and only if it is the graph of an isomorphism in Type u. In particular, isomorphisms in RelCat arise exactly from graphs of isomorphisms of underlying types.
Русский
Отношение является изоморфизмом в RelCat тогда и только тогда, когда оно является графом изоморфизма между типами. Изоморфии в RelCat соответствуют графам изоморфизмов над типами.
LaTeX
$$$ \\forall X,Y,\\ r: X \\to Y,\\ IsIso(r) \\iff \\exists f: Iso(X,Y)\\text{ in Type }u,\\ \\mathrm{graph}(f.hom) = r. $$$
Lean4
/-- A relation is an isomorphism in `RelCat` iff it is the image of an isomorphism in
`Type u`. -/
theorem rel_iso_iff {X Y : RelCat} (r : X ⟶ Y) :
IsIso (C := RelCat) r ↔ ∃ f : Iso (C := Type u) X Y, graphFunctor.map f.hom = r :=
by
constructor
· intro h
have h1 := congr_fun₂ congr((· ~[($h.hom_inv_id).rel] ·))
have h2 := congr_fun₂ congr((· ~[($h.inv_hom_id).rel] ·))
simp only [RelCat.Hom.rel_comp_apply₂, RelCat.Hom.rel_id_apply₂, eq_iff_iff] at h1 h2
obtain ⟨f, hf⟩ := Classical.axiomOfChoice (fun a => (h1 a a).mpr rfl)
obtain ⟨g, hg⟩ := Classical.axiomOfChoice (fun a => (h2 a a).mpr rfl)
suffices hif : IsIso (C := Type u) f by
use asIso f
ext ⟨x, y⟩
exact ⟨by aesop, fun hxy ↦ (h2 (f x) y).1 ⟨x, (hf x).2, hxy⟩⟩
use g
constructor
· ext x
apply (h1 _ _).mp
use f x, (hg _).2, (hf _).2
· ext y
apply (h2 _ _).mp
use g y, (hf (g y)).2, (hg y).2
· rintro ⟨f, rfl⟩
apply graphFunctor.map_isIso
