ofPresheaf — Mathlib

English

The forgetful functor from CommRingCat to RingCat is full; every ring homomorphism between underlying rings arises from a commutative ring homomorphism.

Русский

Полнoсть функторa забывaния от CommRingCat к RingCat: каждый кольцевой гомоморфизм между соответствующими кольцами исходит из коммутативного кольцевого гомоморфизма.

LaTeX

$$$(\text{forget₂ } CommRingCat RingCat).\text{Full}$$$

Lean4

/-- The object in `PresheafOfModules R` that is obtained from `M : Cᵒᵖ ⥤ Ab.{v}` such
that for all `X : Cᵒᵖ`, `M.obj X` is a `R.obj X` module, in such a way that the
restriction maps are semilinear. (This constructor should be used only in cases
when the preferred constructor `PresheafOfModules.mk` is not as convenient as this one.) -/
@[simps]
noncomputable def ofPresheaf : PresheafOfModules.{v} R
    where
  obj
    X :=
    ModuleCat.of _
      (M.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 _ (M.obj Y)))
      { toFun := fun x ↦ M.map f x
        map_add' := by simp
        map_smul' := fun r m ↦ map_smul f r m }

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