Mon_tensor_one_mul — Mathlib

English

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

Русский

Для моноидального объекта M правый унитор с единичным объектом взаимодействует с η[M], давая η.

LaTeX

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

Lean4

theorem Mon_tensor_one_mul (M N : C) [MonObj M] [MonObj N] :
    (((λ_ (𝟙_ C)).inv ≫ (η[M] ⊗ₘ η[N])) ▷ (M ⊗ N)) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) = (λ_ (M ⊗ N)).hom :=
  by
  simp only [comp_whiskerRight_assoc]
  slice_lhs 2 3 => rw [tensorμ_natural_left]
  slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, one_mul, one_mul]
  symm
  exact tensor_left_unitality M N

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