English
Given an adjunction and a unit-counit compatible setup, the unit and its shifts are compatible with the shift commutation at the level of unit-counit data.
Русский
Для данных единицы и кавитации в сопряженном случае совместимость единицы сохраняется при работе со сдвигами и коммутативностью сдвигов.
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`, compatibility of `e₁` and `e₂` with the
unit of the adjunction `adj` implies compatibility with the counit of `adj`.
-/
theorem compatibilityCounit_of_compatibilityUnit (h : CompatibilityUnit adj e₁ e₂) : CompatibilityCounit adj e₁ e₂ :=
by
intro Y
have eq := h (G.obj Y)
simp only [← cancel_mono (e₂.inv.app _ ≫ G.map (e₁.inv.app _)), assoc, Iso.hom_inv_id_app_assoc, comp_id,
← Functor.map_comp, Iso.hom_inv_id_app, Functor.comp_obj, Functor.map_id] at eq
apply (adj.homEquiv _ _).injective
dsimp
rw [adj.homEquiv_unit, adj.homEquiv_unit, G.map_comp, adj.unit_naturality_assoc, ← eq]
simp only [assoc, ← Functor.map_comp, Iso.inv_hom_id_app_assoc]
erw [← e₂.inv.naturality]
dsimp
simp only [right_triangle_components, ← Functor.map_comp_assoc, Functor.map_id, id_comp, Iso.hom_inv_id_app,
Functor.comp_obj]
