English
The mates equivalence commutes with horizontal composition of squares.
Русский
Сопоставление mates сохраняет горизонтальную композицию квадратов.
LaTeX
$$$$ (\\text{mateEquiv (adj1.adj2) (adj3.adj4)}) (\\alpha \\; \\hcomp \\; \\beta) = (\\text{mateEquiv adj3 adj4 } \\beta) \\; \\hcomp \\; (\\text{mateEquiv adj1 adj2 } \\alpha). $$$$
Lean4
/-- The mates equivalence commutes with vertical composition. -/
theorem mateEquiv_vcomp (α : TwoSquare G₁ L₁ L₂ H₁) (β : TwoSquare G₂ L₂ L₃ H₂) :
(mateEquiv adj₁ adj₃) (α ≫ₕ β) = (mateEquiv adj₁ adj₂ α) ≫ᵥ (mateEquiv adj₂ adj₃ β) :=
by
unfold hComp vComp mateEquiv
ext b
simp only [comp_obj, Equiv.coe_fn_mk, whiskerRight_comp, whiskerRight_twice, assoc, whiskerLeft_comp, comp_app,
id_obj, rightUnitor_inv_app, Functor.whiskerLeft_app, associator_hom_app, associator_inv_app,
Functor.whiskerRight_app, map_id, Functor.comp_map, leftUnitor_hom_app, comp_id, id_comp, whiskerLeft_twice,
Iso.hom_inv_id_assoc]
slice_rhs 1 4 => rw [← assoc, ← assoc, ← unit_naturality (adj₃)]
rw [L₃.map_comp, R₃.map_comp]
slice_rhs 2 4 =>
rw [← R₃.map_comp, ← R₃.map_comp, ← assoc, ← L₃.map_comp, ← G₂.map_comp, ← G₂.map_comp]
rw [← Functor.comp_map G₂ L₃, β.naturality]
rw [(L₂ ⋙ H₂).map_comp, R₃.map_comp, R₃.map_comp]
slice_rhs 4 5 =>
rw [← R₃.map_comp, Functor.comp_map L₂ _, ← Functor.comp_map _ L₂, ← H₂.map_comp]
rw [adj₂.counit.naturality]
simp only [comp_obj, Functor.comp_map, map_comp, id_obj, Functor.id_map, assoc]
slice_rhs 4 5 => rw [← R₃.map_comp, ← H₂.map_comp, ← Functor.comp_map _ L₂, adj₂.counit.naturality]
simp only [comp_obj, id_obj, Functor.id_map, map_comp, assoc]
slice_rhs 3 4 => rw [← R₃.map_comp, ← H₂.map_comp, left_triangle_components]
simp only [map_id, id_comp]
