Theorems · Theorem · general topology

Profinite.exists_isClopen_of_cofiltered

∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J]
  {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {U : Set ↑C.pt.toTop}
  (hC : CategoryTheory.Limits.IsLimit C),
  IsClopen U → ∃ j V, IsClopen V ∧ U = ⇑(CategoryTheory.ConcreteCategory.hom (C.π.app j)) ⁻¹' V

If X is a cofiltered limit of profinite sets, then any clopen subset of X arises from a clopen set in one of the terms in the limit.

Defined in

Mathlib.Topology.Category.Profinite.CofilteredLimit

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsCofiltered