English
In an adjoint triple F ⊣ G ⊣ H, F is fully faithful if and only if H is fully faithful.
Русский
В троеке смежностей F ⊣ G ⊣ H выполняется: F полнофункторен тогда и только тогда, когда H полнофункторен.
LaTeX
$$$F.FullyFaithful \iff H.FullyFaithful.$$$
Lean4
/-- Given an adjoint triple `F ⊣ G ⊣ H`, the left adjoint `F` is fully faithful if and only if the
right adjoint `H` is fully faithful.
-/
noncomputable def fullyFaithfulEquiv : F.FullyFaithful ≃ H.FullyFaithful
where
toFun
h :=
haveI := h.full
haveI := h.faithful
haveI : IsIso t.adj₂.counit := by
rw [← t.isIso_unit_iff_isIso_counit]
infer_instance
t.adj₂.fullyFaithfulROfIsIsoCounit
invFun
h :=
haveI := h.full
haveI := h.faithful
haveI : IsIso t.adj₁.unit := by
rw [t.isIso_unit_iff_isIso_counit]
infer_instance
t.adj₁.fullyFaithfulLOfIsIsoUnit
left_inv _ := Subsingleton.elim _ _
right_inv _ := Subsingleton.elim _ _
