nLab frame

Contents

This entry is about the notion of frame in topos theory. For other notions, see frame (disambiguation).

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

(0,1)(0,1)-Category theory

Contents

Idea

The notion of frame is a generalization of the notion of category of open subsets of a topological space. A frame is like a category of open subsets in a space possibly more general than a topological space: a locale. This in turn is effectively defined to be anything that has a collection of open subsets that behaves essentially like the open subsets of a topological space do.

Definition

Definition

A frame 𝒪\mathcal{O} is

  • a poset

  • that has

  • and which satisfies the infinite distributive law:

    x( iy i) i(xy i) x \wedge (\bigvee_i y_i) \leq \bigvee_i (x\wedge y_i)

    for all x,{y i} ix, \{y_i\}_i in AA

    (Note that the converse holds in any case, so we have equality.)

A frame homomorphism is a homomorphism of posets that preserves finite meets and arbitrary joins. Frames and frame homomorphisms form the category Frm.

The formal duals of frames, hence the objects in the opposite category Locale :=:= Frm op{}^{op} are called locales.

Remark

The notation 𝒪\mathcal{O} to supposed to remind us that every frame is like a frame of opens of the corresponding locale.

Remark

So in particular a frame is a lattice which has not only finite joins but all small joins. Being small itself, it is a suplattice, and hence a complete lattice: it also has all (small) meets.

Furthermore, as the distributive law certainly holds when the joins in question are finite, it is a distributive lattice.

Properties

A useful way to understand frames and locales is as the simplest nontrivial special cases of (n,1)-toposes. So we start in

with some remarks on this, and only then turn to

of frames, which should make more sense this way.

As a (0,1)(0,1)-topos

The notion of frame – or rather its formal dual, the notion of locale – is the special case of the notion of (n,1)-toposes for n=0n = 0: (0,1)-toposes.

The axioms on a frame are nothing but Giraud's axioms on sheaf toposes, restricted to (0,1)-categories:

given the existence of finite limits and arbitrary colimits, the infinite distributive law expresses that a frame has universal colimits: they are stable under pullback. (For notice that in a poset pullbacks and products coincide.)

Then a morphism of frames is precisely (the inverse image of) a geometric morphism: a morphism preserving finite limits and arbitrary colimits.

General

Proposition

A frame is automatically a Heyting algebra.

In category theoretic terms this means that it ia a cartesian closed category, hence that

for every object x𝒪x \in \mathcal{O} the functor

x():𝒪𝒪 x \wedge (-) : \mathcal{O} \to \mathcal{O}

that forms the product with xx has a right adjoint

x():𝒪𝒪 x \Rightarrow (-) : \mathcal{O} \to \mathcal{O}
Proof

This exists by the adjoint functor theorem, using that there is only a finite number of morphisms between any two objects (one or none) and that finite limits exist in 𝒪\mathcal{O}.

Remark

Therefore one may think of a of a frame as a cartesian closed suplattice, or a cartesian quantale.

But notice that the frame homomorphisms are not required to preserve the Heyting implication.

As sites

A frame is naturally equipped with the structure of a site:

a family of morphism {U iU}\{U_i \to U\} is covering precisely if UU is the union of the U iU_i

iU i=U. \bigvee_i U_i = U \,.

For more on this see locale.

Formal duals: locales

The opposite category to the category Frm is the category Loc of locales (possibly slightly generalized topological spaces)

Loc:=Frm op Loc := Frm^{op}

Conversely, any topological space has a frame of open subsets. (In fact, one definition of a topological space is a set equipped with a subframe of its power set.)

Examples

Example

For XX a topological space, the category of open subsets of XX is a frame: the frame of opens.

Example

For XX a set, the power set 𝒫(X)\mathcal{P}(X) of XX is the frame of opens corresponding to the discrete topology on XX.

Example

The poset of truth values Ω\Omega is a frame equivalent to the frame of opens corresponding to the discrete topology on a singleton.

Proposition

A complete decidable linear order is a frame.

Proof

For any xx and collection y iy_i, the inequality ixy ix iy i\bigvee_i x \wedge y_i \leq x \wedge \bigvee_i y_i holds automatically. For the reverse inequality, we note this follows trivially in case iy ix\bigvee_i y_i \leq x, since in that case we have y ixy_i \leq x for all ii, whence

x iy i= iy i= ixy i.x \wedge \bigvee_i y_i = \bigvee_i y_i = \bigvee_i x \wedge y_i.

Otherwise we are in the case x< iy ix \lt \bigvee_i y_i, where we must show the inequality

x iy i=x ixy ix \wedge \bigvee_i y_i = x \leq \bigvee_i x \wedge y_i

But this inequality must hold, else ixy i<x\bigvee_i x \wedge y_i \lt x which would imply y i<xy_i \lt x for all ii, whence iy ix\bigvee_i y_i \leq x, contradiction.

References

Frames in univalent foundations:

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

Last revised on January 26, 2024 at 19:35:54. See the history of this page for a list of all contributions to it.