English
If two unit data e2,e2' are compatible with a fixed e1, they must be equal: e2 = e2'.
Русский
Если по фиксированной единице e1 две правые данные совместимости e2 и e2' совпадают, то они равны: e2 = e2'.
LaTeX
$$$ CompatUnit(adj, e_1, e_2) \rightarrow CompatUnit(adj, e_1, e_2') \rightarrow e_2 = 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
counit of the adjunction `adj`, then we get a formula for `e₁.hom` in terms of `e₂`.
-/
theorem compatibilityCounit_left (h : CompatibilityCounit adj e₁ e₂) (X : C) :
e₁.hom.app X = F.map ((adj.unit.app X)⟦a⟧') ≫ F.map (e₂.inv.app _) ≫ adj.counit.app _ :=
by
have := h (F.obj X)
rw [← cancel_epi (F.map (e₂.inv.app _)), ← assoc, ← F.map_comp, Iso.inv_hom_id_app, F.map_id, id_comp] at this
rw [this]
erw [e₁.hom.naturality_assoc]
rw [Functor.comp_map, ← Functor.map_comp, left_triangle_components]
simp only [Functor.comp_obj, Functor.id_obj, Functor.map_id, comp_id]
