English
Let L1 ⊣ R1, L2 ⊣ R2, L3 ⊣ R3 be adjunctions between categories C and D. For morphisms α: L2 → L1 and β: L3 → L2, the conjugation functor is compatible with composition in the sense that conjugateEquiv(adj1, adj2)(α) followed by conjugateEquiv(adj2, adj3)(β) equals conjugateEquiv(adj1, adj3)(β ∘ α).
Русский
Пусть между категориями C и D существуют сопряжения L1 ⊣ R1, L2 ⊣ R2, L3 ⊣ R3. Для морфизмов α: L2 → L1 и β: L3 → L2 верно, что конъюгированное соответствие (conjugateEquiv) совместимо с композицией: conjugateEquiv(adj1, adj2)(α) ∘ conjugateEquiv(adj2, adj3)(β) = conjugateEquiv(adj1, adj3)(β ∘ α).
LaTeX
$$$\\text{conjugateEquiv }\\!\\langle adj_1, adj_2\\rangle(\\alpha) \circ \\text{conjugateEquiv }\\!\\langle adj_2, adj_3\\rangle(\\beta) = \\text{conjugateEquiv }\\!\\langle adj_1, adj_3\\rangle(\\beta \\circ \\alpha) $$$
Lean4
@[simp]
theorem conjugateEquiv_comp (α : L₂ ⟶ L₁) (β : L₃ ⟶ L₂) :
conjugateEquiv adj₁ adj₂ α ≫ conjugateEquiv adj₂ adj₃ β = conjugateEquiv adj₁ adj₃ (β ≫ α) :=
by
ext d
dsimp [conjugateEquiv, mateEquiv]
have vcomp :=
mateEquiv_vcomp adj₁ adj₂ adj₃ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)
(L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)
have vcompd := congr_app vcomp d
simp only [comp_obj, id_obj, mateEquiv_apply, comp_app, rightUnitor_inv_app, Functor.whiskerLeft_app,
associator_hom_app, associator_inv_app, Functor.whiskerRight_app, hComp_app, leftUnitor_hom_app, comp_id, id_comp,
Functor.id_map, map_comp, Functor.comp_map, assoc, whiskerRight_comp, whiskerLeft_comp, vComp_app,
map_id] at vcompd ⊢
rw [vcompd]
