English
A key inverse triangle equality.
Русский
Ключевое обратное треугольное тождество.
LaTeX
$$$e.inverse.map (e.counitInv.app Y) \\;\\circ \\; e.unitInv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y)$$$
Lean4
/-- The other triangle equality. The proof follows the following proof in Globular:
http://globular.science/1905.001 -/
@[reassoc (attr := simp)]
theorem unit_inverse_comp (e : C ≌ D) (Y : D) :
e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y) :=
by
rw [← id_comp (e.inverse.map _), ← map_id e.inverse, ← counitInv_functor_comp, map_comp]
dsimp
rw [← Iso.hom_inv_id_assoc (e.unitIso.app _) (e.inverse.map (e.functor.map _)), Iso.app_hom, Iso.app_inv]
slice_lhs 2 3 => rw [← e.unit_naturality]
slice_lhs 1 2 => rw [← e.unit_naturality]
slice_lhs 4 4 => rw [← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)]
slice_lhs 3 4 =>
dsimp only [Functor.mapIso_hom, Iso.app_hom]
rw [← map_comp e.inverse, e.counit_naturality, e.counitIso.hom_inv_id_app]
dsimp only [Functor.comp_obj]
rw [map_id]
dsimp only [comp_obj, id_obj]
rw [id_comp]
slice_lhs 2 3 =>
dsimp only [Functor.mapIso_inv, Iso.app_inv]
rw [← map_comp e.inverse, ← e.counitInv_naturality, map_comp]
slice_lhs 3 4 => rw [e.unitInv_naturality]
slice_lhs 4 5 =>
rw [← map_comp e.inverse, ← map_comp e.functor, e.unitIso.hom_inv_id_app]
dsimp only [Functor.id_obj]
rw [map_id, map_id]
dsimp only [comp_obj, id_obj]
rw [id_comp]
slice_lhs 3 4 => rw [← e.unitInv_naturality]
slice_lhs 2 3 => rw [← map_comp e.inverse, e.counitInv_naturality, e.counitIso.hom_inv_id_app]
dsimp only [Functor.comp_obj]
simp
