Theorems · Definition · category theory

CompHausLike.LocallyConstant.counitAppApp

{P : TopCat → Prop} →
  [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    [inst : CompHausLike.HasProp P PUnit.{u + 1}] →
      (S : CompHausLike P) →
        (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) →
          [CategoryTheory.Limits.PreservesFiniteProducts Y] →
            [CompHausLike.HasExplicitFiniteCoproducts P] →
              LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))) ⟶ Y.obj (Opposite.op S)

The counit is defined as follows: given a locally constant map f : S → Y(*), let S = S₁ ⊔ ⋯ ⊔ Sₙ be the corresponding decomposition of S into the fibers. We need to provide an element of Y(S). It suffices to provide an element of Y(Sᵢ) for all i. Let yᵢ ∈ Y(*) denote the value of f on Sᵢ. Our desired element is the image of yᵢ under the canonical map Y(*) → Y(Sᵢ).

Defined in

Mathlib.Condensed.Discrete.LocallyConstant

Cited by

5 results in Mathlib

Foundations

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

Assumes

CompHausLike.HasPropCompHausLike.HasPropCategoryTheory.Limits.PreservesFiniteProductsCompHausLike.HasExplicitFiniteCoproducts