nLab lifting a function

Redirected from "lifts to locators".
Contents

Contents

Idea

In real analysis, the notion of lifting a function from the real numbers \mathbb{R} to some sequentially Cauchy complete pseudometric space \mathbb{R}^\mathcal{L} of real numbers equipped with computational structure. The pseudometric space \mathbb{R}^\mathcal{L} comes with a function π 1: \pi_1:\mathbb{R}^\mathcal{L} \to \mathbb{R} whose image is the Cauchy real numbers. The computational structures which can be used for lifting functions include

Definition

Using locators

Let \mathbb{R} be a sequentially Cauchy complete Archimedean ordered field, and let

x:locator(x)\mathbb{R}^\mathcal{L} \coloneqq \sum_{x:\mathbb{R}} \mathrm{locator}(x)

be the set of all pairs of real numbers and locators, with canonical projection function π 1: \pi_1:\mathbb{R}^\mathcal{L} \to \mathbb{R}. This projection function is not an injection because in general a real number may have more than one locator; however, the image of this projection function is the Cauchy real numbers C\mathbb{R}_C, which is a subset of \mathbb{R} and thus does have an injection into \mathbb{R}. A function f:f:\mathbb{R} \to \mathbb{R} lifts to locators if it comes with a function f : f^\mathcal{L}:\mathbb{R}^\mathcal{L} \to \mathbb{R}^\mathcal{L} such that the following square in Set commutes:

f π 1 π 1 f \array{& \mathbb{R}^\mathcal{L} & \overset{f^\mathcal{L}}\rightarrow & \mathbb{R}^\mathcal{L} & \\ \pi_1 & \downarrow &&\downarrow & \pi_1\\ &\mathbb{R} & \underset{f}\rightarrow& \mathbb{R} & \\ }

Using Cauchy sequences of rational numbers

Let \mathbb{R} be a sequentially Cauchy complete Archimedean ordered field, and let

l: x: ϵ: + N: n:(nN)(|x(n)l|<ϵ)\mathbb{R}^\mathcal{L} \coloneqq \sum_{l:\mathbb{R}} \sum_{x:\mathbb{N} \to \mathbb{Q}} \prod_{\epsilon:\mathbb{Q}_+} \sum_{N:\mathbb{N}} \prod_{n:\mathbb{N}} (n \geq N) \to (\vert x(n) - l \vert \lt \epsilon)

be the set consisting of a real number and a Cauchy sequence of rational numbers constructively converging to the real number, in the sense of the BHK interpretation, with canonical function π 1: \pi_1:\mathbb{R}^\mathcal{L} \to \mathbb{R}. A function f:f:\mathbb{R} \to \mathbb{R} lifts to Cauchy sequences of rational numbers if it comes with a function f : f^\mathcal{L}:\mathbb{R}^\mathcal{L} \to \mathbb{R}^\mathcal{L} such that the following square in Set commutes:

f π 1 π 1 f \array{& \mathbb{R}^\mathcal{L} & \overset{f^\mathcal{L}}\rightarrow & \mathbb{R}^\mathcal{L} & \\ \pi_1 & \downarrow &&\downarrow & \pi_1\\ &\mathbb{R} & \underset{f}\rightarrow& \mathbb{R} & \\ }

Alternatively, one can define the set \mathbb{R}^\mathcal{L} directly as the set of Cauchy sequences of rational numbers, defined constructively using the BHK interpretation

x: ϵ: + N: n: m:(nN)×(mN)(|x(n)x(m)|<ϵ)\mathbb{R}^\mathcal{L} \coloneqq \sum_{x:\mathbb{N} \to \mathbb{Q}} \prod_{\epsilon:\mathbb{Q}_+} \sum_{N:\mathbb{N}} \prod_{n:\mathbb{N}} \prod_{m:\mathbb{N}} (n \geq N) \times (m \geq N) \to (\vert x(n) - x(m) \vert \lt \epsilon)

Quotienting \mathbb{R}^\mathcal{L} by a suitable equivalence relation - there are many different options available used in the constructive analysis literature, yields the Cauchy real numbers C\mathbb{R}_C with a quotient map []: C[-]:\mathbb{R}^\mathcal{L} \to \mathbb{R}_C, and the Cauchy real numbers embed into any sequentially Cauchy complete Archimedean ordered field \mathbb{R}, with unique ring homomorphism η: C\eta:\mathbb{R}_C \to \mathbb{R}, yielding a function λx.η([x]): \lambda x.\eta([x]):\mathbb{R}^\mathcal{L} \to \mathbb{R}. A function f:f:\mathbb{R} \to \mathbb{R} lifts to Cauchy sequences of rational numbers if it comes with a function f : f^\mathcal{L}:\mathbb{R}^\mathcal{L} \to \mathbb{R}^\mathcal{L} such that the following square in Set commutes:

f λx.η([x]) λx.η([x]) f \array{& \mathbb{R}^\mathcal{L} & \overset{f^\mathcal{L}}\rightarrow & \mathbb{R}^\mathcal{L} & \\ \lambda x.\eta([x]) & \downarrow &&\downarrow & \lambda x.\eta([x])\\ &\mathbb{R} & \underset{f}\rightarrow& \mathbb{R} & \\ }

Examples

  • The field operations on \mathbb{R} lifts to locators or Cauchy sequences of rational numbers

  • Hence, any real polynomial function or rational function lifts to locators or Cauchy sequences of rational numbers.

  • Given any convergent sequence of functions f:f:\mathbb{N} \to \mathbb{R} \to \mathbb{R} such that each f nf_n lifts to locators or Cauchy sequences of rational numbers, then the limit function lim nf n\lim_{n \to \infty} f_n lifts to locators or Cauchy sequences of rational numbers, since for each real number x:x:\mathbb{R} equipped with a locator or Cauchy sequence of real numbers, the limit of the pointwise sequence f ()(x)f_{(-)}(x) also comes with a locator or Cauchy sequence of real numbers.

  • Hence, any smooth function or analytic function lifts to locators or Cauchy sequences of rational numbers.

  • The absolute value, minimum and maximum lattice operations, real square root, and more generally real nn-th root partial functions all lift to locators or Cauchy sequences of rational numbers. These (partial) functions aren’t smooth at 00, but can nevertheless be defined as the limit of a convergent sequence of functions.

See also

References

Last revised on July 19, 2024 at 17:04:57. See the history of this page for a list of all contributions to it.