English
Conjugation respects associator: conjugateEquiv (adj1.(adj2.adj3)) ((adj1.adj2).adj3) (α.hom) equals α.hom via associator between the right sides.
Русский
Сопряжение совместимо с ассоциатором: conjugateEquiv (adj1·(adj2·adj3)) ((adj1·adj2)·adj3) (α.hom) = α.hom через ассоциатор.
LaTeX
$$$$ \\text{conjugateEquiv} (adj_1 \\cdot (adj_2 \\cdot adj_3)) ((adj_1 \\cdot adj_2) \\cdot adj_3) (\\alpha_\\text{hom}) = (\\alpha_\\text{hom}) $$$$
Lean4
theorem conjugateEquiv_associator_hom {a b c d : B} {l₁ : a ⟶ b} {r₁ : b ⟶ a} (adj₁ : l₁ ⊣ r₁) {l₂ : b ⟶ c} {r₂ : c ⟶ b}
(adj₂ : l₂ ⊣ r₂) {l₃ : c ⟶ d} {r₃ : d ⟶ c} (adj₃ : l₃ ⊣ r₃) :
conjugateEquiv (adj₁.comp (adj₂.comp adj₃)) ((adj₁.comp adj₂).comp adj₃) (α_ _ _ _).hom = (α_ _ _ _).hom :=
by
simp [← cancel_epi (ρ_ ((r₃ ≫ r₂) ≫ r₁)).hom, ← cancel_mono (λ_ (r₃ ≫ r₂ ≫ r₁)).inv, conjugateEquiv_apply,
mateEquiv_eq_iff, Adjunction.homEquiv₁_symm_apply, Adjunction.homEquiv₂_apply]
bicategory
