Theorems · Definition · category theory

CompHausLike.LocallyConstant.sigmaIso

{P : TopCat → Prop} →
  [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    {Q : CompHausLike P} →
      {Z : Type (max u w)} →
        (r : LocallyConstant (↑Q.toTop) Z) →
          [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P] →
            CompHausLike.finiteCoproduct (CompHausLike.LocallyConstant.fiber r) ≅ Q

The canonical map from the coproduct induced by f to S as an isomorphism in CompHausLike P.

Defined in

Mathlib.Condensed.Discrete.LocallyConstant

Cited by

4 results in Mathlib

Foundations

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

Assumes

CompHausLike.HasPropCompHausLike.HasExplicitFiniteCoproducts