tensorRightHomEquiv_naturality — Mathlib

English

A second naturality property for tensorRightHomEquiv; the map respects composition with the right-hand morphism g.

Русский

Вторая естественность для tensorRightHomEquiv: сохраняет композицию справа с g.

LaTeX

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

Lean4

theorem tensorRightHomEquiv_naturality {X Y Y' Z Z' : C} [ExactPairing Y Y'] (f : X ⊗ Y ⟶ Z) (g : Z ⟶ Z') :
    (tensorRightHomEquiv X Y Y' Z') (f ≫ g) = (tensorRightHomEquiv X Y Y' Z) f ≫ g ▷ Y' := by simp [tensorRightHomEquiv]

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