English
The unit-compatibility isomorphism of the LeftAdjointCommShift construction is compatible with all the specified coherences (the long naturality computation).
Русский
Совместимость единичного изоморфизма с координациями LeftAdjointCommShift описана единичной природной связью.
LaTeX
$$$\\text{LeftAdjointCommShift}.compatibilityUnit\\_iso\\ adj\\ a$ satisfies the coherence equations with the shift and unit/counit data.$$
Lean4
/-- The commutation isomorphisms of `Adjunction.LeftAdjointCommShift.iso` are compatible with
the unit of the adjunction.
-/
theorem compatibilityUnit_iso (a : A) : CommShift.CompatibilityUnit adj (iso adj a) (G.commShiftIso a) :=
by
intro
rw [LeftAdjointCommShift.iso_hom_app adj _ _ (add_neg_cancel a)]
simp only [Functor.id_obj, Functor.comp_obj, Functor.map_shiftFunctorCompIsoId_inv_app, Functor.map_comp, assoc,
unit_naturality_assoc, right_triangle_components_assoc]
slice_rhs 4 5 => rw [← Functor.map_comp, Iso.inv_hom_id_app]
simp only [Functor.comp_obj, Functor.map_id, id_comp]
rw [shift_shiftFunctorCompIsoId_inv_app, ← Functor.comp_map,
(shiftFunctorCompIsoId C _ _ (neg_add_cancel a)).hom.naturality_assoc]
simp
