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

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

Contents

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

Given Let apartialUU binary be function a type such thatq:Δ #(S) T U q:\Delta_{\#}(S) \Delta_{\#}(S) \to \subseteq T U , the and currying of q US×S q U \subseteq S \times S . results As in a the result, dependent for functions everyx:Sx:S, there is a dependent type

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

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

A Given function ag:STg:S \to Tpartial is binary a functionlimit of qq approaching the diagonalq:UTq:U \to T , if the for currying all of x q:S x:S q results in the limit of the dependent function functionsq(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 x ( :Sq(x) : [ ( g y: S U ( F x) x:Slim yxq(x ) ,(y) = )g(x)]T hasLimitApproachingDiagonal(q) x:S \coloneqq \vdash \left[\sum_{g:S q(x): \left(\sum_{y:U(x)} (x,y)\right) \to F} T \prod_{x:S} \lim_{y \to x} q(x)(y) = g(x)\right]

The A type function of all functions inΔ #g ( :S) F T \Delta_{\#}(S) g:S \to F T that have a limit approaching the diagonal is defined a aslimit 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

DiagonalLimitFunc(S,T) q:Δ #(S)ThasLimitApproachingDiagonal(q)[ g:ST x:Slim yxq(x)(y)=g(x)] DiagonalLimitFunc(S, hasLimitApproachingDiagonal(q) T) \coloneqq \sum_{q:\Delta_{\#}(S) \left[\sum_{g:S \to T} hasLimitApproachingDiagonal(q) \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): DiagonalLimitFunc DiagLimFunc(S,T)(SF) \lim_{(x, y) \to (x, x)} (-)(x, y): DiagonalLimitFunc(S, DiagLimFunc(S, T) \to (S \to F)

which returns the limit of a partial binary function q: DiagonalLimitFunc DiagLimFunc(S,T)(Δ #(S)T) q:DiagonalLimitFunc(S, q:DiagLimFunc(S, T) \subseteq (\Delta_{\#}(S) \to T) approaching the diagonal and thus satisfies the equationalgebraic limit theorems

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 a calculus 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 April 16, 2022 at 14:59:12 by Anonymous?. See the history of this page for a list of all contributions to it.