tensorLeftHomEquiv_symm_naturality

English

Naturality of the inverse right-hom equivalence under left whiskering; symmetry with respect to precomposition by f.

Русский

Естественность обратной правой эквивалентности: симметрия по префиксному состояению f.

LaTeX

$$$$ (tensorRightHomEquiv X Y Y' Z)^{−1}(f \\circ g) = f \\circ (tensorRightHomEquiv X Y Y' Z)^{−1} g $$$$

Lean4

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

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