English
The functor Type u ⥤ SheafOfModules(R) sending a type I to the free sheaf on I; on morphisms it sends f to freeMap f and respects identities and composition.
Русский
Функтор от типов к свободной оболочке модулей над R: I ↦ free I, на отображениях f ↦ freeMap f, с сохранением тождеств и композиции.
LaTeX
$$$\mathrm{freeFunctor} : \mathbf{Type}_u \to \mathrm{SheafOfModules}(R)$$$
Lean4
/-- The functor `Type u ⥤ SheafOfModules.{u} R` which sends a type `I` to
`free I` which is a coproduct indexed by `I` of copies of `R` (thought of as a
presheaf of modules over itself). -/
noncomputable def freeFunctor : Type u ⥤ SheafOfModules.{u} R
where
obj := free
map f := freeMap f
map_id X := (freeHomEquiv _).injective (by ext1 i; simp)
map_comp {I J K} f g := (freeHomEquiv _).injective (by ext1; simp [freeHomEquiv_comp_apply])
