Documentation

Mathlib.Topology.Category.DeltaGenerated

Delta-generated topological spaces #

The category of delta-generated spaces.

See https://ncatlab.org/nlab/show/Delta-generated+topological+space.

Adapted from Mathlib/Topology/Category/CompactlyGenerated.lean.

TODO #

source
structure DeltaGenerated :
Type (u + 1)

The type of delta-generated topological spaces.

Instances For
    source
    @[implicit_reducible]
    instance DeltaGenerated.instCoeSortType :
    CoeSort DeltaGenerated (Type u_1)
    source
    @[implicit_reducible]
    instance DeltaGenerated.instLargeCategory :
    CategoryTheory.LargeCategory DeltaGenerated
    source
    @[implicit_reducible]
    instance DeltaGenerated.instConcreteCategoryContinuousMapCarrierToTop :
    CategoryTheory.ConcreteCategory DeltaGenerated fun (x1 x2 : DeltaGenerated) => C(↑x1.toTop, ↑x2.toTop)
    source
    @[reducible, inline]
    abbrev DeltaGenerated.of (X : Type u) [TopologicalSpace X] [DeltaGeneratedSpace X] :
    DeltaGenerated

    Constructor for objects of the category DeltaGenerated

    Instances For
      source
      def DeltaGenerated.deltaGeneratedToTop :
      CategoryTheory.Functor DeltaGenerated TopCat

      The forgetful functor DeltaGenerated ⥤ TopCat

      Instances For
        source
        @[simp]
        theorem DeltaGenerated.deltaGeneratedToTop_obj (self : DeltaGenerated) :
        deltaGeneratedToTop.obj self = self.toTop
        source
        @[simp]
        theorem DeltaGenerated.deltaGeneratedToTop_map {X✝ Y✝ : CategoryTheory.InducedCategory TopCat toTop} (f : X✝ ⟶ Y✝) :
        deltaGeneratedToTop.map f = f.hom
        source
        def DeltaGenerated.fullyFaithfulDeltaGeneratedToTop :
        deltaGeneratedToTop.FullyFaithful

        deltaGeneratedToTop is fully faithful.

        Instances For
          source
          instance DeltaGenerated.instFullTopCatDeltaGeneratedToTop :
          deltaGeneratedToTop.Full
          source
          instance DeltaGenerated.instFaithfulTopCatDeltaGeneratedToTop :
          deltaGeneratedToTop.Faithful
          source
          def DeltaGenerated.topToDeltaGenerated :
          CategoryTheory.Functor TopCat DeltaGenerated

          The faithful (but not full) functor taking each topological space to its delta-generated coreflection.

          Instances For
            source
            @[simp]
            theorem DeltaGenerated.topToDeltaGenerated_map_hom_hom_apply {x✝ Y : TopCat} (f : x✝ ⟶ Y) (a : ↑x✝) :
            (TopCat.Hom.hom (topToDeltaGenerated.map f).hom) a = (CategoryTheory.ConcreteCategory.hom f) a
            source
            @[simp]
            theorem DeltaGenerated.topToDeltaGenerated_obj_toTop_carrier (X : TopCat) :
            ↑(topToDeltaGenerated.obj X).toTop = DeltaGeneratedSpace.of ↑X
            source
            instance DeltaGenerated.instFaithfulTopCatTopToDeltaGenerated :
            topToDeltaGenerated.Faithful
            source
            def DeltaGenerated.coreflectorAdjunction :
            deltaGeneratedToTop ⊣ topToDeltaGenerated

            The adjunction between the forgetful functor DeltaGenerated ⥤ TopCat and its coreflector.

            Instances For
              source
              @[implicit_reducible]
              instance DeltaGenerated.deltaGeneratedToTop.coreflective :
              CategoryTheory.Coreflective deltaGeneratedToTop

              The category of delta-generated spaces is coreflective in the category of topological spaces.

              source
              @[implicit_reducible]
              noncomputable instance DeltaGenerated.deltaGeneratedToTop.createsColimits :
              CategoryTheory.CreatesColimits deltaGeneratedToTop
              source
              instance DeltaGenerated.hasLimits :
              CategoryTheory.Limits.HasLimits DeltaGenerated
              source
              instance DeltaGenerated.hasColimits :
              CategoryTheory.Limits.HasColimits DeltaGenerated