English
A component of the counit relation in the mates correspondence.
Русский
Компонент отношения counit в соответствие mates.
LaTeX
$$$$\\text{mateEquiv_counit}: \\text{...}$$$$
Lean4
theorem unit_mateEquiv (α : TwoSquare G L₁ L₂ H) (c : C) :
G.map (adj₁.unit.app c) ≫ (mateEquiv adj₁ adj₂ α).app _ = adj₂.unit.app _ ≫ R₂.map (α.app _) :=
by
simp only [id_obj, comp_obj, mateEquiv, Equiv.coe_fn_mk, comp_app, rightUnitor_inv_app, Functor.whiskerLeft_app,
associator_hom_app, associator_inv_app, Functor.whiskerRight_app, Functor.comp_map, leftUnitor_hom_app, comp_id,
id_comp]
rw [← adj₂.unit_naturality_assoc]
slice_lhs 2 3 => rw [← R₂.map_comp, ← Functor.comp_map G L₂, α.naturality]
rw [R₂.map_comp]
slice_lhs 3 4 => rw [← R₂.map_comp, Functor.comp_map L₁ H, ← H.map_comp, left_triangle_components]
simp only [comp_obj, map_id, comp_id]
