English
The iso corresponding to the right adjoint commShift is compatible with the unit of the adjunction.
Русский
Изоморфизм, связанный с RightAdjointCommShift, совместим с единицей сопряжения.
LaTeX
$$$ \text{compatibilityUnit} adj (\mathrm{RightAdjointCommShift}.iso adj a)(\mathrm{iso} adj a)$$$
Lean4
/-- The commutation isomorphisms of `Adjunction.RightAdjointCommShift.iso` are compatible with
the unit of the adjunction.
-/
theorem compatibilityUnit_iso (a : A) : CommShift.CompatibilityUnit adj (F.commShiftIso a) (iso adj a) :=
by
intro
rw [← cancel_mono ((RightAdjointCommShift.iso adj a).inv.app _), assoc, assoc, Iso.hom_inv_id_app,
RightAdjointCommShift.iso_inv_app adj _ _ (neg_add_cancel a)]
apply (adj.homEquiv _ _).symm.injective
dsimp
simp only [comp_id, homEquiv_counit, Functor.map_comp, assoc, counit_naturality, counit_naturality_assoc,
left_triangle_components_assoc]
erw [← NatTrans.naturality_assoc]
dsimp
rw [shift_shiftFunctorCompIsoId_hom_app, Iso.inv_hom_id_app_assoc, Functor.commShiftIso_hom_naturality_assoc, ←
Functor.map_comp, left_triangle_components, Functor.map_id, comp_id]
