adj₁_counit_app_rightToLeft_app

English

For each X, t.rightToLeft.app X is epi if and only if F.map(t.adj₂.counit.app X) is epi.

Русский

Для каждого X компонент RightToLeft.app X является эпиморфиальным тогда и только тогда, когда F.map(counit.adj₂.app X) эпиморфен.

LaTeX

$$$\forall X,\; \operatorname{Epi}(t.rightToLeft.app X) \iff \operatorname{Epi}\big(F.map\big(t.adj_2.counit.app X\big)\big)$$$

Lean4

@[reassoc (attr := simp)]
theorem adj₁_counit_app_rightToLeft_app (X : C) :
    t.adj₁.counit.app (H.obj X) ≫ t.rightToLeft.app X = F.map (t.adj₂.counit.app X) :=
  G.map_injective (by simp [← cancel_epi (t.adj₁.unit.app _)])

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