English
Naturality of the inverse of the left-tensor hom-equivalence with respect to precomposition: composing on the left corresponds to composing under the inverse equivalence on the left side.
Русский
Естественность обратной левой эквивалентности гомов по отношению к предсоставлению слева: композиция слева соответствует композиции под обратной эквивалентностью слева.
LaTeX
$$$$ (\\tensorLeftHomEquiv X Y Y' Z)^{−1} (f \\circ g) = (\\text{_ } \\ ) ◁ f \\circ (\\tensorLeftHomEquiv X' Y Y' Z)^{−1} g $$$$
Lean4
/-- The composition of left adjoint mates is the adjoint mate of the composition. -/
@[reassoc]
theorem comp_leftAdjointMate {X Y Z : C} [HasLeftDual X] [HasLeftDual Y] [HasLeftDual Z] {f : X ⟶ Y} {g : Y ⟶ Z} :
(ᘁf ≫ g) = (ᘁg) ≫ ᘁf := by
rw [leftAdjointMate_comp]
simp only [leftAdjointMate, MonoidalCategory.whiskerLeft_comp]
simp only [← Category.assoc]; congr 3; simp only [Category.assoc]
simp only [← comp_whiskerRight]; congr 2
symm
calc
_ =
𝟙 _ ⊗≫
((𝟙_ C) ◁ η_ (ᘁY) Y ≫ η_ (ᘁX) X ▷ ((ᘁY) ⊗ Y)) ⊗≫ (ᘁX) ◁ f ▷ (ᘁY) ▷ Y ⊗≫ (ᘁX) ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ (ᘁX) ◁ g :=
by rw [tensorHom_def]; monoidal
_ = η_ (ᘁX) X ⊗≫ (((ᘁX) ⊗ X) ◁ η_ (ᘁY) Y ≫ ((ᘁX) ◁ f) ▷ ((ᘁY) ⊗ Y)) ⊗≫ (ᘁX) ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ (ᘁX) ◁ g := by
rw [whisker_exchange]; monoidal
_ = η_ (ᘁX) X ⊗≫ ((ᘁX) ◁ f) ⊗≫ (ᘁX) ◁ (Y ◁ η_ (ᘁY) Y ⊗≫ ε_ (ᘁY) Y ▷ Y) ⊗≫ (ᘁX) ◁ g := by rw [whisker_exchange];
monoidal
_ = η_ (ᘁX) X ≫ (ᘁX) ◁ f ≫ (ᘁX) ◁ g := by rw [coevaluation_evaluation'']; monoidal
