whiskerRight_unit_iso_of_R_fully_faithful

English

If L is full and faithful, whiskerRight of the unit with L is an isomorphism.

Русский

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

LaTeX

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

Lean4

instance whiskerRight_unit_iso_of_R_fully_faithful [R.Full] [R.Faithful] : IsIso (whiskerRight h.unit L) :=
  by
  have := h.left_triangle
  rw [← IsIso.eq_comp_inv] at this
  rw [this]
  infer_instance

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