Coherent space

From Wikipedia, the free encyclopedia

In proof theory, a coherent space is a concept introduced in the semantic study of linear logic.

Let a set C be given. Two subsets S,T ⊆ C are said to be orthogonal, written S ⊥ T, if S ∩ T is ∅ or a singleton. For a family of C-sets (i.e., F ⊆ ℘(C)), the dual of F, written F ^⊥, is defined as the set of all C-sets S such that for every T ∈ F, S ⊥ T. A coherent space F over C is a family C-sets for which F = (F ^⊥) ^⊥.

In topology, a coherent space is a sober space with a basis of compact sets in which finite intersections preserve the property of being compact open. A continuous map between coherent spaces is called coherent if its associated preimage map takes compact open sets to compact open sets.

In Proofs and Types coherent spaces are called coherence spaces. A footnote explains that although in the French original they were espaces cohérents, the coherence space translation was used because spectral spaces are sometimes called coherent spaces.