rightToLeft_app_adj₂_unit_app — Mathlib

English

If G is fully faithful, Epi(t.rightToLeft.app X) is equivalent to Epi(H.map(adj₁.unit.app X)).

Русский

Если G полностью верен, то эпиморфизм t.rightToLeft.app X эквивалентен эпиморфизму H.map(adj₁.unit.app X).

LaTeX

$$$\forall X,\; \operatorname{Epi}(t.rightToLeft.app X) \iff \operatorname{Epi}\big(H.map\big( t.adj_1.unit.app X \big)\big)$$$

Lean4

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

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