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) :
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.