English
Conjugation commutes with whiskering on the right: conjugateEquiv (adj1.comp adj2) (adj1'.comp adj2) (φ ▷ l2) = r2 ▷ conjugateEquiv adj1 adj1' φ.
Русский
Сопряжение сохраняет правый whisker: conjugateEquiv (adj1.comp adj2) (adj1'.comp adj2) (φ ▷ l2) = r2 ◁ conjugateEquiv adj1 adj1' φ.
LaTeX
$$$$ \\text{conjugateEquiv} (adj_1\\cdot adj_2) (adj_1'\\cdot adj_2) (\\phi \\;\\triangleright\\; l_2) = r_2 \\;\\triangleleft\\; conjugateEquiv adj_1 adj_1' \\phi. $$$$
Lean4
theorem conjugateEquiv_whiskerRight {a b c : B} {l₁ : a ⟶ b} {r₁ : b ⟶ a} (adj₁ : l₁ ⊣ r₁) {l₁' : a ⟶ b} {r₁' : b ⟶ a}
(adj₁' : l₁' ⊣ r₁') {l₂ : b ⟶ c} {r₂ : c ⟶ b} (adj₂ : l₂ ⊣ r₂) (φ : l₁' ⟶ l₁) :
conjugateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂) (φ ▷ l₂) = r₂ ◁ conjugateEquiv adj₁ adj₁' φ :=
by
have := mateEquiv_hcomp adj₁ adj₁' adj₂ adj₂ ((λ_ _).hom ≫ φ ≫ (ρ_ _).inv) ((λ_ _).hom ≫ (ρ_ _).inv)
dsimp [leftAdjointSquare.hcomp, rightAdjointSquare.hcomp] at this
simp only [comp_whiskerRight, leftUnitor_whiskerRight, Category.assoc, whiskerLeft_comp, whiskerLeft_rightUnitor_inv,
Iso.hom_inv_id, Category.comp_id, triangle_assoc, inv_hom_whiskerRight_assoc, Iso.inv_hom_id_assoc,
mateEquiv_leftUnitor_hom_rightUnitor_inv, leftUnitor_inv_whiskerRight, Iso.inv_hom_id,
triangle_assoc_comp_right_assoc] at this
simp [conjugateEquiv_apply, this]
