Theorems · Theorem · category theory

CompHausLike.LocallyConstant.incl_of_counitAppApp

∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  {S : CompHausLike P} {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))}
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}]
  (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))))
  [inst_2 : CategoryTheory.Limits.PreservesFiniteProducts Y] [inst_3 : CompHausLike.HasExplicitFiniteCoproducts P]
  (a : Function.Fiber ⇑f),
  (CategoryTheory.ConcreteCategory.hom (Y.map (CompHausLike.LocallyConstant.sigmaIncl f a).op))
      ((CategoryTheory.ConcreteCategory.hom (CompHausLike.LocallyConstant.counitAppApp S Y)) f) =
    CompHausLike.LocallyConstant.counitAppAppImage f a

Defined in

Mathlib.Condensed.Discrete.LocallyConstant

Cited by

3 results in Mathlib

Foundations

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

Assumes

CompHausLike.HasPropCompHausLike.HasPropCategoryTheory.Limits.PreservesFiniteProductsCompHausLike.HasExplicitFiniteCoproducts