English
The triangle identity holds in the localized monoidal category: the associator and unit constraints satisfy the standard coherence triangle.
Русский
Треугольная когерентность выполняется в локализованной монойдальной категории: ассоциатор и ограничения единицы удовлетворяют стандартному коэрентному треугольнику.
LaTeX
$$$(\alpha_X(\mathbf{1})Y)^{\mathrm{hom}} \;\circ\; X \triangleleft (\lambda_Y)^{\mathrm{hom}} = (\rho_X)^{\mathrm{hom}} \triangleright Y$$$
Lean4
theorem triangle (X Y : LocalizedMonoidal L W ε) : (α_ X (𝟙_ _) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y :=
by
obtain ⟨X', ⟨e₁⟩⟩ : ∃ X₁, Nonempty ((L').obj X₁ ≅ X) := ⟨_, ⟨(L').objObjPreimageIso X⟩⟩
obtain ⟨Y', ⟨e₂⟩⟩ : ∃ X₂, Nonempty ((L').obj X₂ ≅ Y) := ⟨_, ⟨(L').objObjPreimageIso Y⟩⟩
have h₁ := (associator_hom_app L W ε X' (𝟙_ _) Y' =≫ (𝟙 ((L').obj X') ⊗ₘ (μ L W ε (𝟙_ C) Y').hom))
simp only [assoc, id_tensorHom, ← whiskerLeft_comp, Iso.inv_hom_id, whiskerLeft_id, comp_id, Iso.inv_hom_id,
← cancel_mono (μ L W ε X' (𝟙_ C ⊗ Y')).hom] at h₁
have h₂ := (ε' L W ε).hom ▷ (L').obj Y' ≫= leftUnitor_hom_app L W ε Y'
simp only [← whiskerRight_comp_assoc, Iso.hom_inv_id, whiskerRight_id, id_comp] at h₂
have h₃ := (((μ L W ε _ _).hom ⊗ₘ 𝟙 _) ≫ (μ L W ε _ _).hom) ≫= ((L').congr_map (MonoidalCategory.triangle X' Y'))
simp only [assoc, Functor.map_comp, ← reassoc_of% h₁] at h₃
rw [← μ_natural_left, tensorHom_id, ← whiskerRight_comp_assoc, ← μ_natural_right, ← Iso.comp_inv_eq, assoc, assoc,
assoc, Iso.hom_inv_id, comp_id, ← whiskerLeft_comp, ← h₂] at h₃
replace h₃ := ((e₁.inv ⊗ₘ ε.inv) ⊗ₘ e₂.inv) ≫= (h₃ =≫ (_ ◁ e₂.hom)) =≫ (e₁.hom ▷ _)
simp only [← whiskerLeft_comp, assoc, ← leftUnitor_naturality, ← whisker_exchange] at h₃
have : _ = (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom := triangle_aux₁ _ _ _ e₁.symm ε.symm e₂.symm
simp only [← this, Iso.symm_hom, Iso.symm_inv, assoc, ← id_tensorHom, ← tensor_comp, comp_id]
convert h₃
· exact triangle_aux₂ _ _ _ e₁ e₂
· exact triangle_aux₃ _ _ _ e₁ e₂
