Theorems · Definition · category theory

CompHausLike.LocallyConstantModule.functorToPresheaves

{P : TopCat → Prop} →
  (R : Type (max u w)) →
    [inst : Ring R] → CategoryTheory.Functor (ModuleCat R) (CategoryTheory.Functor (CompHausLike P)ᵒᵖ (ModuleCat R))

The functor from the category of R-modules to presheaves on CompHausLike P given by locally constant maps.

Defined in

Mathlib.Condensed.Discrete.Module

Cited by

4 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Ring