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 := FinTopCat.mk { α := PEmpty.{?u.3 + 1}, str := inferInstance } }

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.instConcreteCategory : CategoryTheory.ConcreteCategory FinTopCat

Equations

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

instance FinTopCat.instTopologicalSpaceObjForget (X : FinTopCat) : TopologicalSpace ((CategoryTheory.forget FinTopCat).obj X)

Equations

• X.instTopologicalSpaceObjForget = inferInstanceAs (TopologicalSpace ↑X.toTop)

instance FinTopCat.instFintypeObjForget (X : FinTopCat) : Fintype ((CategoryTheory.forget FinTopCat).obj X)

Equations

• X.instFintypeObjForget = X.fintype

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 = FinTopCat.mk (TopCat.of X)

@[simp]

theorem FinTopCat.coe_of (X : Type u) [Fintype X] [TopologicalSpace X] : ↑(FinTopCat.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.instTopologicalSpaceαFintypeObjFintypeCatForget₂ (X : FinTopCat) : TopologicalSpace ↑((CategoryTheory.forget₂ FinTopCat FintypeCat).obj X)

Equations

• X.instTopologicalSpaceαFintypeObjFintypeCatForget₂ = 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.instFintypeαTopologicalSpaceObjTopCatForget₂ (X : FinTopCat) : Fintype ↑((CategoryTheory.forget₂ FinTopCat TopCat).obj X)

Equations

• X.instFintypeαTopologicalSpaceObjTopCatForget₂ = X.fintype