Invariance of domain #
This file contains the completed invariance-of-domain portion of Kai Lam's development in
mathlib4 PR #36770, adapted from
commit 230d75acb32d80e7d7c4f4cd028b139f3dc28be7. It proves invariance of domain for
finite-dimensional real inner product spaces, conditional on Brouwer's fixed-point theorem for the
closed unit ball.
The chart-independence layer is adapted from Steven Sivek's
TopologicalManifolds development at commit
05f80330d5a41b05376ae90eb8aa32c0166721db. It packages invariance of domain as a reusable
topological typeclass and applies it to the interior and boundary strata of charted spaces.
The proof follows Terry Tao's exposition, using the Tietze extension theorem, Stone-Weierstrass approximation, and a measure-theoretic perturbation argument.
Main declarations #
BrouwerFixedPoint: the required fixed-point principle for the closed unit ball.differentiable_approx_of_continuous: differentiable approximation on compact sets.stability_of_zero: stability of a zero under a bounded perturbation.invariance_of_domain_interior: the closed-ball form of invariance of domain.invariance_of_domain_open_map: the open-set form of invariance of domain.invariance_of_domain_partial_equiv: the neighbourhood form for partial equivalences.HasInvarianceOfDomain: a reusable topological form of invariance of domain.isInteriorPoint_iff_any_chart: chart independence of interior points.isBoundaryPoint_iff_any_chart: chart independence of boundary points.
Reference #
- Terry Tao, "Brouwer's fixed point and invariance of domain theorems, and Hilbert's fifth problem", 2011.
BrouwerFixedPoint E is a typeclass asserting that the Brouwer fixed point theorem holds for
the closed unit ball in the inner product space E. That is: for every continuous map
f : closedBall 0 1 → closedBall 0 1, there exists x such that f x = x.
This is assumed and used to prove invariance of domain.
- brouwer_fixed_point (f : ↑(Metric.closedBall 0 1) → ↑(Metric.closedBall 0 1)) (hf : Continuous f) : ∃ (x : ↑(Metric.closedBall 0 1)), f x = x
Instances
On a compact set, any continuous map can be uniformly approximated by a differentiable map.
Stability of zero (Lemma 6). If G is a left inverse of f on the closed ball,
and Gtilde is a continuous function on f(Bⁿ) with ‖G - Gtilde‖ ≤ 1 pointwise,
then Gtilde has a zero in f(Bⁿ).
Let B^n be the closed unit ball (closedBall 0 1).
Let f : B^n → ℝ^n be an continuous injective map.
Then f(0) lies in the interior of f(B^n).
The invariance of domain theorem: if U ⊆ E is open,
f : E → E is continuous on U and injective on U, then the image f '' U is open in E.
If f is a partial equivalence continuous on its source, then it maps
neighbourhoods of x (contained in the source) to neighbourhoods of f(x).
A topological space has invariance of domain if each continuous partial equivalence maps neighbourhoods contained in its source to neighbourhoods of the corresponding image point.
- invariance_of_domain {x : X} {s : Set X} {f : PartialEquiv X X} (hCont : ContinuousOn (↑f) f.source) : s ∈ nhds x → s ⊆ f.source → ↑f '' s ∈ nhds (↑f x)
Instances
Apply a HasInvarianceOfDomain instance to a continuous partial equivalence.
Brouwer's fixed-point theorem supplies invariance of domain in a finite-dimensional real inner product space.
If some OpenPartialHomeomorph M H sends a point to the interior of range I, then
so does any other OpenPartialHomeomorph M H.
A point lies in the interior of M iff any OpenPartialHomeomorph M H
sends it to the interior of range I.
A point lies on the boundary of M iff any OpenPartialHomeomorph M H
sends it to the frontier of range I.
An embedded open part of the model vector space has open image in a manifold modeled on
I. This is the manifold-with-boundary form of invariance of domain needed at an interior
edge of an embedded finite triangle complex.
The use of the extended target chart is important: if the image point were on the manifold
boundary, invariance of domain would produce an ambient vector-space neighborhood contained in
range I, which is impossible there.
Embedding-form wrapper for
isOpen_range_of_isOpen_of_continuous_injective.
At an interior point of the ambient manifold, re-embedding a fixed source cannot turn the corresponding local sheet into a boundary point of the new image.
This is deliberately an interior-point statement. It is false at a manifold-boundary point: an embedding of a half-plane may bend its boundary into the ambient interior.