tensor_actionHomRight — Mathlib

English

For x,y in C and z in D, the action by the tensor product x ⊗ y on a morphism f: z ⟶ z' is given by the associator and the actions on f: actionHomRight (x ⊗ y) f = α_hom ≫ (x ⊴ y) ⊴ f ≫ α_inv.

Русский

Действие тензора x ⊗ y на морфизм f: z ⟶ z' задаётся через ассоциатор и действия: actionHomRight (x ⊗ y) f = α_hom ≫ x ⊴ y ⊴ f ≫ α_inv.

LaTeX

$$$\\forall x,y:\\, C,\\; \\forall f:\\; \\mathrm{Hom}(z,z'),\\; \\; (x \\otimes y) ⊴ₗ f = (\\alpha_{\\ell} x y z).\\text{hom} \\; \\; ≫ (x ⊴ₗ y) ⊴ₗ f \\; ≫ (\\alpha_{\\ell} x y z').\\text{inv}$$$

Lean4

@[reassoc, simp]
theorem tensor_actionHomRight (x y : C) {z z' : D} (f : z ⟶ z') :
    (x ⊗ y) ⊴ₗ f = (αₗ x y z).hom ≫ x ⊴ₗ y ⊴ₗ f ≫ (αₗ x y z').inv :=
  by
  simp only [← id_actionHom]
  rw [← Category.assoc, ← actionAssocIso_hom_naturality]
  simp

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