Theorems · Theorem · general topology

Profinite.exists_locallyConstant_finite_aux

∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J]
  {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {α : Type u_1} [Finite α]
  (hC : CategoryTheory.Limits.IsLimit C) (f : LocallyConstant (↑C.pt.toTop) α),
  ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Defined in

Mathlib.Topology.Category.Profinite.CofilteredLimit

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsCofilteredFinite