full_linearCoyoneda — Mathlib

English

The linear Coyoneda construction is full when transported along forgetful functors into ModuleCat.

Русский

Линейная Coyoneda-конструкция полна при переносе через забывающие функторы в ModuleCat.

LaTeX

$$$\\text{linearCoyoneda } R C \\text{ is full under forgetful whiskering.}$$$

Lean4

instance full_linearCoyoneda : (linearCoyoneda R C).Full :=
  let _ : Functor.Full (linearCoyoneda R C ⋙ (whiskeringRight _ _ _).obj (forget (ModuleCat.{v} R))) :=
    Coyoneda.coyoneda_full
  Functor.Full.of_comp_faithful (linearCoyoneda R C) ((whiskeringRight _ _ _).obj (forget (ModuleCat.{v} R)))

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