whiskerRight_rightToLeft — Mathlib

English

If G is fully faithful, whiskering the rightToLeft transformation by G yields the composite of the second adjunction’s counit with the first’s unit.

Русский

Если G полностью верен, то поворот вправо правой стороны (rightToLeft) по G даёт композицию каути-главной второй адъюнкции с единицей первой.

LaTeX

$$$\mathrm{whiskerRight}(t.rightToLeft, G) = t.adj_2.counit \;\circ\; t.adj_1.unit.$$$

Lean4

/-- For an adjoint triple `F ⊣ G ⊣ H` where `G` is fully faithful, whiskering the natural
transformation `H ⟶ F` with `G` yields the composition of the counit of the second adjunction with
the unit of the first adjunction. -/
@[simp, reassoc]
theorem whiskerRight_rightToLeft : whiskerRight t.rightToLeft G = t.adj₂.counit ≫ t.adj₁.unit :=
  ((FullyFaithful.ofFullyFaithful G).whiskeringRight _).map_preimage _

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