mathlib3 documentation

topology.category.Top.limits.cofiltered

Cofiltered limits in Top. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given a compatible collection of topological bases for the factors in a cofiltered limit which contain set.univ and are closed under intersections, the induced naive collection of sets in the limit is, in fact, a topological basis.

theorem Top.is_topological_basis_cofiltered_limit {J : Type v} [category_theory.small_category J] [category_theory.is_cofiltered J] (F : J Top) (C : category_theory.limits.cone F) (hC : category_theory.limits.is_limit C) (T : Π (j : J), set (set (F.obj j))) (hT : (j : J), topological_space.is_topological_basis (T j)) (univ : (i : J), set.univ T i) (inter : (i : J) (U1 U2 : set (F.obj i)), U1 T i U2 T i U1 U2 T i) (compat : (i j : J) (f : i j) (V : set (F.obj j)), V T j (F.map f) ⁻¹' V T i) :
topological_space.is_topological_basis {U : set (C.X) | (j : J) (V : set (F.obj j)), V T j U = (C.π.app j) ⁻¹' V}

Given a compatible collection of topological bases for the factors in a cofiltered limit which contain set.univ and are closed under intersections, the induced naive collection of sets in the limit is, in fact, a topological basis.