Theorems · Theorem · category theory

TopCat.isTopologicalBasis_cofiltered_limit

∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [CategoryTheory.IsCofiltered J]
  (F : CategoryTheory.Functor J TopCat) (C : CategoryTheory.Limits.Cone F) (hC : 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, ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i) →
          TopologicalSpace.IsTopologicalBasis
            {U | ∃ j, ∃ V ∈ T j, U = ⇑(CategoryTheory.ConcreteCategory.hom (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.

Defined in

Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofiltered