unit

Mathlib.Algebra.Category.ModuleCat.Presheaf

URI: https://scilib.ai/kg/mathlib#PresheafOfModules.unit

Lean4

/-- The obvious free presheaf of modules of rank `1`. -/
noncomputable def unit : PresheafOfModules R
    where
  obj
    X :=
    ModuleCat.of _
      (R.obj X)
        -- TODO: after https://github.com/leanprover-community/mathlib4/pull/19511 we need to hint `(Y := ...)`.
          -- This suggests `restrictScalars` needs to be redesigned.

  map {X Y}
    f :=
    ModuleCat.ofHom (Y := (ModuleCat.restrictScalars (R.map f).hom).obj (ModuleCat.of (R.obj Y) (R.obj Y)))
      { toFun := fun x ↦ R.map f x
        map_add' := by simp
        map_smul' := by cat_disch }

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru