Theorems · Definition · category theory

Profinite.Extend.functor

{I : Type u} →
  [inst : CategoryTheory.SmallCategory I] →
    {F : CategoryTheory.Functor I FintypeCat} →
      (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) →
        CategoryTheory.Functor I (CategoryTheory.StructuredArrow c.pt FintypeCat.toProfinite)

Given a cone in Profinite, consisting of finite sets and indexed by a cofiltered category, we obtain a functor from the indexing category to StructuredArrow c.pt toProfinite.

Defined in

Mathlib.Topology.Category.Profinite.Extend

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategory