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

@[implicit_reducible]

instance FinTopCat.instInhabited : Inhabited FinTopCat

Equations

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

@[implicit_reducible]

instance FinTopCat.instCoeSortType : CoeSort FinTopCat (Type u)

Equations

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

@[implicit_reducible]

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

Equations

• FinTopCat.instCategory = inferInstanceAs (CategoryTheory.Category.{?u.3, ?u.3 + 1} (CategoryTheory.InducedCategory TopCat FinTopCat.toTop))

@[implicit_reducible]

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

@[implicit_reducible]

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

The forgetful functor to FintypeCat.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

The forgetful functor to TopCat.

Equations

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

@[implicit_reducible]

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

Equations

• X.instFintypeCarrierObjTopCatForget₂ContinuousMapToTop = X.fintype

@[implicit_reducible]

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

@[implicit_reducible]

def FintypeCatDiscrete.instHasForget₂FintypeCatHomCarrierTopCatContinuousMapCarrier : 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.