English
If unit-isos e1,e2 and e1',e2' satisfy the unit compatibility, then e1 = e1'.
Русский
Если единичные изоморфизмы удовлетворяют условию совместимости, то e1 = e1'.
LaTeX
$$$ CompatUnit(adj, e_1, e_2) \rightarrow CompatUnit(adj, e_1', e_2) \rightarrow e_1 = e_1'$$$
Lean4
/-- Given an adjunction `adj : F ⊣ G`, `a, b` in `A` and commutation isomorphisms
between shifts by `a` (resp. `b`) and `F` and `G`, if these commutation isomorphisms are
compatible with the unit of `adj`, then so are the commutation isomorphisms between shifts
by `a + b` and `F` and `G` constructed by `Functor.CommShift.isoAdd`.
-/
theorem compatibilityUnit_isoAdd (h : CompatibilityUnit adj e₁ e₂) (h' : CompatibilityUnit adj f₁ f₂) :
CompatibilityUnit adj (Functor.CommShift.isoAdd e₁ f₁) (Functor.CommShift.isoAdd e₂ f₂) :=
by
intro X
have := h' (X⟦a⟧)
simp only [← cancel_mono (f₂.inv.app _), assoc, Iso.hom_inv_id_app, Functor.id_obj, Functor.comp_obj, comp_id] at this
simp only [Functor.id_obj, Functor.comp_obj, Functor.CommShift.isoAdd_hom_app, Functor.map_comp, assoc,
unit_naturality_assoc]
slice_rhs 5 6 => rw [← G.map_comp, Iso.inv_hom_id_app]
simp only [Functor.comp_obj, Functor.map_id, id_comp, assoc]
erw [f₂.hom.naturality_assoc]
rw [← reassoc_of% this, ← cancel_mono ((shiftFunctorAdd C a b).hom.app _), assoc, assoc, assoc, assoc, assoc, assoc,
Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]
dsimp
rw [← (shiftFunctor C b).map_comp_assoc, ← (shiftFunctor C b).map_comp_assoc, assoc, ← h X, NatTrans.naturality]
dsimp
rw [comp_id]
