Theorems · Definition · category theory

Profinite.NobelingProof.spanFunctor

{I : Type u} →
  {C : Set (I → Bool)} →
    [(s : Finset I) → (i : I) → Decidable (i ∈ s)] → IsCompact C → CategoryTheory.Functor (Finset I)ᵒᵖ Profinite

For a given compact subset C of I → Bool, spanFunctor is the functor from the poset of finsets of I to Profinite, sending a finite subset set J to the image of C under the projection Proj J.

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

Decidable