leftToRight_op — Mathlib

English

Another variant of the epi equivalence stating that epi of rightToLeft at X corresponds to epi of F.map of adj₂.counit.app X.

Русский

Ещё одно выражение эквивалентности: эпиморфизм rightToLeft.app X соответствует эпиморфизму F.map adj₂.counit.app X.

LaTeX

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

Lean4

/-- For an adjoint triple `F ⊣ G ⊣ H` where `F` and `H` are fully faithful, the natural
transformation `H.op ⟶ F.op` obtained from the dual adjoint triple `H.op ⊣ G.op ⊣ F.op` is
dual to the natural transformation `F ⟶ H`. -/
@[simp]
theorem leftToRight_op : t.op.leftToRight = NatTrans.op t.leftToRight :=
  by
  ext
  rw [leftToRight, leftToRight_eq_counits]
  simp

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