ncatlab.org

locator in nLab

Contents

Context

Analysis

Contents

Definition

In the real numbers

A locator for a real number c∈ℝc \in \mathbb{R} is an element of the indexed cartesian product

l∈∏ a∈ℚ∏ b∈ℚ([{d∈ℝ|a<d<c}]⊎[{d∈ℝ|c<d<b}]) [{d∈ℝ|a<d<b}]l \in \prod_{a \in \mathbb{Q}} \prod_{b \in \mathbb{Q}} \left([\{d \in \mathbb{R} \vert a \lt d \lt c\}] \uplus [\{d \in \mathbb{R} \vert c \lt d \lt b\}]\right)^{[\{d \in \mathbb{R} \vert a \lt d \lt b\}]}

where A⊎BA \uplus B is the disjoint union of two sets AA and BB, B AB^A is the set of functions from AA to BB, [A][A] is the support of AA, and the indexed cartesian product is defined in set theory as

∏ a∈AB(a)={f∈(⋃ a∈AB(a)) A|∀a,f(a)∈B(a)}\prod_{a \in A} B(a) = \{f \in \left(\bigcup_{a\in A} B(a)\right)^A \vert \forall a, f(a) \in B(a) \}

for family of sets (B(a)) a∈A(B(a))_{a \in A}.

Equivalently, a locator is an element of the indexed cartesian product

l∈∏ a∈ℚ∏ b∈ℚ[{d∈ℝ|a<d<c}] [{d∈ℝ|a<d<b}]×[{d∈ℝ|c<d<b}] [{d∈ℝ|a<d<b}]l \in \prod_{a \in \mathbb{Q}} \prod_{b \in \mathbb{Q}} [\{d \in \mathbb{R} \vert a \lt d \lt c\}]^{[\{d \in \mathbb{R} \vert a \lt d \lt b\}]} \times [\{d \in \mathbb{R} \vert c \lt d \lt b\}]^{[\{d \in \mathbb{R} \vert a \lt d \lt b\}]}

In arbitrary dense linear orders

Given a dense linear order (A,< A)(A, \lt_A), the open interval in AA between elements a∈Aa \in A and b∈Bb \in B is the set

OpenInt(a,b)={c∈A|a<c<b}\mathrm{OpenInt}(a,b) = \{c \in A \vert a \lt c \lt b\}

Given a countable dense linear order (B,< B)(B, \lt_B) such that B⊆AB \subseteq A and for all elements a∈Aa \in A and b∈Ab \in A where a<ba \lt b, there exists c∈Bc \in B such that a<c<ba \lt c \lt b, a BB-indexed locator for an element c∈Ac \in A is an element of the indexed cartesian product

l∈∏ a∈B∏ b∈B([OpenInt(a,c)]⊎[OpenInt(c,b)]) [OpenInt(a,b)]l \in \prod_{a \in B} \prod_{b \in B} \left([\mathrm{OpenInt}(a,c)] \uplus [\mathrm{OpenInt}(c,b)]\right)^{[\mathrm{OpenInt}(a,b)]}

In dependent type theory

In dependent type theory, given a real number r:ℝr:\mathbb{R}, a locator on the Dedekind real numbers is a dependent function

l:∏ p:ℚ∏ q:ℚ(p<q)→((p<r)+(r<q))l:\prod_{p:\mathbb{Q}} \prod_{q:\mathbb{Q}} (p \lt q) \to ((p \lt r) + (r \lt q))

This above type is equivalent to the types

∏ p:ℚ∏ q:ℚ(p<q)→∑ b:bool((b=1)→(p<r))×((b=0)→(r<q))\prod_{p:\mathbb{Q}} \prod_{q:\mathbb{Q}} (p \lt q) \to \sum_{b:\mathrm{bool}} ((b = 1) \to (p \lt r)) \times ((b = 0) \to (r \lt q))

∏ p:ℚ∏ q:ℚ(p<q)→∑ b:bool((b=0)→(p<r))×((b=1)→(r<q))\prod_{p:\mathbb{Q}} \prod_{q:\mathbb{Q}} (p \lt q) \to \sum_{b:\mathrm{bool}} ((b = 0) \to (p \lt r)) \times ((b = 1) \to (r \lt q))

Properties

Principle of locators

Note: The “principle of locators” or “axiom of locators” are placeholder names for a principle or axiom which may or may not have an already existing name in the mathematics literature.

The principle of locators state that every real number x:ℝx:\mathbb{R} merely has a locator (i.e. the support of the locator has an element), and implies that the Cauchy real numbers is the terminal Archimedean ordered field, and coincides with the Dedekind real numbers. This is true in classical mathematics, as is in constructive mathematics which also uses countable choice.

However, in general constructive mathematics, while theorem 6.10.3 of Booij 2020 states that a real number is a Cauchy real number if and only if it merely has a locator, not every real number is necessarily a Cauchy real number, so it is not necessarily true that every real number has a locator. In that case, this principle becomes the axiom of locators, which says that every element x:ℝx:\mathbb{R} of the terminal Archimedean ordered field ℝ\mathbb{R} merely has a locator, making it coincide with the Cauchy real numbers. We use terminal Archimedean ordered field since in predicative mathematics the Dedekind real numbers may not exist.

References

Last revised on February 13, 2024 at 01:56:07. See the history of this page for a list of all contributions to it.