leftToRight_app_map_adj₁_unit_app

English

For each X, t.rightToLeft.app X is epi if and only if the corresponding mapped composition is epi.

Русский

Для каждого X компонент t.rightToLeft.app X эпиморфен тогда и только тогда, когда соответствующая отображённая композиция эпиморфна.

LaTeX

$$$\forall X,\; \operatorname{Epi}(t.rightToLeft.app X) \iff \operatorname{Epi}(t.adj_1.counit.app (H.obj X) \;\circ\; \text{...})$$$

Lean4

@[reassoc (attr := simp)]
theorem leftToRight_app_map_adj₁_unit_app (X : C) :
    t.leftToRight.app X ≫ H.map (t.adj₁.unit.app X) = t.adj₂.unit.app (F.obj X) := by simp [leftToRight_app]

Похожие утверждения