Theorems · Definition · category theory

CompHausLike.LocallyConstant.componentHom

{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})))) →
            {T : CompHausLike P} →
              (g : T ⟶ S) →
                (a : Function.Fiber ⇑(LocallyConstant.comap (TopCat.Hom.hom g.hom) f)) →
                  CompHausLike.LocallyConstant.fiber (LocallyConstant.comap (TopCat.Hom.hom g.hom) f) a ⟶
                    CompHausLike.LocallyConstant.fiber f
                      (Function.Fiber.mk (⇑f)
                        ((CategoryTheory.ConcreteCategory.hom g)
                          (Function.Fiber.preimage (⇑(LocallyConstant.comap (TopCat.Hom.hom g.hom) f)) a)))

This is an auxiliary definition, the details do not matter. What's important is that this map exists so that the lemma incl_comap works.

Defined in

Mathlib.Condensed.Discrete.LocallyConstant

Cited by

1 results in Mathlib

Foundations

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

Assumes

CompHausLike.HasPropCompHausLike.HasProp