Theorems · Definition · category theory

CompHausLike.LocallyConstantModule.functor

{P : TopCat → Prop} →
  (R : Type (max u w)) →
    [inst : Ring R] →
      [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P] →
        [inst_2 : CompHausLike.HasExplicitPullbacks P] →
          (hs :
              ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
                CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
            CategoryTheory.Functor (ModuleCat R)
              (CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (ModuleCat R))

CompHausLike.LocallyConstantModule.functorToPresheaves lands in sheaves.

Defined in

Mathlib.Condensed.Discrete.Module

Cited by

3 results in Mathlib

Foundations

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

Assumes

RingCompHausLike.HasExplicitFiniteCoproductsCompHausLike.HasExplicitPullbacks