English
For a morphism f: a ⟶ b in a bicategory, the following four conditions are equivalent: f is a left adjoint; f has an absolute left Kan extension along id_a; there exists a left Kan extension along id_a; Lan.CommuteWith f (id_a) f.
Русский
Для морфизма f: a ⟶ b в бисистеме четыре условия равны по значению: f — левый сопряжённый; существует абсолютное левое кан-расширение вдоль id_a; существует левое кан-расширение вдоль id_a; Lan.CommuteWith f (id_a) f.
LaTeX
$$$\mathrm{IsLeftAdjoint}(f) \iff \mathrm{HasAbsLeftKanExtension}(f, \mathrm{id}_a) \iff \exists H\,\mathrm{HasLeftKanExtension}(f, \mathrm{id}_a) \iff \mathrm{Lan.CommuteWith}(f, \mathrm{id}_a, f).$$$
Lean4
theorem isLeftAdjoint_TFAE (f : a ⟶ b) :
List.TFAE
[IsLeftAdjoint f, HasAbsLeftKanExtension f (𝟙 a), ∃ _ : HasLeftKanExtension f (𝟙 a), Lan.CommuteWith f (𝟙 a) f] :=
by
tfae_have 1 → 2
| h => IsAbsKan.hasAbsLeftKanExtension (Adjunction.ofIsLeftAdjoint f).isAbsoluteLeftKan
tfae_have 2 → 3
| h => ⟨inferInstance, inferInstance⟩
tfae_have 3 → 1
| ⟨h, h'⟩ => .mk <| (lanIsKan f (𝟙 a)).adjunction <| Lan.CommuteWith.isKan f (𝟙 a) f
tfae_finish
