English
Coherence of inserting unit via η and the associator when considering multiple tensorings with the unit object; this expresses equality of two complex composites involving λ, η, and α.
Русский
Согласованность вставки единицы через η и ассоциатор при рассмотрении нескольких тензорований с единичным объектом; выражает равенство двух сложных композиции, содержащих λ, η и α.
LaTeX
$$$$ ((\lambda_{(\mathbf{1})})^{-1} \circ ((λ_{(\mathbf{1})})^{-1} \circ (η[M] \otimes η[N]) \otimes η[P])) \circ (α_{M N P})^{hom} = (λ_{(\mathbf{1})})^{-1} \circ (η[M] ⊗ ( (λ_{(\mathbf{1})})^{-1} \circ (η[N] ⊗ η[P])) ) $$$$
Lean4
theorem one_associator {M N P : C} [MonObj M] [MonObj N] [MonObj P] :
((λ_ (𝟙_ C)).inv ≫ ((λ_ (𝟙_ C)).inv ≫ (η[M] ⊗ₘ η[N]) ⊗ₘ η[P])) ≫ (α_ M N P).hom =
(λ_ (𝟙_ C)).inv ≫ (η[M] ⊗ₘ (λ_ (𝟙_ C)).inv ≫ (η[N] ⊗ₘ η[P])) :=
by
simp only [Category.assoc, Iso.cancel_iso_inv_left]
slice_lhs 1 3 => rw [← Category.id_comp (η : 𝟙_ C ⟶ P), ← tensorHom_comp_tensorHom]
slice_lhs 2 3 => rw [associator_naturality]
slice_rhs 1 2 => rw [← Category.id_comp η, ← tensorHom_comp_tensorHom]
slice_lhs 1 2 => rw [tensorHom_id, ← leftUnitor_tensor_inv]
rw [← cancel_epi (λ_ (𝟙_ C)).inv]
slice_lhs 1 2 => rw [leftUnitor_inv_naturality]
simp
