English
Conjugation commutes with whiskering on the left: conjugateEquiv (adj1.comp adj2) (adj1.comp adj2') (l1 ◁ φ) = whisker on the right of φ by adjunction results.
Русский
Сопряжение сохраняет левый whisker: conjugateEquiv (adj1.comp adj2) (adj1.comp adj2') (l1 ◁ φ) = φ свернуть справа через adjoint.
LaTeX
$$$$ \\text{conjugateEquiv} (adj_1\\cdot adj_2) (adj_1\\cdot adj_2') (l_1 \\triangleleft \\phi) = \\text{conjugateEquiv} adj_2 adj_2' \\phi \\;\\triangleright\\; r_1. $$$$
Lean4
theorem conjugateEquiv_whiskerLeft {a b c : B} {l₁ : a ⟶ b} {r₁ : b ⟶ a} (adj₁ : l₁ ⊣ r₁) {l₂ : b ⟶ c} {r₂ : c ⟶ b}
(adj₂ : l₂ ⊣ r₂) {l₂' : b ⟶ c} {r₂' : c ⟶ b} (adj₂' : l₂' ⊣ r₂') (φ : l₂' ⟶ l₂) :
conjugateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂') (l₁ ◁ φ) = conjugateEquiv adj₂ adj₂' φ ▷ r₁ :=
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, whiskerLeft_rightUnitor, triangle_assoc_comp_left_inv_assoc,
Iso.hom_inv_id_assoc] at this
simp [conjugateEquiv_apply, this]
