nLab formal topology

Formal topology

This entry is about a generalized notion of topology. For the notion of formal space in the sense of rational homotopy theory, see formal dg-algebra.


Context

Topology

topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory

Introduction

Basic concepts

Universal constructions

Extra stuff, structure, properties

Examples

Basic statements

Theorems

Analysis Theorems

topological homotopy theory

Formal topology

Idea

Formal topology is a programme for doing topology in a finite, predicative, and constructive fashion.

It is a kind of pointless topology; in the context of classical mathematics, it reproduces the theory of locales rather than topological spaces (although of course one can recover topological spaces from locales).

The basic definitions can be motivated by an attempt to study locales entirely through the posites that generate them. However, in order to recover all basic topological notions (particularly those associated with closed rather than open features) predicatively, we need to add a ‘positivity’ relation to the ‘coverage’ relation of sites.

Definitions

A formal topology or formal space is a set SS together with

such that

  1. a=ba = b whenever a{b}a \lhd \{b\} and b{a}b \lhd \{a\},
  2. aUa \lhd U whenever aUa \in U,
  3. aVa \lhd V whenever aUa \lhd U and xVx \lhd V for all xUx \in U,
  4. abUa \cap b \lhd U whenever aUa \lhd U or bUb \lhd U,
  5. a{xy|xU,yV}a \lhd \{ x \cap y \;|\; x \in U,\; y \in V \} whenever aUa \lhd U and aVa \lhd V,
  6. a{}a \lhd \{\top\},
  7. x\Diamond x for some xUx \in U whenever a\Diamond a and aUa \lhd U, and
  8. aUa \lhd U whenever aUa \lhd U if a\Diamond a,

for all aa, bb, UU, and VV.

We interpret the elements of SS as basic opens in the formal space. We call \top the entire space and aba \cap b the intersection of aa and bb. We say that aa is covered by UU or that UU is a cover of aa if aUa \lhd U. We say that aa is positive or inhabited if a\Diamond a. (For a topological space equipped with a strict topological base SS, taking these intepretations literally does in fact define a formal space; see the Examples.)

Some immediate points to notice:

  • If we drop (1), then the hypothesis of (1) defines an equivalence relation on SS which is a congruence for \top, \cap, \lhd, and \Diamond, so that we may simply pass to the quotient set. In appropriate foundations, we can even allow SS to be a preset originally, then use (1) as a definition of equality.
  • We can prove that (S,,)(S,\cap,\top) is a bounded semilattice; if (as the notation suggests) we interpret this as a meet-semilattice, then aba \leq b if and only if a{b}a \lhd \{b\}. Conversely, we could require that (S,,)(S,\cap,\top) be a semilattice originally, then let (1) say that aba \leq b whenever a{b}a \lhd \{b\}.
  • We can prove that a\Diamond a holds iff every cover of aa is inhabited and that a\Diamond a fails iff aa \lhd \empty. Accordingly, this predicate is uniquely definable (in two equivalent ways, one impredicative and one nonconstructive) in a classical treatment; only in a treatment that is both predicative and constructive do we need to include it in the axioms. See positivity predicate.

Examples

Let XX be a topological space, and let SS be the collection of open subsets of XX. Let \top be XX itself, and let aba \cap b be the literal intersection of aa and bb for a,bSa, b \in S. Let aUa \lhd U if and only UU is literally an open cover of aa, and let a\Diamond a if and only if aa is literally inhabited. Then (S,,,,)(S,\top,\cap,\lhd,\Diamond) is a formal topology.

The above example is impredicative (since the collection of open subsets is generally large), but now let SS be a base for the topology of XX which is strict in the sense that it is closed under finitary intersection. Let the other definitions be as before. Then (S,,,,)(S,\top,\cap,\lhd,\Diamond) is a formal topology.

More generally, let BB be a subbase for the topology of XX, and let SS be the free monoid on BB, that is the set of finite lists of elements of BB (so this example is not strictly finitist), modulo the equivalence relation by which two lists are identified if their intersections are equal. Let \top be the empty list, let aba \cap b be the concatenation of aa and bb, let aUa \lhd U if the intersection of aa is contained in the union of the intersections of the elements of UU, and let a\Diamond a if the intersection of aa is inhabited. Then (S,,,,)(S,\top,\cap,\lhd,\Diamond) is a formal topology.

Let XX be an accessible locale generated by a posite whose underlying poset SS is a (meet)-semilattice. Let \top and \cap be as in the semilattice structure on SS, and let aUa \lhd U if UU contains a basic cover (in the posite structure on SS) of aa. Then we get a formal topology, defining \Diamond in the unique way.

The last example is not predicative, and this is in part why one studies formal topologies instead of sites, if one wishes to be strictly predicative. (It still needs to be motivated that we want \Diamond at all.)

 In dependent type theory

Impredicative definition

In dependent type theory, let (Ω,El Ω)(\Omega, \mathrm{El}_\Omega) be the type of all propositions, and let the relation a SAa \in_S A for a:Sa:S and A:SΩA:S \to \Omega as

a SAEl Ω(A(a))a \in_S A \coloneqq \mathrm{El}_\Omega(A(a))

The singleton subtype function is a function {}:S(SΩ)\{-\}:S \to (S \to \Omega), such that for all elements a:Sa:S, p(a):a S{a}p(a):a \in_S \{a\}, and for all functions R:S(SΩ)R:S \to (S \to \Omega) such that for all elements a:Sa:S, p R(a):a SR(a)p_R(a):a \in_S R(a), the type of functions (b S{a})(b SR(a))(b \in_S \{a\}) \to (b \in_S R(a)) is contractible for all a:Aa:A and b:Ab:A.

A formal topology or formal space is a type SS together with

such that

  1. For all elements a:Sa:S and b:Sb:S, the canonical function
    idToFormalTop(a,b):(a= Sb)((a{b})×(b{a}))\mathrm{idToFormalTop}(a, b):(a =_S b) \to ((a \lhd \{b\}) \times (b \lhd \{a\}))

    is an equivalence of types.

    a:S b:SisEquiv(idToFormalTop(a,b))\prod_{a:S} \prod_{b:S} \mathrm{isEquiv}(\mathrm{idToFormalTop}(a, b))
  2. For all elements a:Sa:S and subsets A:SΩA:S \to \Omega, if a SAa \in_S A, then aAa \lhd A
    a:S A:SΩ(a SA)(aA)\prod_{a:S} \prod_{A:S \to \Omega} (a \in_S A) \to (a \lhd A)
  3. For all elements a:Sa:S and subsets A:SΩA:S \to \Omega and B:SΩB:S \to \Omega, if aAa \lhd A and for all elements x:Sx:S, xBx \lhd B and x SAx \in_S A, then aBa \lhd B
    a:S A:SΩ B:SΩ((aA)× x:S(x SA)×(xB))(aB)\prod_{a:S} \prod_{A:S \to \Omega} \prod_{B:S \to \Omega} \left((a \lhd A) \times \prod_{x:S} (x \in_S A) \times (x \lhd B)\right) \to (a \lhd B)
  4. For all elements a:Sa:S and b:Sb:S and subsets A:SΩA:S \to \Omega, if aAa \lhd A or bAb \lhd A, then abAa \cap b \lhd A.
    a:S b:S A:SΩ((aA)×(bA))(abA)\prod_{a:S} \prod_{b:S} \prod_{A:S \to \Omega} ((a \lhd A) \times (b \lhd A)) \to (a \cap b \lhd A)
  5. For all elements a:Sa:S and subsets A:SΩA:S \to \Omega and B:SΩB:S \to \Omega, if aAa \lhd A and aBa \lhd B, then
    a z:S x:S y:S(x SA)×(y SB)×(z= Sxu)a \lhd \sum_{z:S} \prod_{x:S} \prod_{y:S} (x \in_S A) \times (y \in_S B) \times (z =_S x \cap u)
    a:S A:SΩ B:SΩ(aA)×(aB)(a z:S x:S y:S(x SA)×(y SB)×(z= Sxy))\prod_{a:S} \prod_{A:S \to \Omega} \prod_{B:S \to \Omega} (a \lhd A) \times (a \lhd B) \to \left(a \lhd \sum_{z:S} \prod_{x:S} \prod_{y:S} (x \in_S A) \times (y \in_S B) \times (z =_S x \cap y)\right)
  6. For all elements a:Sa:S, a{}a \lhd \{\top\},
    a:Sa{}\prod_{a:S} a \lhd \{\top\}
  7. For all elements a:Sa:S and subsets A:SΩA:S \to \Omega, if a\Diamond a and aAa \lhd A, there exists an element x:Sx:S such that x SAx \in_S A and x\Diamond x.
    a:S A:SΩ(a)×(aA) x:S(x SA)×(x)\prod_{a:S} \prod_{A:S \to \Omega} (\Diamond a) \times (a \lhd A) \to \sum_{x:S} (x \in_S A) \times (\Diamond x)
  8. For all elements a:Sa:S and subsets A:SΩA:S \to \Omega, if a\Diamond a implies aAa \lhd A, then aAa \lhd A.
    a:S A:SΩ(aaA)(aA)\prod_{a:S} \prod_{A:S \to \Omega} (\Diamond a \to a \lhd A) \to (a \lhd A)

 Predicative definition

Suppose that the dependent type theory does not have a type of all propositions, nor any type universes. This means that subtypes of a type SS do not form a type, which is necessary for defining the cover relation, which is inherently a relation between elements of SS and subtypes of SS. However, one can resolve this problem by using a definition of formal topology which does not require a cover relation in its definition, and then inductively define the cover relation on SS as a higher inductive family of inductive cover relations for every single type in AA.

Ayberk Tosun in Tosun 2020 defined a formal topology as a poset (A,)(A, \leq) with families of types x:AB(x)x:A \vdash B(x), x:A,y:B(x)C(x,y)x:A, y:B(x) \vdash C(x, y) and a dependent function

d: x:A y:B(x)C(x,y)Ad:\prod_{x:A} \prod_{y:B(x)} C(x, y) \to A

such that

  • for all x:Ax:A, y:B(x)y:B(x), and z:C(x,y)z:C(x, y), d(x,y,z)xd(x, y, z) \leq x
x:A y:B(x) z:C(x,y)d(x,y,z)x\prod_{x:A} \prod_{y:B(x)} \prod_{z:C(x, y)} d(x, y, z) \leq x
  • for all x:Ax:A and x:Ax':A, xxx' \leq x implies that for all y:B(x)y:B(x) one can construct y:B(x)y':B(x') such that for all z:C(x,y)z:C(x, y), one can construct z:C(x,y)z':C(x', y') such that d(x,y,z)d(x,y,z)d(x', y', z') \leq d(x, y, z).
x:A x:A(aa) y:B(x) y:B(x) z:C(x,y) z:C(x,y)d(x,y,z)d(x,y,z)\prod_{x:A} \prod_{x:A'} (a \leq a') \to \prod_{y:B(x)}\sum_{y':B(x')} \prod_{z:C(x, y)} \sum_{z':C(x', y')} d(x', y', z') \leq d(x, y, z)

If one has a type universe UU, then the locally UU-small inductive cover relation is given by

Γa:AΓI:UΓe:IAΓp:x:I.e(x)= AaΓdir U(a,I,e,p):a U(I,e)\frac{\Gamma \vdash a:A \quad \Gamma \vdash I:U \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:\exists x:I.e(x) =_A a}{\Gamma \vdash \mathrm{dir}_U(a, I, e, p):a \lhd_U (I, e)}
Γa:AΓI:UΓe:IAΓb:B(a)Γf: c:C(a,b)d(a,b,c) U(I,e)Γbranch U(a,I,e,b,f):a U(I,e)\frac{\Gamma \vdash a:A \quad \Gamma \vdash I:U \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash b:B(a) \quad \Gamma \vdash f:\prod_{c:C(a, b)} d(a, b, c) \lhd_U (I, e)}{\Gamma \vdash \mathrm{branch}_U(a, I, e, b, f):a \lhd_U (I, e)}
Γa:AΓI:UΓe:IAΓp:a U(I,e)Γq:a U(I,e)Γsquash U(a,I,e,p,q):p= a U(I,e)q\frac{\Gamma \vdash a:A \quad \Gamma \vdash I:U \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:a \lhd_U (I, e) \quad \Gamma \vdash q:a \lhd_U (I, e)}{\Gamma \vdash \mathrm{squash}_U(a, I, e, p, q):p =_{a \lhd_U (I, e)} q}

If one doesn’t have type universes, then one could use the stack semantics instead. Given a type II, the cover relation for II is a higher inductive type family a Iea \lhd_I e between elements a:Aa:A and embeddings of types e:IAe:I \hookrightarrow A generated by the constructors

Γa:AΓItypeΓe:IAΓp:x:I.e(x)= AaΓdir I(a,e,p):a Ie\frac{\Gamma \vdash a:A \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:\exists x:I.e(x) =_A a}{\Gamma \vdash \mathrm{dir}_I(a, e, p):a \lhd_I e}
Γa:AΓItypeΓe:IAΓb:B(a)Γf: c:C(a,b)d(a,b,c) IeΓbranch I(a,e,b,f):a Ie\frac{\Gamma \vdash a:A \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash b:B(a) \quad \Gamma \vdash f:\prod_{c:C(a, b)} d(a, b, c) \lhd_I e}{\Gamma \vdash \mathrm{branch}_I(a, e, b, f):a \lhd_I e}
Γa:AΓItypeΓe:IAΓp:a IeΓq:a IeΓsquash I(a,e,p,q):p= a Ieq\frac{\Gamma \vdash a:A \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:a \lhd_I e \quad \Gamma \vdash q:a \lhd_I e}{\Gamma \vdash \mathrm{squash}_I(a, e, p, q):p =_{a \lhd_I e} q}

Families of types x:AB(x)x:A \vdash B(x) are equivalently functions BAB \to A, so one can express the above definition in terms of single types. A formal topology is a poset (A,)(A, \leq) with a set BB, a function f:BAf:B \to A, a set CC with a function g:CBg:C \to B and a function d:CAd:C \to A, such that

  • for all z:Cz:C, d(z)g(f(z))d(z) \leq g(f(z))
z:Cd(z)g(f(z))\prod_{z:C} d(z) \leq g(f(z))
  • for all x:Ax:A and x:Ax':A, if xxx \leq x', then for all y:By:B, f(y)= Axf(y) =_A x implies that one can construct a y:By':B such that f(y)= Axf(y') =_A x' implies that for all z:Cz:C, g(z)= Byg(z) =_B y implies that one can construct a z:Cz':C such that g(z)= Byg(z') =_B y' implies d(z)d(z)d(z') \leq d(z).
x:A x:A(aa) y:B(f(y)= Ax) y:B(f(y)= Ax) z:C(g(z)= By) z:C(g(z)= By)(d(z)d(z))\prod_{x:A} \prod_{x:A'} (a \leq a') \to \prod_{y:B} (f(y) =_A x) \to \sum_{y':B} (f(y') =_A x') \to \prod_{z:C} (g(z) =_B y) \to \sum_{z':C} (g(z') =_B y') \to (d(z') \leq d(z))

If one has a type universe UU, then the locally UU-small inductive cover relation is given by

ΓBtypeΓCtypeΓf:BAΓg:CBΓd:CA Γa:AΓI:UΓe:IAΓp:x:I.e(x)= AaΓdir U(a,I,e,p):a U(I,e)\frac{ \begin{array}{c} \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:B \to A \quad \Gamma \vdash g:C \to B \quad \Gamma \vdash d:C \to A \\ \Gamma \vdash a:A \quad \Gamma \vdash I:U \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:\exists x:I.e(x) =_A a \end{array} }{\Gamma \vdash \mathrm{dir}_U(a, I, e, p):a \lhd_U (I, e)}
ΓBtypeΓCtypeΓf:BAΓg:CBΓd:CA Γa:AΓI:UΓe:IAΓb:BΓp:f(b)= AaΓh: c:C(g(c)= Bb)(d(c) U(I,e))Γbranch U(a,I,e,b,p,h):a U(I,e)\frac{ \begin{array}{c} \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:B \to A \quad \Gamma \vdash g:C \to B \quad \Gamma \vdash d:C \to A \\ \Gamma \vdash a:A \quad \Gamma \vdash I:U \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash b:B \quad \Gamma \vdash p:f(b) =_A a \quad \Gamma \vdash h:\prod_{c:C} (g(c) =_B b) \to (d(c) \lhd_U (I, e)) \end{array} }{\Gamma \vdash \mathrm{branch}_U(a, I, e, b, p, h):a \lhd_U (I, e)}
ΓBtypeΓCtypeΓf:BAΓg:CBΓd:CA Γa:AΓI:UΓe:IAΓp:a U(I,e)Γq:a U(I,e)Γsquash U(a,I,e,p,q):p= a U(I,e)q\frac{ \begin{array}{c} \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:B \to A \quad \Gamma \vdash g:C \to B \quad \Gamma \vdash d:C \to A \\ \Gamma \vdash a:A \quad \Gamma \vdash I:U \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:a \lhd_U (I, e) \quad \Gamma \vdash q:a \lhd_U (I, e) \end{array} }{\Gamma \vdash \mathrm{squash}_U(a, I, e, p, q):p =_{a \lhd_U (I, e)} q}

If one doesn’t have type universes, then one could use the stack semantics instead. Given a type II, the cover relation for II is a higher inductive type family a Iea \lhd_I e between elements a:Aa:A and embeddings of types e:IAe:I \hookrightarrow A generated by the constructors

ΓBtypeΓCtypeΓf:BAΓg:CBΓd:CA Γa:AΓItypeΓe:IAΓp:x:I.e(x)= AaΓdir I(a,e,p):a Ie\frac{ \begin{array}{c} \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:B \to A \quad \Gamma \vdash g:C \to B \quad \Gamma \vdash d:C \to A \\ \Gamma \vdash a:A \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:\exists x:I.e(x) =_A a \end{array} }{\Gamma \vdash \mathrm{dir}_I(a, e, p):a \lhd_I e}
ΓBtypeΓCtypeΓf:BAΓg:CBΓd:CA Γa:AΓItypeΓe:IAΓb:BΓp:f(b)= AaΓh: c:C(g(c)= Bb)(d(c) Ie)Γbranch I(a,e,b,p,h):a Ie\frac{ \begin{array}{c} \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:B \to A \quad \Gamma \vdash g:C \to B \quad \Gamma \vdash d:C \to A \\ \Gamma \vdash a:A \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash b:B \quad \Gamma \vdash p:f(b) =_A a \quad \Gamma \vdash h:\prod_{c:C} (g(c) =_B b) \to (d(c) \lhd_I e) \end{array} }{\Gamma \vdash \mathrm{branch}_I(a, e, b, p, h):a \lhd_I e}
ΓBtypeΓCtypeΓf:BAΓg:CBΓd:CA Γa:AΓItypeΓe:IAΓp:a IeΓq:a IeΓsquash I(a,e,p,q):p= a Ieq\frac{ \begin{array}{c} \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:B \to A \quad \Gamma \vdash g:C \to B \quad \Gamma \vdash d:C \to A \\ \Gamma \vdash a:A \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:a \lhd_I e \quad \Gamma \vdash q:a \lhd_I e \end{array} }{\Gamma \vdash \mathrm{squash}_I(a, e, p, q):p =_{a \lhd_I e} q}

References

  • Mike Fourman and Grayson (1982); Formal Spaces. This is the original development, intended as an application of locale theory to logic.

  • Giovanni Sambin (1987); Intuitionistic formal spaces; pdf.

    • This is the probably the main reference on the subject.
    • Warning: you can ignore the material about foundations and type theory, but if you do read any of it, the term ‘category’ means (roughly) proper class; this was common in type theory in the 1980s.
  • Giovanni Sambin (2001); Some points in formal topology; pdf. This has newer results, alternative formulations, etc.

  • Erik Palmgren, From Intuitionistic to Point-Free Topology: On the Foundation of Homotopy Theory, Logicism, Intuitionism, and Formalism Volume 341 of the series Synthese Library pp 237-253, 2005 (pdf)

  • Ayberk Tosun, Formal Topology in Univalent Foundations, (pdf, slides)

Last revised on February 7, 2024 at 20:58:42. See the history of this page for a list of all contributions to it.