one_smul — Mathlib

English

The unit of the monoidal action acts trivially: the unit action composed with the left unitor equals the unit isomorphism.

Русский

Единичное действие моноидального действия действует тривиально: композиция единичного действия с левой униторой равна единичному однообразному гомомору.

LaTeX

$$$\\eta \\;\u22a5_\\ell X \\;\\circ\\; γ = (\\lambda_\\ell[C] X).hom$$$

Lean4

@[reassoc (attr := simp)]
theorem one_smul (X : D) [ModObj M X] : η ⊵ₗ X ≫ γ[M,X] = (λₗ[C] X).hom :=
  ModObj.one_smul' X

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