English
Let h be a commutative square with functors T, L, R, B. Then applying vInv to the left-hand data, and then again to the result, yields back the original square h.
Русский
Пусть имеется комм-квадрат с факторми T, L, R, B. Тогда применение vInv к левому набору данных, затем повторное применение к полученному результату возвращает исходный квадрат h.
LaTeX
$$Theorem vInv_vInv (h : CatCommSq T L.functor R.functor B.functor) : vInv B L.symm R.symm T (vInv T L R B h) = h$$
Lean4
theorem vInv_vInv (h : CatCommSq T L.functor R.functor B) : vInv B L.symm R.symm T (vInv T L R B h) = h :=
by
ext X
rw [vInv_iso_hom_app]
dsimp
rw [vInv_iso_inv_app]
rw [← cancel_mono (B.map (L.functor.map (NatTrans.app L.unitIso.hom X)))]
rw [← Functor.comp_map]
dsimp
simp only [Functor.map_comp, Equivalence.fun_inv_map, Functor.comp_obj, Functor.id_obj, assoc,
Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app, comp_id]
rw [← B.map_comp, L.counit_app_functor, ← L.functor.map_comp, ← NatTrans.comp_app, Iso.inv_hom_id, NatTrans.id_app,
L.functor.map_id]
simp only [Functor.comp_obj]
rw [B.map_id]
rw [comp_id, R.counit_app_functor, ← R.functor.map_comp_assoc, ← R.functor.map_comp_assoc, assoc, ← NatTrans.comp_app,
Iso.hom_inv_id, NatTrans.id_app]
simp
