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