Theorems · Theorem · category theory

Profinite.exists_hom

∀ {I : Type u} [inst : CategoryTheory.SmallCategory I] [CategoryTheory.IsCofiltered I]
  {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite))
  (hc : CategoryTheory.Limits.IsLimit c) {X : FintypeCat} (f : c.pt ⟶ FintypeCat.toProfinite.obj X),
  ∃ i g, f = CategoryTheory.CategoryStruct.comp (c.π.app i) (FintypeCat.toProfinite.map g)

A continuous map from a profinite set to a finite set factors through one of the components of the profinite set when written as a cofiltered limit of finite sets.

Defined in

Mathlib.Topology.Category.Profinite.Extend

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsCofiltered