Homotopy Type Theory difference quotient > history (Rev #3)

Contents

Definition

Given a Heyting field FF and a subtype SFS \subseteq F, 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

In a field

Given a function f:SFf:S \to F, the difference quotient q:Δ #(S)Fq:\Delta_{\#}(S) \to F is the partial binary function

q(x,y):=f(x)f(y)xyq(x, y) := \frac{f(x) - f(y)}{x - y}

In a vector space

Given a FF-bimodule VV and a function f:SVf:S \to V, the difference quotient q:Δ #(S)Vq:\Delta_{\#}(S) \to V is the partial binary function

q(x,y):=1xy(f(x)f(y))q(x, y) := \frac{1}{x - y} (f(x) - f(y))

See also

Revision on April 23, 2022 at 19:08:09 by Anonymous?. See the history of this page for a list of all contributions to it.