tensorLeftHomEquiv_naturality — Mathlib

English

Naturality of tensorRightHomEquiv with respect to postcomposition on the right: composing f with g corresponds to applying the equivalence to f and then whiskering by g.

Русский

Естественность для правого гом-эквивалента относительно постсоставления справа: композиция с g равна применению эквивалентности к f и затем whisker по g.

LaTeX

$$$$ (tensorRightHomEquiv X Y Y' Z')(f) \\circ g = (tensorRightHomEquiv X Y Y' Z) f \\circ (g \\triangleleft Y') $$$$

Lean4

theorem tensorLeftHomEquiv_naturality {X Y Y' Z Z' : C} [ExactPairing Y Y'] (f : Y' ⊗ X ⟶ Z) (g : Z ⟶ Z') :
    (tensorLeftHomEquiv X Y Y' Z') (f ≫ g) = (tensorLeftHomEquiv X Y Y' Z) f ≫ Y ◁ g := by simp [tensorLeftHomEquiv]

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