English
The natural transformation F.op ⟶ H.op obtained from the dual adjoint triple is the dual of rightToLeft.
Русский
Естественное преобразование F.op ⟶ H.op, полученное из двойственной троицы смежностей, является двойным к rightToLeft.
LaTeX
$$@[simp] theorem op_rightToLeft : t.op.rightToLeft = NatTrans.op t.rightToLeft$$
Lean4
/-- For an adjoint triple `F ⊣ G ⊣ H` where `G` is fully faithful and `H` preserves epimorphisms
(which is for example the case if `H` has a further right adjoint), the components of the natural
transformation `H ⟶ F` are epic iff the respective components of the natural transformation
`H ⋙ G ⟶ F ⋙ G` obtained from the units and counits of the adjunctions are. -/
theorem epi_rightToLeft_app_iff [H.PreservesEpimorphisms] {X : C} :
Epi (t.rightToLeft.app X) ↔ Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X) :=
by
have _ := t.adj₂.isLeftAdjoint
refine ⟨fun h ↦ by rw [← map_rightToLeft_app]; exact G.map_epi _, fun h ↦ ?_⟩
rw [epi_rightToLeft_app_iff_epi_map_adj₁_unit_app]
simpa using epi_comp (t.adj₂.unit.app (H.obj X)) (H.map (t.adj₂.counit.app X ≫ t.adj₁.unit.app X))
