braiding_naturality_left — Mathlib

English

For morphism f: X → Y and Z in ModuleCat R, the left whiskering with Z commutes with the braiding: f ▷ Z ≫ braiding YZ.hom = braiding XZ.hom ≫ Z ▷ f.

Русский

Для отображения f: X → Y и Z выполняется равенство тождественных диагоналей слева по отношению к braiding: f ▷ Z ≫ braiding.hom = braiding.hom ≫ Z ◁ f.

LaTeX

$$$f \\;▷\\; Z \\;\\;\\;\\; \\;= \\; (\\text{braiding}_{X,Z}).\\mathrm{hom} \\; \\circ Z ◁ f$$$

Lean4

@[simp]
theorem braiding_naturality_left {X Y : ModuleCat R} (f : X ⟶ Y) (Z : ModuleCat R) :
    f ▷ Z ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ Z ◁ f :=
  by
  simp_rw [← id_tensorHom]
  apply braiding_naturality

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