functorToPresheaves — Mathlib

English

The counit projection at a fiber a acts by mapping the fiber element through the terminal projection.

Русский

Проекция куша при отвечает за отображение элемента волокна через терминал.

LaTeX

$$$\\text{counitAppAppImage}(f)\\;(a) = Y.map\\big(\\text{isTerminalPUnit.from} (f)\\big)^{op}\\; a.\\text{image}$$$

Lean4

/-- The functor from the category of `R`-modules to presheaves on `CompHausLike P` given by locally
constant maps.
-/
@[simps]
def functorToPresheaves : ModuleCat.{max u w} R ⥤ ((CompHausLike.{u} P)ᵒᵖ ⥤ ModuleCat R)
    where
  obj
    X :=
    { obj := fun ⟨S⟩ ↦ ModuleCat.of R (LocallyConstant S X)
      map := fun f ↦ ModuleCat.ofHom (comapₗ R f.unop.hom) }
  map f := { app := fun S ↦ ModuleCat.ofHom (mapₗ R f.hom) }

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