Homotopy Type Theory Hausdorff ring > history (Rev #1)

Idea
Definition
See also

Idea

Limits in the real numbers satisfy certain algebraic properties, while the usual notion of convergence space, Hausdorff space, and topological space are purely analytic.

Definition

Let $R$ be a ring and a Hausdorff space.

Let $I$ be a directed type and $x:I \to R$ and $y:I \to R$ be nets which converges to $a:R$ and $b:R$ respectively. By the definition of a function algebra, one could define pointwise the nets $0$ , $x + y$ , $1$ , $-x$ , $x \cdot y$ for natural number $n$ . Let us denote the limit of a net as the partial function

\lim_{i:I, i \to \infty} (-)(i): (I \to R) \to R

$R$ is a Hausdorff ring if the limit of a net partial function preserves the ring operations, provided the limit exists:

p_{0}:\lim_{i:I, i \to \infty} 0(i) = 0

x: I\to R, y:I \to R, \lim_{i:I, i \to \infty} x(i):R, \lim_{i:I, i \to \infty} y(i):R \vdash p_{+}(x, y):\lim_{i:I, i \to \infty} (x + y)(i) = \lim_{i:I, i \to \infty} x(i) + \lim_{i:I, i \to \infty} y(i)

x: I\to R, \lim_{i:I, i \to \infty} x(i):R \vdash p_{-}(x):\lim_{i:I, i \to \infty} (-x)(i) = -\lim_{i:I, i \to \infty} x(i)

p_{1}:\lim_{i:I, i \to \infty} 1(i) = 1

x: I\to R, y:I \to R, \lim_{i:I, i \to \infty} x(i):R, \lim_{i:I, i \to \infty} y(i):R \vdash p_{\cdot}(x, y):\lim_{i:I, i \to \infty} (x \cdot y)(i) = \lim_{i:I, i \to \infty} x(i) \cdot \lim_{i:I, i \to \infty} y(i)

Homotopy Type Theory Hausdorff ring > history (Rev #1)

Contents

Idea

Definition

See also