Theorems · Definition · category theory

Profinite.indexFunctor

{ι : Type u} →
  {X : ι → Type} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {C : Set ((i : ι) → X i)} →
        [∀ (i : ι), T2Space (X i)] →
          [∀ (i : ι), TotallyDisconnectedSpace (X i)] → IsCompact C → CategoryTheory.Functor (Finset ι)ᵒᵖ Profinite

The functor from the poset of finsets of ι to Profinite, indexing the limit.

Defined in

Mathlib.Topology.Category.Profinite.Product

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2SpaceTotallyDisconnectedSpace