English
If e1,e2 and f1,f2 are compatible with unit data, then their sum via isoAdd is compatible as well.
Русский
Если пары изоморфизмов e1,e2 и f1,f2 совместимы с единицей, то их сумма через isoAdd также совместима.
LaTeX
$$$ CompatUnit(adj, e_1, e_2) \rightarrow CompatUnit(adj, f_1, f_2) \rightarrow CompatUnit(adj, IsoAdd(e_1, f_1), IsoAdd(e_2, f_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 `e₂` uniquely determines `e₁`.
-/
theorem compatibilityUnit_unique_left (h : CompatibilityUnit adj e₁ e₂) (h' : CompatibilityUnit adj e₁' e₂) :
e₁ = e₁' := by
ext
rw [compatibilityCounit_left adj e₁ e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h),
compatibilityCounit_left adj e₁' e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h')]
