freeYoneda — Mathlib

English

The collection of objects of the category PresheafOfModules consisting precisely of those objects that are formed as (free R).obj (yoneda.obj X) for some X.

Русский

Множество объектов в категории PresheafOfModules состоит ровно из тех объектов, которые имеют вид (free R).obj (yoneda.obj X) для некоторого X.

LaTeX

$$$\\{\, (\\mathrm{free}\\;R)(\\mathrm{yoneda}(X)) \\mid X \\text{ object in } C \\}$ as a subset of PresheafOfModules R$$

Lean4

/-- The set of `PresheafOfModules.{v} R` consisting of objects of the
form `(free R).obj (yoneda.obj X)` for some `X`. -/
def freeYoneda : Set (PresheafOfModules.{v} R) :=
  Set.range (yoneda ⋙ free R).obj

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