English
The naturality of the left-tensor hom-equivalence with respect to postcomposition: composing with g on the right corresponds to applying the equivalence to f and then whiskering by g.
Русский
Естественность левой эквивалентности гомов по отношению к постсоставлению: композиция с g справа соответствует применению эквивалентности к f и последующей операцией с g.
LaTeX
$$$$ (tensorLeftHomEquiv X Y Y' Z) (f \\circ g) = (tensorLeftHomEquiv X Y Y' Z) f \\circ (Y \\triangleleft g) $$$$
Lean4
/-- The composition of right adjoint mates is the adjoint mate of the composition. -/
@[reassoc]
theorem comp_rightAdjointMate {X Y Z : C} [HasRightDual X] [HasRightDual Y] [HasRightDual Z] {f : X ⟶ Y} {g : Y ⟶ Z} :
(f ≫ g)ᘁ = gᘁ ≫ fᘁ := by
rw [rightAdjointMate_comp]
simp only [rightAdjointMate, comp_whiskerRight]
simp only [← Category.assoc]; congr 3; simp only [Category.assoc]
simp only [← MonoidalCategory.whiskerLeft_comp]; congr 2
symm
calc
_ = 𝟙 _ ⊗≫ (η_ Y Yᘁ ▷ 𝟙_ C ≫ (Y ⊗ Yᘁ) ◁ η_ X Xᘁ) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 _ := by
rw [tensorHom_def']; monoidal
_ = η_ X Xᘁ ⊗≫ (η_ Y Yᘁ ▷ (X ⊗ Xᘁ) ≫ (Y ⊗ Yᘁ) ◁ f ▷ Xᘁ) ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 _ := by
rw [← whisker_exchange]; monoidal
_ = η_ X Xᘁ ⊗≫ f ▷ Xᘁ ⊗≫ (η_ Y Yᘁ ▷ Y ⊗≫ Y ◁ ε_ Y Yᘁ) ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 _ := by rw [← whisker_exchange]; monoidal
_ = η_ X Xᘁ ≫ f ▷ Xᘁ ≫ g ▷ Xᘁ := by rw [evaluation_coevaluation'']; monoidal
