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

Equations

• FinTopCat.instInhabited = { default := { toTop := TopCat.of PEmpty.{?u.2 + 1}, fintype := Fintype.instPEmpty } }

instance FinTopCat.instCoeSortType : CoeSort FinTopCat (Type u)

Equations

• FinTopCat.instCoeSortType = { coe := fun (X : FinTopCat) => ↑X.toTop }

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

Equations

• FinTopCat.instCategory = CategoryTheory.InducedCategory.category FinTopCat.toTop

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

Equations

• FinTopCat.instConcreteCategoryContinuousMapCarrierToTop = CategoryTheory.InducedCategory.concreteCategory FinTopCat.toTop

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

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

Equations

• FinTopCat.of X = { toTop := TopCat.of X, fintype := inst✝¹ }

@[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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• X.instTopologicalSpaceCarrierObjFintypeCatForget₂ = inferInstanceAs (TopologicalSpace ↑X.toTop)

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

The forgetful functor to TopCat.

Equations

• FinTopCat.instHasForget₂TopCat = CategoryTheory.InducedCategory.hasForget₂ FinTopCat.toTop

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

Equations

• X.instFintypeCarrierObjTopCatForget₂ = X.fintype

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

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

Equations

• FintypeCatDiscrete.instTopologicalSpaceCarrier X = ⊥

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.

Equations

• One or more equations did not get rendered due to their size.