whiskerLeft_counit_iso_of_L_fully_faithful

English

If L is full and faithful, then whiskerLeft L of the counit is an isomorphism.

Русский

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

LaTeX

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

Lean4

instance whiskerLeft_counit_iso_of_L_fully_faithful [L.Full] [L.Faithful] : IsIso (whiskerLeft L h.counit) :=
  by
  have := h.left_triangle
  rw [← IsIso.eq_inv_comp] at this
  rw [this]
  infer_instance

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