Homotopy Type Theory
algebraic limit field > history (Rev #9, changes)
Showing changes from revision #8 to #9:
Added | Removed | Changed
Contents
Idea
A field with a notion of a limit of a function that satisfy the algebraic limit theorems.
Definition
Let F F be a Heyting field and a function limit space , where x − 1 x^{-1} is another notation for 1 x \frac{1}{x} . F F is a algebraic limit field if the algebraic limit theorems are satisfied, i.e. if the limit preserves the ring operations:
z : ∏ c : S ( lim x → c 0 ( x ) = 0 ) z:\prod_{c:S} \left(\lim_{x \to c} 0(x) = 0\right) a : ∏ c : S ∏ f : FuncWithLim ( S , F ) ( c ) ∏ g : FuncWithLim ( S , F ) ( c ) ( lim x → c f ( x ) + g ( x ) = lim x → c f ( x ) + lim x → c g ( x ) ) a:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{g:FuncWithLim(S, F)(c)} \left(\lim_{x \to c} f(x) + g(x) = \lim_{x \to c} f(x) + \lim_{x \to c} g(x)\right) n : ∏ c : S ∏ f : FuncWithLim ( S , F ) ( c ) ( lim x → c − f ( x ) = − lim x → c f ( x ) ) n:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \left(\lim_{x \to c} -f(x) = -\lim_{x \to c} f(x) \right) s : ∏ c : S ∏ f : FuncWithLim ( S , F ) ( c ) ∏ g : FuncWithLim ( S , F ) ( c ) ( lim x → c f ( x ) − g ( x ) = lim x → c f ( x ) − lim x → c g ( x ) ) s:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{g:FuncWithLim(S, F)(c)} \left(\lim_{x \to c} f(x) - g(x) = \lim_{x \to c} f(x) - \lim_{x \to c} g(x)\right) α : ∏ c : S ∏ f : FuncWithLim ( S , F ) ( c ) ∏ a : ℤ ( lim x → c a f ( x ) = a ( lim x → c f ( x ) ) ) \alpha:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{a:\mathbb{Z}} \left(\lim_{x \to c} a f(x) = a \left(\lim_{x \to c} f(x)\right) \right) α : ∏ c : S ∏ f : FuncWithLim ( S , F ) ( c ) ∏ a : S ( lim x → c a f ( x ) = a ( lim x → c f ( x ) ) ) \alpha:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{a:S} \left(\lim_{x \to c} a f(x) = a \left(\lim_{x \to c} f(x)\right) \right) o : ∏ c : S ( lim x → c 1 ( x ) = 1 ) o:\prod_{c:S} \left(\lim_{x \to c} 1(x) = 1\right) m : ∏ c : S ∏ f : FuncWithLim ( S , F ) ( c ) ∏ g : FuncWithLim ( S , F ) ( c ) ( lim x → c f ( x ) ⋅ g ( x ) = lim x → c f ( x ) ⋅ lim x → c g ( x ) ) m:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{g:FuncWithLim(S, F)(c)} \left(\lim_{x \to c} f(x) \cdot g(x) = \lim_{x \to c} f(x) \cdot \lim_{x \to c} g(x)\right) p : ∏ c : S ∏ f : FuncWithLim ( S , F ) ( c ) ∏ n : ℕ ( lim x → c f ( x ) n = ( lim x → c f ( x ) ) n ) p:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{n:\mathbb{N}} \left(\lim_{x \to c} {f(x)}^n = {\left(\lim_{x \to c} f(x)\right)}^n \right)
and the field operations:
r : ∏ c : S ∏ f : FuncWithLim ( S , F ) ( c ) ( ( lim x → c g ( x ) ) # 0 ) → ( lim x → c f ( x ) − 1 = ( lim x → c f ( x ) ) − 1 ) r:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \left(\left(\lim_{x \to c} g(x)\right) \# 0\right) \to \left(\lim_{x \to c} {f(x)}^{-1} = {\left(\lim_{x \to c} f(x)\right)}^{-1}\right) i : ∏ c : S ∏ f : FuncWithLim ( S , F ) ( c ) ( ( lim x → c x ) # 0 ) → ( lim x → c f ( x ) ⋅ f ( x ) − 1 = 1 ) i:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{x \to c} f(x) \cdot {f(x)}^{-1} = 1\right)
See also
Revision on June 10, 2022 at 17:40:55 by
Anonymous? .
See the history of this page for a list of all contributions to it.