TopCat.isTopologicalBasis_cofiltered_limit

theorem TopCat.isTopologicalBasis_cofiltered_limit : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsCofiltered J] (F : CategoryTheory.Functor J TopCatMax) (C : CategoryTheory.Limits.Cone F), CategoryTheory.Limits.IsLimit C → ∀ (T : (j : J) → Set (Set ↑(F.obj j))), (∀ (j : J), TopologicalSpace.IsTopologicalBasis (T j)) → (∀ (i : J), Set.univ ∈ T i) → (∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i) → (∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(F.map f) ⁻¹' V ∈ T i) → TopologicalSpace.IsTopologicalBasis {U | ∃ j, ∃ V ∈ T j, U = ⇑(C.π.app j) ⁻¹' V}

This theorem states that given a collection of topological bases for the factors in a cofiltered limit, which includes the universal set and is closed under intersections, the "naive" collection of sets induced in the limit is a topological basis. This assumes that the collection is "compatible" with the limit, in the sense that for every morphism in the category and every set in the topological basis of the target of the morphism, the preimage of that set under the morphism is in the topological basis of the source of the morphism. The theorem is formulated in the context of a small category `J` that is cofiltered, a functor `F` from `J` to the category of topological spaces, and a cone `C` with apex the limit of `F`. The theorem applies to any such `F` and `C` for which `C` is a limit cone.

More concisely: Given a cofiltered small category J, a functor F from J to the category of topological spaces, and a limit cone C in F with a collection of topological bases for the factors that is closed under intersections and compatible with the limit, the induced collection of sets is a topological basis for the limit.