map_rightToLeft_app — Mathlib

English

For each object X, applying G to the rightToLeft component at X yields the composite of adj₂’s counit and adj₁’s unit at X.

Русский

Для каждого X применение G к компоненте rightToLeft в X даёт композицию каути adj₂ и единицы adj₁ в X.

LaTeX

$$$G\big(t.rightToLeft.\mathrm{app} X\big) = t.adj_2.counit.\mathrm{app} X \circ t.adj_1.unit.\mathrm{app} X$$$

Lean4

/-- For an adjoint triple `F ⊣ G ⊣ H` where `G` is fully faithful, the images of the components of
the natural transformation `H ⟶ F` under `G` are the components of the composition of counit of the
second adjunction with the unit of the first adjunction. -/
@[simp, reassoc]
theorem map_rightToLeft_app (X : C) : G.map (t.rightToLeft.app X) = t.adj₂.counit.app X ≫ t.adj₁.unit.app X :=
  congr_app t.whiskerRight_rightToLeft X

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