one_rightUnitor — Mathlib

English

For a monoid object M, the left unitor with tensor unit interacts with η[M] to give the unit, i.e., ((λ_{1_C}).inv ≫ (η[M] ⊗ 𝟙_{1_C})) ≫ (λ_{M}).hom = η.

Русский

Для моноидального объекта M левый унитор с единичным объектом взаимодействует с η[M], давая единицу: ((λ_{1_C}).inv ≫ (η[M] ⊗ 𝟙_{1_C})) ≫ (λ_{M}).hom = η.

LaTeX

$$$ ((\lambda_{ \mathbf{1} } )^{-1} \circ (η[M] \otimes 𝟙_{ \mathbf{1} })) \circ (λ_M)^{hom} = η $$$

Lean4

theorem one_rightUnitor {M : C} [MonObj M] : ((λ_ (𝟙_ C)).inv ≫ (η[M] ⊗ₘ 𝟙 (𝟙_ C))) ≫ (ρ_ M).hom = η := by
  simp [← unitors_equal]

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