Homotopy Type Theory Hausdorff ring > history (changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

Contents

< Hausdorff space

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 RR be a ring and a Hausdorff space. RR is a Hausdorff ring if the ring operations are pointwise continuous…

This is dumb, that the ring operations are pointwise continuous follows from the ring axioms and fact that product Hausdorff spaces exist.

Let II be a directed type and x:IRx:I \to R and y:IRy:I \to R be nets which converges to a:Ra:R and b:Rb:R respectively. By the definition of a function algebra, one could define pointwise the nets 00, x+yx + y, 11, x-x, xyx \cdot y for natural number nn. Let us denote the limit of a net as the partial function

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

RR 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,i0(i)=0p_{0}:\lim_{i:I, i \to \infty} 0(i) = 0
x:IR,y:IR,lim i:I,ix(i):R,lim i:I,iy(i):Rp +(x,y):lim i:I,i(x+y)(i)=lim i:I,ix(i)+lim i:I,iy(i)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:IR,lim i:I,ix(i):Rp (x):lim i:I,i(x)(i)=lim i:I,ix(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,i1(i)=1p_{1}:\lim_{i:I, i \to \infty} 1(i) = 1
x:IR,y:IR,lim i:I,ix(i):R,lim i:I,iy(i):Rp (x,y):lim i:I,i(xy)(i)=lim i:I,ix(i)lim i:I,iy(i)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)

See also

Last revised on June 10, 2022 at 01:40:14. See the history of this page for a list of all contributions to it.