English
For a morphism u: b ⟶ a in a bicategory, the following four conditions are equivalent: u is a right adjoint; HasAbsLeftKanLift u (id a); ∃ HasLeftKanLift u (id a); LanLift.CommuteWith u (id a) u.
Русский
Для морфизма u: b ⟶ a в бисистеме четыре условия равны по значению: u — правый сопряжённый; существует абсолютный левый кан-лифтовый подъем along id a; существует левый кан-лифтовый подъем along id a; LanLift.CommuteWith u (id a) u.
LaTeX
$$$\mathrm{IsRightAdjoint}(u) \iff \mathrm{HasAbsLeftKanLift}(u, \mathrm{id}_a) \iff \exists H\, \mathrm{HasLeftKanLift}(u, \mathrm{id}_a) \iff \mathrm{LanLift.CommuteWith}(u, \mathrm{id}_a, u).$$$
Lean4
theorem isRightAdjoint_TFAE (u : b ⟶ a) :
List.TFAE
[IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ _ : HasLeftKanLift u (𝟙 a), LanLift.CommuteWith u (𝟙 a) u] :=
by
tfae_have 1 → 2
| h => IsAbsKan.hasAbsLeftKanLift (Adjunction.ofIsRightAdjoint u).isAbsoluteLeftKanLift
tfae_have 2 → 3
| h => ⟨inferInstance, inferInstance⟩
tfae_have 3 → 1
| ⟨h, h'⟩ => .mk <| (lanLiftIsKan u (𝟙 a)).adjunction <| LanLift.CommuteWith.isKan u (𝟙 a) u
tfae_finish
