analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
synthetic differential geometry
Introductions
from point-set topology to differentiable manifolds
geometry of physics: coordinate systems, smooth spaces, manifolds, smooth homotopy types, supergeometry
Differentials
Tangency
The magic algebraic facts
Theorems
Axiomatics
(shape modality $\dashv$ flat modality $\dashv$ sharp modality)
$(\esh \dashv \flat \dashv \sharp )$
dR-shape modality$\dashv$ dR-flat modality
$\esh_{dR} \dashv \flat_{dR}$
(reduction modality $\dashv$ infinitesimal shape modality $\dashv$ infinitesimal flat modality)
$(\Re \dashv \Im \dashv \&)$
fermionic modality$\dashv$ bosonic modality $\dashv$ rheonomy modality
$(\rightrightarrows \dashv \rightsquigarrow \dashv Rh)$
Models
Models for Smooth Infinitesimal Analysis
smooth algebra ($C^\infty$-ring)
differential equations, variational calculus
Chern-Weil theory, ∞-Chern-Weil theory
Cartan geometry (super, higher)
The inverse function theorem says that given any sequentially Cauchy complete Archimedean field $\mathbb{R}$ and a continuously differentiable function $f:I \to \mathbb{R}$ from an open interval $I \subseteq \mathbb{R}$ such that for all points $a \in I$,
the inverse function $f^{-1}:\mathrm{im}(f) \to \mathbb{R}$ exists and is unique and is defined by the first-order nonlinear ordinary differential equation
with initial condition $f^{-1}(f(a)) = a$. Classically, $\mathbb{R}$ is essentially unique, but constructively, there are multiple inequivalent sequentially Cauchy complete Archimedean fields.
To be done…
This proof is adapted from the Wikipedia article on the inverse function theorem, in the section “A proof using the contraction mapping principle”, the contraction mapping principle being another name for the Banach fixed-point theorem.
Let $(-r, r)$ denote an open interval in $\mathbb{R}$ with radius $r$ and centre $0$. If $g:(-r, r) \to \mathbb{R}$ is a map such that $g(0) = 0$ and there exists a rational constant $0 \lt c \lt 1$ such that $\vert g(y) - g(x) \vert = c \vert y - x \vert$ for all $x \in (-r, r)$ and $y \in (-r, r)$, then $f = \mathrm{id}_\mathbb{R} + g$ is injective on $(-r, r)$ and
where $\mathrm{id}_\mathbb{R}$ is the identity map on the real numbers, restricted in the domain to $(-r, r)$, and given an open interval $I \subseteq \mathbb{R}$, $f(I)$ is the image of $f$ under $I$.
First, the map $f$ is injective on $(-r, r)$, since if $f(x) = f(y)$, then $g(y) - g(x) = x - y$ and so $\vert g(y) - g(x) \vert = \vert y - x \vert$, which is a contradiction unless $y = x$. Next we show
The idea is to note that this is equivalent to, given a point $y$ in $(-(1-c) r, (1-c) r)$, find a fixed point of the map
defined as $F(x) = y - g(x)$ where $0 \lt r' \lt r$ such that $\vert y \vert \leq (1-c)r'$ and the bar means a closed ball. To find a fixed point, we use the Banach fixed-point theorem and checking that $F$ is a well-defined strict-contraction mapping is straightforward. Finally, we have:
since
Now that we have established the lemma, we could proved the main theorem:
It is enough to prove the special case when $a = 0, b = f(a) = 0$ and $f'(0) = \mathrm{id}_\mathbb{R}$. Let $g = f - \mathrm{id}_\mathbb{R}$. The mean value theorem applied to $t \mapsto g(x + t(y - x))$ says:
Since $g'(0) = \mathrm{id}_\mathbb{R} - \mathrm{id}_\mathbb{R} = 0$ and $g'$ is continuous, we can find an $r \gt 0$ such that
for all $x, y$ in $(-r, r)$. Then the earlier lemma says that $f = g + \mathrm{id}_\mathbb{R}$ is injective on $(-r, r)$ and $(-r/2, r/2) \subset (-r, r)$. Then
is bijective and thus has the inverse, where given an open interval $I \subseteq \mathbb{R}$, $f^{-1}(I)$ is the inverse image of $f$ over $I$.
to be continued…
The given proof of the inverse function theorem above relies on the mean value theorem, which in constructive mathematics is only true for uniformly differentiable functions. There might be other proofs which might not rely on the mean value theorem and could prove the inverse function theorem for continuously differentiable functions.
While continuously differentiable functions and locally uniformly differentiable functions are well-defined in every Archimedean ordered field, the inverse function theorem does not hold in all Archimedean ordered fields. One could instead consider adding the inverse function theorem as an axiom to an arbitrary Archimedean ordered field $R$. There are a few axioms which could be used here
For any Archimedean ordered field $R$, the continuously differentiable inverse function axiom for $R$ states that given any differentiable function $f:I \to R$ on an open subinterval $I \subseteq R$ such that its derivative $\frac{d f}{d x}:I \to R$ is pointwise continuous and always apart from zero, there is a unique differentiable function $f^{-1}:\mathrm{im}(f) \to R$ called the inverse function with pointwise continuous derivative $\frac{d f^{-1}}{d x}:\mathrm{im}(f) \to R$ such that $f^{-1}(f(a)) = a$ and for all elements $a \in \mathrm{im}(f)$ and
For any Archimedean ordered field $R$, the locally uniformly differentiable inverse function axiom for $R$ states that given any differentiable function $f:I \to R$ on an open subinterval $I \subseteq R$ such that its derivative $\frac{d f}{d x}:I \to R$ is locally uniformly continuous and always apart from zero, there is a unique differentiable function $f^{-1}:\mathrm{im}(f) \to R$ called the inverse function with locally uniformly continuous derivative $\frac{d f^{-1}}{d x}:\mathrm{im}(f) \to R$ such that $f^{-1}(f(a)) = a$ and for all elements $a \in \mathrm{im}(f)$ and
The former is stronger than the latter, although they are equivalent in the presence of excluded middle. If $R$ satisfies the locally uniformly continuous inverse function axiom, then $R$ is a real closed field.
There is also a third possible axiom in dependent type theory, which uses the shape modality. Given an Archimedean ordered field $R$, let $\esh \coloneqq L_R$ be the shape modality, the localization at $R$. A type $T$ is shapewise contractible if its shape is contractible. Given an open interval $I \subseteq R$, a function $f:I \to R$ is shapewise continuous if the graph of $f$, the set of all pairs $(x, y)$ in $I \times R$ such that $y = f(x)$, is shapewise contractible:
See also:
Last revised on December 14, 2022 at 18:22:29. See the history of this page for a list of all contributions to it.