Homotopy Type Theory limit of a binary function approaching a diagonal > history (Rev #5, changes)

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

Contents

< limit of a binary function approaching a diagonal

Definition

Let TT be a function limit space with a tight apartness relation #\# and let STS \subseteq T be a subtype of TT. Let us define the subtype Δ #(S)S×S\Delta_{\#}(S) \subseteq S \times S of pairs of elements apart from the diagonal as

Δ #(S) (x,y):S×Sx#y\Delta_{\#}(S) \coloneqq \sum_{(x,y):S \times S} x \# y

Let UU be a type such that Δ #(S)U\Delta_{\#}(S) \subseteq U and US×SU \subseteq S \times S. As a result, for every x:Sx:S, there is a dependent type

U(x) y:S(x,y)U(x) \coloneqq \sum_{y:S} (x, y)

Given a partial binary function q:UTq:U \to T, the currying of qq results in the dependent functions

x:Sq(x):( y:U(x)(x,y))Tx:S \vdash q(x): \left(\sum_{y:U(x)} (x,y)\right) \to T

A function g:STg:S \to T is a limit of qq approaching the diagonal if for all x:Sx:S the limit of the dependent function q(x)q(x) approaching xx is g(x)g(x). We can define a predicate that the qq has a limit approaching the diagonal as

hasLimitApproachingDiagonal(q)[ g:ST x:Slim yxq(x)(y)=g(x)]hasLimitApproachingDiagonal(q) \coloneqq \left[\sum_{g:S \to T} \prod_{x:S} \lim_{y \to x} q(x)(y) = g(x)\right]

The type of all functions in UTU \to T that have a limit approaching the diagonal is defined as

DiagLimFunc(S,T) q:UThasLimitApproachingDiagonal(q)DiagLimFunc(S, T) \coloneqq \sum_{q:U \to T} hasLimitApproachingDiagonal(q)

As a result, there exists a function

lim (x,y)(x,x)()(x,y):DiagLimFunc(S,T)(SF)\lim_{(x, y) \to (x, x)} (-)(x, y): DiagLimFunc(S, T) \to (S \to F)

which returns the limit of a partial binary function q:DiagLimFunc(S,T)q:DiagLimFunc(S, T) approaching the diagonal and thus satisfies the equation

x:Slim yxq(x)(y)=lim (x,y)(x,x)q(x,y)\prod_{x:S} \lim_{y \to x} q(x)(y) = \lim_{(x, y) \to (x, x)} q(x, y)

Properties

In an algebraic limit field FF, the algebraic limit theorems are satisfied:

Limits preserve the zero function

x:Slim (x,y)(x,x)0(x,y)=lim yx0(x)(y)\prod_{x:S} \lim_{(x, y) \to (x, x)} 0(x, y) = \lim_{y \to x} 0(x)(y)
x:Slim (x,y)(x,x)0(x,y)=0\prod_{x:S} \lim_{(x, y) \to (x, x)} 0(x, y) = 0
x:Slim (x,y)(x,x)0(x,y)=0(x,x)\prod_{x:S} \lim_{(x, y) \to (x, x)} 0(x, y) = 0(x, x)

Limits preserve addition of functions

x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)+g(x,y)=lim (x,y)(x,x)(f+g)(x,y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{(x, y) \to (x, x)} (f + g)(x, y)
x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)+g(x,y)=lim yx(f+g)(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{y \to x} (f + g)(x)(y)
x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)+g(x,y)=lim yxf(x)(y)+g(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{y \to x} f(x)(y) + g(x)(y)
x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)+g(x,y)=lim yxf(x)(y)+lim yxg(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{y \to x} f(x)(y) + \lim_{y \to x} g(x)(y)
x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)+g(x,y)=lim (x,y)(x,x)f(x,y)+lim (x,y)(x,x)g(x,y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{(x, y) \to (x, x)} f(x, y) + \lim_{(x, y) \to (x, x)} g(x, y)

Limits preserve negation of functions

x:S f:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)=lim yxf(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} -f(x, y) = \lim_{y \to x} -f(x)(y)
x:S f:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)=lim yxf(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} -f(x, y) = -\lim_{y \to x} f(x)(y)
x:S f:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)=lim (x,y)(x,x)f(x,y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} -f(x, y) = -\lim_{(x, y) \to (x, x)} f(x, y)

Limits preserve subtraction of functions

x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)g(x,y)=lim (x,y)(x,x)(fg)(x,y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{(x, y) \to (x, x)} (f - g)(x, y)
x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)g(x,y)=lim yx(fg)(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{y \to x} (f - g)(x)(y)
x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)g(x,y)=lim yxf(x)(y)g(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{y \to x} f(x)(y) - g(x)(y)
x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)g(x,y)=lim yxf(x)(y)lim yxg(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{y \to x} f(x)(y) - \lim_{y \to x} g(x)(y)
x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)g(x,y)=lim (x,y)(x,x)f(x,y)lim (x,y)(x,x)g(x,y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{(x, y) \to (x, x)} f(x, y) - \lim_{(x, y) \to (x, x)} g(x, y)

Limits preserve the left multiplicative \mathbb{Z}-action of functions

x:S f:DiagLimFunc(S,F) n:lim (x,y)(x,x)nf(x,y)=lim (x,y)(x,x)(nf)(x,y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = \lim_{(x, y) \to (x, x)} (n f)(x, y)
x:S f:DiagLimFunc(S,F) n:lim (x,y)(x,x)nf(x,y)=lim yx(nf)(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = \lim_{y \to x} (n f)(x)(y)
x:S f:DiagLimFunc(S,F) n:lim (x,y)(x,x)nf(x,y)=lim yxnf(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = \lim_{y \to x} n f(x)(y)
x:S f:DiagLimFunc(S,F) n:lim (x,y)(x,x)nf(x,y)=nlim yxf(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = n \lim_{y \to x} f(x)(y)
x:S f:DiagLimFunc(S,F) n:lim (x,y)(x,x)nf(x,y)=nlim (x,y)(x,x)f(x,y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = n \lim_{(x, y) \to (x, x)} f(x, y)

Limits preserve multiplication of functions by scalars

x:S f:DiagLimFunc(S,F) a:Flim (x,y)(x,x)af(x,y)=lim (x,y)(x,x)(af)(x,y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:F} \lim_{(x, y) \to (x, x)} a f(x, y) = \lim_{(x, y) \to (x, x)} (a f)(x, y)
x:S f:DiagLimFunc(S,F) a:Flim (x,y)(x,x)af(x,y)=lim yx(af)(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:F} \lim_{(x, y) \to (x, x)} a f(x, y) = \lim_{y \to x} (a f)(x)(y)
x:S f:DiagLimFunc(S,F) a:flim (x,y)(x,x)af(x,y)=lim yxaf(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:f} \lim_{(x, y) \to (x, x)} a f(x, y) = \lim_{y \to x} a f(x)(y)
x:S f:DiagLimFunc(S,F) a:Flim (x,y)(x,x)af(x,y)=alim yxf(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:F} \lim_{(x, y) \to (x, x)} a f(x, y) = a \lim_{y \to x} f(x)(y)
x:S f:DiagLimFunc(S,F) a:Flim (x,y)(x,x)af(x,y)=alim (x,y)(x,x)f(x,y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:F} \lim_{(x, y) \to (x, x)} a f(x, y) = a \lim_{(x, y) \to (x, x)} f(x, y)

Limits preserve the one function

x:Slim (x,y)(x,x)1(x,y)=lim yx1(x)(y)\prod_{x:S} \lim_{(x, y) \to (x, x)} 1(x, y) = \lim_{y \to x} 1(x)(y)
x:Slim (x,y)(x,x)1(x,y)=1\prod_{x:S} \lim_{(x, y) \to (x, x)} 1(x, y) = 1
x:Slim (x,y)(x,x)1(x,y)=1(x,x)\prod_{x:S} \lim_{(x, y) \to (x, x)} 1(x, y) = 1(x, x)

Limits preserve multiplication of functions

x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)g(x,y)=lim (x,y)(x,x)(fg)(x,y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{(x, y) \to (x, x)} (f \cdot g)(x, y)
x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)g(x,y)=lim yx(fg)(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{y \to x} (f \cdot g)(x)(y)
x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)g(x,y)=lim yxf(x)(y)g(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{y \to x} f(x)(y) \cdot g(x)(y)
x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)g(x,y)=lim yxf(x)(y)lim yxg(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{y \to x} f(x)(y) \cdot \lim_{y \to x} g(x)(y)
x:S f:DiagLimFunc(S,F) g:DiagLimFunc(S,F)lim (x,y)(x,x)f(x,y)g(x,y)=lim (x,y)(x,x)f(x,y)lim (x,y)(x,x)g(x,y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{(x, y) \to (x, x)} f(x, y) \cdot \lim_{(x, y) \to (x, x)} g(x, y)

Limits preserve powers of functions

x:S f:DiagLimFunc(S,F) n:lim (x,y)(x,x)f(x,y) n=lim (x,y)(x,x)(f n)(x,y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \lim_{(x, y) \to (x, x)} (f^n)(x, y)
x:S f:DiagLimFunc(S,F) n:lim (x,y)(x,x)f(x,y) n=lim yx(f n)(x)(y)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \lim_{y \to x} (f^n)(x)(y)
x:S f:DiagLimFunc(S,F) n:lim (x,y)(x,x)f(x,y) n=lim yx(f(x)(y)) n\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \lim_{y \to x} (f(x)(y))^n
x:S f:DiagLimFunc(S,F) n:lim (x,y)(x,x)f(x,y) n=(lim yxf(x)(y)) n\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \left(\lim_{y \to x} f(x)(y)\right)^n
x:S f:DiagLimFunc(S,F) n:lim (x,y)(x,x)f(x,y) n=(lim (x,y)(x,x)f(x,y)) n\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \left(\lim_{(x, y) \to (x, x)} f(x, y)\right)^n

Limits preserve reciprocals of functions

Where x 1x^{-1} is another notation for 1x\frac{1}{x}

x:S f:DiagLimFunc(S,F) n:(lim (x,y)(x,x)f(x,y)#0)(lim (x,y)(x,x)f(x,y) 1=lim (x,y)(x,x)(f 1)(x,y))\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \lim_{(x, y) \to (x, x)} (f^{-1})(x, y)\right)
x:S f:DiagLimFunc(S,F) n:(lim (x,y)(x,x)f(x,y)#0)(lim (x,y)(x,x)f(x,y) 1=lim yx(f 1)(x)(y))\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \lim_{y \to x} (f^{-1})(x)(y)\right)
x:S f:DiagLimFunc(S,F) n:(lim (x,y)(x,x)f(x,y)#0)(lim (x,y)(x,x)f(x,y) 1=lim yx(f(x)(y)) 1)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \lim_{y \to x} (f(x)(y))^{-1}\right)
x:S f:DiagLimFunc(S,F) n:(lim (x,y)(x,x)f(x,y)#0)(lim (x,y)(x,x)f(x,y) 1=(lim yxf(x)(y)) 1)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \left(\lim_{y \to x} f(x)(y)\right)^{-1}\right)
x:S f:DiagLimFunc(S,F) n:(lim (x,y)(x,x)f(x,y)#0)(lim (x,y)(x,x)f(x,y) 1=(lim (x,y)(x,x)f(x,y)) 1)\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \left(\lim_{(x, y) \to (x, x)} f(x, y)\right)^{-1}\right)

Limits preserve that the reciprocals of functions are multiplicative inverses

Where x 1x^{-1} is another notation for 1x\frac{1}{x}

x:S((lim xcx)#0)(lim (x,y)(x,x)f(x,y)f(x,y) 1=lim (x,y)(x,x)(ff 1)(x,y))\prod_{x:S} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y) \cdot {f(x, y)}^{-1} = \lim_{(x, y) \to (x, x)} (f \cdot f^{-1})(x, y)\right)
x:S((lim xcx)#0)(lim (x,y)(x,x)f(x,y)f(x,y) 1=lim yx(ff 1)(x)(y))\prod_{x:S} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y) \cdot {f(x, y)}^{-1} = \lim_{y \to x} (f \cdot f^{-1})(x)(y)\right)
x:S((lim xcx)#0)(lim (x,y)(x,x)f(x,y)f(x,y) 1=lim yxf(x)(y)f(x)(y) 1)\prod_{x:S} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y) \cdot {f(x, y)}^{-1} = \lim_{y \to x} f(x)(y) \cdot {f(x)(y)}^{-1}\right)
x:S((lim xcx)#0)(lim (x,y)(x,x)f(x,y)f(x,y) 1=1)\prod_{x:S} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y) \cdot {f(x, y)}^{-1} = 1\right)

See also

Revision on June 10, 2022 at 13:44:53 by Anonymous?. See the history of this page for a list of all contributions to it.