English
In a setting of shift compatibility, a pair of isomorphisms e1,e2 is compatible with the unit; this yields a well-defined relation among shifted components.
Русский
В условиях совместимости сдвигов пары изоморфизмов e1,e2 совместимы с единицей; образуется последовательность связанных компонентов.
LaTeX
$$$ CompatibilityUnit(adj, e_1, e_2)$$$
Lean4
/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, if `e₁` and `e₂` are compatible with the
unit of the adjunction `adj`, then we get a formula for `e₂.inv` in terms of `e₁`.
-/
theorem compatibilityUnit_right (h : CompatibilityUnit adj e₁ e₂) (Y : D) :
e₂.inv.app Y = adj.unit.app _ ≫ G.map (e₁.hom.app _) ≫ G.map ((adj.counit.app _)⟦a⟧') :=
by
have := h (G.obj Y)
rw [← cancel_mono (e₂.inv.app _), assoc, assoc, Iso.hom_inv_id_app] at this
erw [comp_id] at this
rw [← assoc, ← this, assoc]; erw [← e₂.inv.naturality]
rw [← cancel_mono (e₂.hom.app _)]
simp only [Functor.comp_obj, Iso.inv_hom_id_app, Functor.id_obj, Functor.comp_map, assoc, comp_id,
← (shiftFunctor C a).map_comp, right_triangle_components, Functor.map_id]
