English
Another naturality statement for the symmetrized left adjoint mate; the second naturality follows from the first via functoriality of the tensor product.
Русский
Ещё одно свойство естественности для симметричной левой сопряженной пары; второе естественно от первого через функториальность тензора.
LaTeX
$$$$ (\\text{equiv})^{symm}_n = \\dots $$$$
Lean4
/-- Given an exact pairing on `Y Y'`,
we get a bijection on hom-sets `(X ⊗ Y ⟶ Z) ≃ (X ⟶ Z ⊗ Y')`
by "pulling the string on the right" up or down.
-/
def tensorRightHomEquiv (X Y Y' Z : C) [ExactPairing Y Y'] : (X ⊗ Y ⟶ Z) ≃ (X ⟶ Z ⊗ Y')
where
toFun f := (ρ_ _).inv ≫ _ ◁ η_ _ _ ≫ (α_ _ _ _).inv ≫ f ▷ _
invFun f := f ▷ _ ≫ (α_ _ _ _).hom ≫ _ ◁ ε_ _ _ ≫ (ρ_ _).hom
left_inv
f := by
calc
_ = 𝟙 _ ⊗≫ X ◁ η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 _ := by monoidal
_ = 𝟙 _ ⊗≫ X ◁ (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ⊗≫ f := by rw [← whisker_exchange]; monoidal
_ = f := by rw [evaluation_coevaluation'']; monoidal
right_inv
f := by
calc
_ = 𝟙 _ ⊗≫ (X ◁ η_ Y Y' ≫ f ▷ (Y ⊗ Y')) ⊗≫ Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 _ := by monoidal
_ = f ⊗≫ Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ 𝟙 _ := by rw [whisker_exchange]; monoidal
_ = f := by rw [coevaluation_evaluation'']; monoidal
