Category of finite topological spaces

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

structure FinTopCat : Type (u + 1)

A bundled finite topological space.

• toTop : TopCat

  carrier of a finite topological space.

• fintype : Fintype ↑self.toTop

instance FinTopCat.instInhabited : Inhabited FinTopCat

instance FinTopCat.instCoeSortType : CoeSort FinTopCat (Type u)

instance FinTopCat.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} FinTopCat

instance FinTopCat.instConcreteCategoryContinuousMapCarrierToTop : CategoryTheory.ConcreteCategory FinTopCat fun (x1 x2 : FinTopCat) => C(↑x1.toTop, ↑x2.toTop)

def FinTopCat.of (X : Type u) [Fintype X] [TopologicalSpace X] : FinTopCat

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

@[simp]

theorem FinTopCat.coe_of (X : Type u) [Fintype X] [TopologicalSpace X] : ↑(of X).toTop = X

instance FinTopCat.instHasForget₂FintypeCat : CategoryTheory.HasForget₂ FinTopCat FintypeCat

The forgetful functor to FintypeCat.

instance FinTopCat.instTopologicalSpaceCarrierObjFintypeCatForget₂ (X : FinTopCat) : TopologicalSpace ((CategoryTheory.forget₂ FinTopCat FintypeCat).obj X).carrier

instance FinTopCat.instHasForget₂TopCat : CategoryTheory.HasForget₂ FinTopCat TopCat

The forgetful functor to TopCat.

instance FinTopCat.instFintypeCarrierObjTopCatForget₂ (X : FinTopCat) : Fintype ↑((CategoryTheory.forget₂ FinTopCat TopCat).obj X)

def FintypeCatDiscrete.instTopologicalSpaceCarrier (X : FintypeCat) : TopologicalSpace X.carrier

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

theorem FintypeCatDiscrete.instDiscreteTopologyCarrier (X : FintypeCat) : DiscreteTopology X.carrier

def FintypeCatDiscrete.instHasForget₂FintypeCatTopCat : CategoryTheory.HasForget₂ FintypeCat TopCat

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