Piecewise-linear maps between real topological vector spaces #
A map is piecewise linear — PL, and piecewise affine would be the more honest word — when it
is affine on each cell of a polyhedral decomposition of its domain. This file builds that
predicate in the shape the PL structure groupoid needs, and proves the closure properties which
make it a Pregroupoid property: restriction to a subset, locality, invariance under changing the
map off the set, and closure under composition.
The shape of the definition #
Two predicates are defined, one on top of the other.
TauCeti.IsPiecewiseAffineOn f Vsays thatVis covered by finitely many convex polyhedra (TauCeti.IsConvexPolyhedron) on each of whichfagrees with a continuous affine map. This is the concrete, cell-by-cell notion.TauCeti.IsPLOn f ssays that every point ofshas a neighbourhood inson whichfis piecewise affine in the previous sense. This is the predicate the groupoid uses.
Both weakenings of the textbook notion of a polyhedral subdivision are deliberate, and are what
make the predicate usable as a Pregroupoid property on open subsets of a model space.
The cells are asked only to cover the set, not to be contained in it. A non-closed open subset of
a model space cannot be a locally finite union of the closed polyhedra used here, so a locally
finite subdivision of the set would not exist for the sets the groupoid quantifies over. The
covering form restricts to subsets for free (TauCeti.IsPiecewiseAffineOn.mono).
Finiteness is asked for only near each point. A piecewise-linear map may genuinely have infinitely
many pieces — a breakpoint at every integer, say — so a globally finite decomposition is not a
local condition, and Pregroupoid.locality demands one. Local finiteness is the textbook remedy,
and it implies the present predicate: a family that is locally finite along the set is, by
definition, finite on a small enough neighbourhood of each of the set's points.
TauCeti.isPLOn_of_locallyFinite records that implication, in this direction only — no converse
is proved, and none is claimed — and it is the bridge from a triangulation, which supplies exactly
such a family of affine pieces.
Main definitions #
TauCeti.IsPiecewiseAffineOn: a finite polyhedral decomposition on whose cells the map is affine.TauCeti.IsPLOn: the localisation of the previous predicate, the piecewise-linear property.TauCeti.IsPLWithinAt: its germ at a point, the property lifted to charted spaces inTauCeti.Geometry.Manifold.PLGroupoid.Mapto define PL maps between PL manifolds.
Main results #
TauCeti.isPiecewiseAffineOn_of_finiteandTauCeti.isPLOn_of_locallyFinite: the two constructors, from a cover indexed by an arbitrary finite type and from one that is locally finite along the set.TauCeti.IsPLOn.continuousOn: a piecewise-linear map is continuous. This is the "PL implies Top" content; the cells are closed and locally finite in number, so continuity is a pasting argument.TauCeti.IsPLOn.mono,TauCeti.IsPLOn.congr,TauCeti.isPLOn_of_locally,TauCeti.IsPLOn.comp: the four closure properties aPregroupoidproperty must have.TauCeti.isPLOn_iff_forall_isPLWithinAt,TauCeti.isPLWithinAt_inter,TauCeti.IsPLWithinAt.congr,TauCeti.IsPLWithinAt.comp: the germ form and the closure properties which make it a local invariant property of charted spaces.ContinuousAffineMap.isPLOn_affineGraph: the graph of a continuous affine map is piecewise affine on every subset of its domain.TauCeti.IsPLOn.exists_eqOn_Icc: a piecewise-linear map of the line is affine on each side of every point of the interior of its domain.TauCeti.IsPLOn.exists_image_Icc_eq_affineSegment: near each point, an injective piecewise-linear curve is two segments from the image of the point, meeting only there.TauCeti.isPLOn_absandTauCeti.not_exists_continuousAffineMap_eq_abs: the absolute value is piecewise linear and is not affine, so the predicate is strictly weaker than affineness.
This is part of the structure-group track of layer 1 of the geometric-topology roadmap
(TauCetiRoadmap/GeometricTopology/README.md); the groupoid built from it lives in
TauCeti/Geometry/Manifold/PLGroupoid/Basic.lean.
IsPiecewiseAffineOn f V says that the set V is covered by finitely many convex polyhedra
on each of which the map f agrees with a continuous affine map.
Instances For
The finite polyhedral decomposition characterizing piecewise affineness.
The constructor of TauCeti.IsPiecewiseAffineOn for a cover indexed by an arbitrary finite
type, rather than by Fin n.
A continuous affine map is piecewise affine on every set, with the whole space as its single cell.
Piecewise affineness passes to subsets: the same cells and affine pieces work.
Piecewise affineness only depends on the values of the map on the set.
A piecewise affine map is continuous on the set carrying the decomposition.
The cells are closed and finite in number, so this is a pasting argument: the neighbourhood filter of a point within the set is the supremum of its neighbourhood filters within the cells, the filters attached to cells missing the point are trivial because the cells are closed, and on the remaining cells the map agrees with a continuous affine map.
Piecewise affine maps compose: refine the cells of the source decomposition by pulling the cells of the target decomposition back along the affine pieces.
No continuity is needed here, because the refined cover is honest: the affine piece of f on a
source cell agrees with f there, so it lands in the same target cell that f does.
IsPLOn f s says that the map f is piecewise linear on the set s: every point of s
has a neighbourhood in s covered by finitely many convex polyhedra on each of which f agrees
with a continuous affine map.
Instances For
The local finite-decomposition characterization of piecewise linearity.
A piecewise affine map is piecewise linear on the set carrying its decomposition.
A continuous affine map is piecewise linear on every set.
The graph of a continuous affine map is piecewise affine on every subset of its domain.
The identity is piecewise linear on every set.
The piecewise-linear property passes to subsets.
The piecewise-linear property only depends on the values of the map on the set.
A piecewise-linear map is continuous.
The piecewise-linear property is local: it suffices to have it on a neighbourhood in s of
each point of s.
The piecewise-linear property is local, in the form the Pregroupoid locality axiom asks
for: it suffices to have it on the trace of an open neighbourhood of each point of s.
Piecewise-linear maps compose.
Continuity of f (TauCeti.IsPLOn.continuousOn) enters here, and only here: it is what shrinks
the neighbourhood of x on which f is piecewise affine to one that f carries into the
neighbourhood of f x on which g is piecewise affine.
Piecewise linearity at a point #
The germ form of TauCeti.IsPLOn, as ContDiffWithinAt is to ContDiffOn: f is piecewise
affine on a neighbourhood of x within insert x s. Asking for insert x s rather than s pins
down the value of f at x even when x ∉ s, which is what the lift of the property to charted
spaces needs (TauCeti.PLWithinAtProp).
IsPLWithinAt f s x says that f is piecewise affine on a neighbourhood of x within
insert x s.
Instances For
Piecewise linearity at a point, unfolded: a piecewise affine neighbourhood of x within s
which contains x.
Piecewise linearity within the whole space at a point: a piecewise affine neighbourhood.
A map piecewise linear on s is piecewise linear within s at each point of s.
Piecewise linearity on a set is piecewise linearity within the set at each of its points.
A continuous affine map is piecewise linear within every set at every point.
A map piecewise linear within s at x is continuous within insert x s at x.
A map piecewise linear within s at x is continuous within s at x.
Piecewise linearity within s at x passes to any set t of which s is a neighbourhood
within at x.
Piecewise linearity within a set at a point passes to subsets.
Piecewise linearity within s at x is unchanged by intersecting s with a neighbourhood
of x.
Piecewise linearity within s at x only depends on the values of the map on s and at
x.
Maps piecewise linear at a point compose.
Continuous affine extension and restriction transport PL maps to the image of a set. Only the domain restriction must undo its extension; the codomain map may be arbitrary.
PL regularity is preserved and reflected by continuous affine extensions with left inverses on the set and its image under the map under consideration.
A polyhedral cover of s on whose cells f is affine and which is locally finite along s
— every point of s has a neighbourhood meeting only finitely many cells — makes f piecewise
linear on s. This is the bridge from a triangulation, which supplies exactly such a cover; the
implication runs in this direction only, and no converse is proved here.
Piecewise-linear maps of the line #
The two-piece criterion on ℝ, its local converse, and the absolute value as a piecewise-linear
map that is not affine. The criterion is what the concrete examples of the PL groupoid are built
from; the converse, that a piecewise-linear map of the line has two affine pieces at each point, is
the local picture of a piecewise-linear curve, which for an injective curve is two segments meeting
only at the point; and the absolute value pins down that TauCeti.IsPLOn is strictly weaker than
affineness rather than a roundabout way of saying it.
A piecewise-linear map of the line is affine on each side of a point. If g is piecewise
linear on a neighbourhood of t, then for some ε > 0 it agrees with a continuous affine map on
[t - ε, t] and with another on [t, t + ε].
An injective piecewise-linear curve is two segments near each point. If g is piecewise
linear and injective near t, then for some ε > 0 it maps [t - ε, t] and [t, t + ε] onto
two nondegenerate segments from g t meeting only at g t.
A map that fails to send a midpoint to the corresponding midpoint agrees with no continuous affine map. This is the certificate used below to show that a piecewise-linear map need not be affine.