scale in nLab

Contents

This entry is about scales in algebra and linear logic. For scales in geometry and physics, see length scale.

Contents

Idea

The idea of a scale comes from Peter Freyd, in his attempt to give an algebraic (in the sense of universal algebra) description of the real interval, which he believed to be more fundamental than the real numbers themselves in analysis, and of concepts from analysis such as Lipschitz continuity, limits, differentiation and differential equations. Freyd also discovered that scales are models of multiplicative-additive linear logic with a midpoint operation.

Definition

A scale is a minor scale MM satisfying the scale identities:

• for all aa and bb in MM, a⊗b=(a ∨⊗b ∧)|(a ∧⊗b ∨)a \otimes b = (a^\vee \otimes b^\wedge) \vert (a^\wedge \otimes b^\vee)

• for all aa and bb in MM, a⊕b=(a ∧⊕b ∨)|(a ∨⊕b ∧)a \oplus b = (a^\wedge \oplus b^\vee) \vert (a^\vee \oplus b^\wedge)

Properties

Every scale with ⊥=⊤\bot = \top is trivial.

As a scale is a closed midpoint algebra, a scale has a partial order ≤\leq. For all aa and bb in MM, a≤ba \leq b if and only if a⊸b=⊤a \multimap b = \top.

A subset ℐ\mathcal{I} of a scale MM is an ideal if ⊥∈ℐ\bot \in \mathcal{I}, and x∨y∈ℐx \vee y \in \mathcal{I} if and only if x∈ℐx \in \mathcal{I} and y∈ℐy \in \mathcal{I}. An ideal is a zoom-invariant ideal if it is closed under ⊥\bot-zooming.

A subset ℐ\mathcal{I} of a scale MM is a ⊥\bot-face if ⊥∈ℐ\bot \in \mathcal{I}, and x|y∈ℐx \vert y \in \mathcal{I} if and only if x∈ℐx \in \mathcal{I} and y∈ℐy \in \mathcal{I}.

Every ⊥\bot-face is a zoom-invariant ideal.

Given an element aa in scale MM, a principal ⊥\bot-face ((a))((a)) is the subset of all bb in MM such that (⊥|) nb≤a(\bot\vert)^n b \leq a for all large nn in ℕ\mathbb{N}.

A Jacobson radical of a scale MM is the set J(M)J(M) of all aa in MM such that for all nn in ℕ\mathbb{N}, x≤(⊥|) n⊤x \leq (\bot\vert)^n \top. MM is semi-simple if J(M)J(M) is trivial.

The proof of the Linear Representation Theorem in section 8 of Algebraic Real Analysis by Peter Freyd requires the use of excluded middle through its implicit definition of the quasiorder <\lt from the algebraically defined partial order ≤\leq. In particular, that every scale is a *-autonomous category and thus a model for linear logic and that every equational axiom added to the theory of minor scales is either a consequence of the scale identity for scales or is inconsistent with the theory of minor scales are classical results, as certain lemmas used in the proofs have only been derived from the scale identities through the Linear Representation Theorem. The same is true of the definition of simple scales in section 10, of the algebraic construction of the standard interval II from simple scales in section 11, and various results involving absolute retracts in section 25. Since quasiorders can be constructed from partial orders in any set with a tight apartness relation, these results hold if the scales have a tight apartness relation, but it is unknown if these results still hold for general scales in constructive mathematics.

Examples

The unit interval with a|b≔a+b2a \vert b \coloneqq \frac{a + b}{2}, ⊙=12\odot = \frac{1}{2}, a •=1−aa^\bullet = 1 - a, ⊥=0\bot = 0, ⊤=1\top = 1, a ∧=max(2a−1,0)a^\wedge = max(2a-1,0), and a ∨=min(2a,1)a^\vee = min(2a,1) is an example of a scale.

The set of truth values in Girard’s linear logic is a scale.

• minor scale

• Heyting scale

• linear logic

References

• Peter Freyd, Algebraic real analysis, Theory and Applications of Categories, Vol. 20, 2008, No. 10, pp 215-306 (tac:20-10)