Theorems · Theorem · category theory

CompHausLike.LocallyConstantModule.functor_obj_obj_obj_carrier

∀ {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))
  (X : ModuleCat R) (x : (CompHausLike P)ᵒᵖ),
  ↑(((CompHausLike.LocallyConstantModule.functor R hs).obj X).obj.obj x) = LocallyConstant ↑(Opposite.unop x).toTop ↑X

Defined in

Mathlib.Condensed.Discrete.Module

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingCompHausLike.HasExplicitFiniteCoproductsCompHausLike.HasExplicitPullbacks