English
A key compatibility that witnesses adjointification of η and ε.
Русский
Ключевая совместимость, доказывающая существование сопряжённости между η и ε.
LaTeX
$$$F.map ((adjointify\\eta\\eta\\varepsilon).hom.app X) \\;\\circ \\; \\varepsilon.hom.app (F.obj X) = 𝟙 (F.obj X)$$$
Lean4
@[reassoc]
theorem adjointify_η_ε (X : C) : F.map ((adjointifyη η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X) :=
by
dsimp [adjointifyη, Trans.trans]
simp only [comp_id, assoc, map_comp]
have := ε.hom.naturality (F.map (η.inv.app X)); dsimp at this; rw [this]; clear this
rw [← assoc _ _ (F.map _)]
have := ε.hom.naturality (ε.inv.app <| F.obj X); dsimp at this; rw [this]; clear this
have := (ε.app <| F.obj X).hom_inv_id; dsimp at this; rw [this]; clear this
rw [id_comp]; have := (F.mapIso <| η.app X).hom_inv_id; dsimp at this; rw [this]
