English
There is a canonical bijection between morphisms g ⟶ l ≫ h and r ≫ g ⟶ h given an adjunction l ⊣ r.
Русский
Существует каноническое биективное соответствие между морфизмами g → l ≫ h и r ≫ g → h при данном adjunction l ⊣ r.
LaTeX
$$$\\mathrm{homEquiv}_1 : (g \\to l \\gg h) \\cong (r \\gg g \\to h)$$$
Lean4
/-- The bijection `(g ⟶ l ≫ h) ≃ (r ≫ g ⟶ h)` induced by an adjunction
`l ⊣ r` in a bicategory. -/
@[simps -isSimp]
def homEquiv₁ {g : b ⟶ d} {h : c ⟶ d} : (g ⟶ l ≫ h) ≃ (r ≫ g ⟶ h)
where
toFun γ := r ◁ γ ≫ (α_ _ _ _).inv ≫ adj.counit ▷ h ≫ (λ_ _).hom
invFun β := (λ_ _).inv ≫ adj.unit ▷ _ ≫ (α_ _ _ _).hom ≫ l ◁ β
left_inv
γ :=
calc
_ = 𝟙 _ ⊗≫ (adj.unit ▷ g ≫ (l ≫ r) ◁ γ) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 _ := by bicategory
_ = γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 _ :=
by
rw [← whisker_exchange]
bicategory
_ = γ := by
rw [adj.left_triangle]
bicategory
right_inv
β := by
calc
_ = 𝟙 _ ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 _ := by bicategory
_ = 𝟙 _ ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β :=
by
rw [whisker_exchange]
bicategory
_ = β := by
rw [adj.right_triangle]
bicategory
