English
A conjugation mapping between two adjunctions induces a correspondence on mates.
Русский
Сопоставление конъюгаций между двумя сопутствующими сопряжениями порождает соответствие мейт.
LaTeX
$$$$ (conjugateEquiv (adj1) (adj2)) \\; \\text{on } \\alpha$$$$
Lean4
/-- The mates equivalence commutes with horizontal composition of squares. -/
theorem mateEquiv_hcomp (α : TwoSquare G L₁ L₂ H) (β : TwoSquare H L₃ L₄ K) :
(mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (α ≫ᵥ β) = (mateEquiv adj₃ adj₄ β) ≫ₕ (mateEquiv adj₁ adj₂ α) :=
by
unfold vComp hComp mateEquiv Adjunction.comp
ext c
simp only [comp_obj, whiskerRight_comp, assoc, mk'_unit, whiskerLeft_comp, mk'_counit, whiskerRight_twice,
Iso.inv_hom_id_assoc, Equiv.coe_fn_mk, comp_app, id_obj, rightUnitor_inv_app, Functor.whiskerLeft_app,
Functor.whiskerRight_app, map_id, associator_inv_app, associator_hom_app, Functor.comp_map, rightUnitor_hom_app,
leftUnitor_hom_app, comp_id, id_comp, whiskerLeft_twice, Iso.hom_inv_id_assoc]
slice_rhs 2 4 => rw [← R₂.map_comp, ← R₂.map_comp, ← assoc, ← unit_naturality (adj₄)]
rw [R₂.map_comp, L₄.map_comp, R₄.map_comp, R₂.map_comp]
slice_rhs 4 5 => rw [← R₂.map_comp, ← R₄.map_comp, ← Functor.comp_map _ L₄, β.naturality]
simp only [comp_obj, Functor.comp_map, map_comp, assoc]
