Preface to the special issue for The Fifth Workshop on Formal Topology

THIERRY COQUAND, MARIA EMILIA MAIETTI, and ERIK PALMGREN

The paper introduces Formal Topology, which is a constructive approach to pointfree topology. Here we instead look at topologies with points, over finite sets and show:

• there is a unique topology on Fin 0;
• there is a unique topology on Fin 1;
• there exist two distinct topologies on Fin 2
• We also construct the remaining two topologies on Fin 2 giving a total of 4, and show they are homeomorphic.

theorem uniqueTopFin0 (σ τ : TopologicalSpace (Fin 0)) : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen

There is only one topology on Fin 0.

theorem uniqueTopFin1 (σ τ : TopologicalSpace (Fin 1)) : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen

There is only one topology on Fin 1.

theorem nonUniqueTopFin2 : ∃ (σ : TopologicalSpace (Fin 2)) (τ : TopologicalSpace (Fin 2)), TopologicalSpace.IsOpen ≠ TopologicalSpace.IsOpen

There are two distinct topologies on Fin 2.

def mytop (z : Fin 2) : TopologicalSpace (Fin 2)

Here are two more topologies on Fin 2. In fact a topology on Fin 2 must contain Set.univ and ∅, and then there are four possibilities depending on which of {0}, {1} are included.

Equations

• mytop z = { IsOpen := fun (S : Set (Fin 2)) => S = ∅ ∨ S = Set.univ ∨ S = {z}, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

def myequiv : Fin 2 ≃ Fin 2

We can show that the latter two topologies are homeomorphic.

Equations

• myequiv = { toFun := fun (x : Fin 2) => x + 1, invFun := fun (x : Fin 2) => x + 1, left_inv := myequiv._proof_2, right_inv := myequiv._proof_3 }

def myhomeo : Fin 2 ≃ₜ Fin 2

Equations

• myhomeo = { toEquiv := myequiv, continuous_toFun := myhomeo._proof_1, continuous_invFun := myhomeo._proof_2 }