full_linearYoneda — Mathlib

English

The linear Yoneda functor is full after composing with forgetful whiskering through ModuleCat.

Русский

Линейный Yoneda-функтор полнотe после компоновки с забывающим whiskering через ModuleCat.

LaTeX

$$$\\text{linearYoneda } R C \\text{ is full via composition with forgetful whiskering.}$$$

Lean4

instance full_linearYoneda : (linearYoneda R C).Full :=
  let _ : Functor.Full (linearYoneda R C ⋙ (whiskeringRight _ _ _).obj (forget (ModuleCat.{v} R))) := Yoneda.yoneda_full
  Functor.Full.of_comp_faithful (linearYoneda R C) ((whiskeringRight _ _ _).obj (forget (ModuleCat.{v} R)))

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