Documentation

Mathlib.Topology.Category.FinTopCat

Category of finite topological spaces #

Definition of the category of finite topological spaces with the canonical forgetful functors.

source
🔶 coverage
structure FinTopCat :
Type (u + 1)

A bundled finite topological space.

Instances For
    source
    🔸 coverage
    @[implicit_reducible]
    instance FinTopCat.instInhabited :
    Inhabited FinTopCat
    source
    🔸 coverage
    @[implicit_reducible]
    instance FinTopCat.instCoeSortType :
    CoeSort FinTopCat (Type u)
    source
    🔸 coverage
    @[implicit_reducible]
    instance FinTopCat.instCategory :
    CategoryTheory.Category.{u_1, u_1 + 1} FinTopCat
    source
    🔸 coverage
    @[implicit_reducible]
    instance FinTopCat.instConcreteCategoryContinuousMapCarrierToTop :
    CategoryTheory.ConcreteCategory FinTopCat fun (x1 x2 : FinTopCat) => C(↑x1.toTop, ↑x2.toTop)
    source
    🔸 coverage
    def FinTopCat.of (X : Type u) [Fintype X] [TopologicalSpace X] :
    FinTopCat

    Construct a bundled FinTopCat from the underlying type and the appropriate typeclasses.

    Instances For
      source
      📐 coverage
      @[simp]
      theorem FinTopCat.coe_of (X : Type u) [Fintype X] [TopologicalSpace X] :
      ↑(of X).toTop = X
      source
      🔸 coverage
      @[implicit_reducible]
      instance FinTopCat.instHasForget₂ContinuousMapCarrierToTopFintypeCatHomObjFinite :
      CategoryTheory.HasForget₂ FinTopCat FintypeCat

      The forgetful functor to FintypeCat.

      source
      🔸 coverage
      @[implicit_reducible]
      instance FinTopCat.instTopologicalSpaceObjFiniteObjFintypeCatForget₂ContinuousMapCarrierToTopHom (X : FinTopCat) :
      TopologicalSpace ((CategoryTheory.forget₂ FinTopCat FintypeCat).obj X).obj
      source
      🔸 coverage
      @[implicit_reducible]
      instance FinTopCat.instHasForget₂ContinuousMapCarrierToTopTopCat :
      CategoryTheory.HasForget₂ FinTopCat TopCat

      The forgetful functor to TopCat.

      source
      🔸 coverage
      @[implicit_reducible]
      instance FinTopCat.instFintypeCarrierObjTopCatForget₂ContinuousMapToTop (X : FinTopCat) :
      Fintype ↑((CategoryTheory.forget₂ FinTopCat TopCat).obj X)
      source
      🔸 coverage
      @[implicit_reducible]
      def FintypeCatDiscrete.instTopologicalSpaceObjFinite (X : FintypeCat) :
      TopologicalSpace X.obj

      Scoped topological space instance on objects of the category of finite types, assigning the discrete topology.

      Instances For
        source
        📐 coverage
        theorem FintypeCatDiscrete.instDiscreteTopologyObjFinite (X : FintypeCat) :
        DiscreteTopology X.obj
        source
        🔸 coverage
        @[implicit_reducible]
        def FintypeCatDiscrete.instHasForget₂FintypeCatHomObjFiniteTopCatContinuousMapCarrier :
        CategoryTheory.HasForget₂ FintypeCat TopCat

        The forgetful functor from finite types to topological spaces, forgetting discreteness. This is a scoped instance.

        Instances For