tensorRightHomEquiv_whiskerRight_comp_evaluation

English

For X has right dual structure, the right-hom equivalence interacts with whiskering on the left and evaluation to yield a standard evaluation–whisker identity.

Русский

Для X с правым дуальным строением эквивалентность правого гомоморфизма взаимодействует с левым перетасовкой и оценкой, образуя стандартное тождество оценки и перетасовки.

LaTeX

$$$(\\mathrm{tensorRightHomEquiv}\\,(X',X)\\;Y\\;Y')(f)^{\\!-1} (f \\circ g) = g \\circ (\\mathrm{Exac tPairing}.evaluation)$$$

Lean4

@[simp]
theorem tensorRightHomEquiv_whiskerRight_comp_evaluation {X Y : C} [HasRightDual X] (f : Y ⟶ Xᘁ) :
    (tensorRightHomEquiv _ _ _ _) (f ▷ X ≫ ε_ X (Xᘁ)) = f ≫ (λ_ _).inv :=
  calc
    _ = 𝟙 _ ⊗≫ (Y ◁ η_ X Xᘁ ≫ f ▷ (X ⊗ Xᘁ)) ⊗≫ ε_ X Xᘁ ▷ Xᘁ := by dsimp [tensorRightHomEquiv]; monoidal
    _ = f ⊗≫ (Xᘁ ◁ η_ X Xᘁ ⊗≫ ε_ X Xᘁ ▷ Xᘁ) := by rw [whisker_exchange]; monoidal
    _ = _ := by rw [coevaluation_evaluation''];
      monoidal
        -- Next four lemmas passing `fᘁ` or `ᘁf` through (co)evaluations.

Похожие утверждения