whiskerRight_counit_iso_of_L_fully_faithful

English

If L is full and faithful, then whiskerRight of the counit with R is an isomorphism.

Русский

Если L полно и верно, то whiskerRight counit R — изоморфизм.

LaTeX

$$$\big( L\text{ Full} \land L\text{ Faithful} \big) \Rightarrow \text{IsIso}(\mathrm{whiskerRight}(h.counit, R))$$$

Lean4

instance whiskerRight_counit_iso_of_L_fully_faithful [L.Full] [L.Faithful] : IsIso (whiskerRight h.counit R) :=
  by
  have := h.right_triangle
  rw [← IsIso.eq_inv_comp] at this
  rw [this]
  infer_instance

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