Piecewise-linear maps between PL manifolds

A PL manifold is a charted space M over H with HasGroupoid M (PLGroupoid I) (TauCeti.PLGroupoid). This file defines the maps between such spaces that are piecewise linear, in the same way as Mathlib defines ContMDiff from ContDiffWithinAt: a map is PL at a point when it is continuous there and, read in the preferred charts at the point and at its image and then in the model vector spaces through I and I', it is piecewise affine on a neighbourhood of the point (TauCeti.IsPLWithinAt).

The property in the model, TauCeti.PLWithinAtProp, is local and invariant under the PL groupoids in the source and in the target (TauCeti.plWithinAtProp_localInvariantProp), so Mathlib's theory of local invariant properties applies. In particular, on PL manifolds the preferred charts can be replaced by any charts of the maximal PL atlases (TauCeti.isPLMapAt_iff_of_mem_maximalAtlas): being PL is a property of the PL structures, not of the chosen atlases. Charts of the maximal PL atlas and their inverses are PL (TauCeti.isPLMapAt_of_mem_maximalAtlas, TauCeti.isPLMapAt_symm_of_mem_maximalAtlas), so are the identity and constant maps, PL maps compose (TauCeti.IsPLMapAt.comp), and between real normed spaces with their trivial charts the PL maps are exactly the maps piecewise linear on the whole space (TauCeti.isPLMap_iff_isPLOn_univ).

The construction and the proof of TauCeti.plWithinAtProp_localInvariantProp follow Mathlib's ContDiffWithinAtProp and contDiffWithinAt_localInvariantProp (Mathlib/Geometry/Manifold/ContMDiff/Defs.lean), by Sébastien Gouëzel and Floris van Doorn.

Main definitions

• TauCeti.PLWithinAtProp I I' f s x: the map f : H → H' of model spaces is piecewise linear within s at x when read in the model vector spaces.
• TauCeti.IsPLMapAt I I' f x: the map f : M → M' is continuous at x and piecewise linear near x when read in charts.
• TauCeti.IsPLMap I I' f: the map f : M → M' is piecewise linear at every point.

Main results

• TauCeti.plWithinAtProp_localInvariantProp: piecewise linearity in the model is a local property invariant under the PL groupoids.
• TauCeti.isPLMapAt_iff: the defining condition, in the preferred charts.
• TauCeti.isPLMapAt_iff_of_mem_maximalAtlas: the same condition in any charts of the maximal PL atlases.
• TauCeti.isPLMapAt_of_mem_maximalAtlas, TauCeti.isPLMapAt_symm_of_mem_maximalAtlas: charts of the maximal PL atlas and their inverses are PL.
• TauCeti.isPLMap_id, TauCeti.isPLMap_const, TauCeti.IsPLMapAt.comp, TauCeti.IsPLMap.comp: identities and constant maps are PL, and PL maps compose.
• TauCeti.isPLMap_iff_isPLOn_univ: a map between real normed spaces is a PL map exactly when it is piecewise linear on the whole space.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapter 1, for PL maps and PL manifolds.

The property in the model spaces

def TauCeti.PLWithinAtProp {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') (f : H → H') (s : Set H) (x : H) : Prop

A map f : H → H' between model spaces is piecewise linear within s at x when I' ∘ f ∘ I.symm, its reading in the model vector spaces, is piecewise linear within I.symm ⁻¹' s ∩ range I at I x. This is the property lifted to charted spaces to define PL maps, as ContDiffWithinAtProp is for ContMDiff.

theorem TauCeti.plWithinAtProp_id {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (x : H) : PLWithinAtProp I I id Set.univ x

The identity of a model space is piecewise linear everywhere.

theorem TauCeti.plWithinAtProp_localInvariantProp {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') : (PLGroupoid I).LocalInvariantProp (PLGroupoid I') (PLWithinAtProp I I')

Piecewise linearity is a local invariant property: in the model it is local, and invariant under the PL groupoids of the source and of the target. So it lifts to charted spaces, where it does not depend on the charts of the maximal PL atlases used to read it.

PL maps between charted spaces

def TauCeti.IsPLMapAt {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] (f : M → M') (x : M) : Prop

A map f : M → M' between charted spaces is piecewise linear at x when it is continuous at x and, read in the preferred charts at x and at f x and then in the model vector spaces, it is piecewise linear near x (TauCeti.isPLMapAt_iff). On PL manifolds any charts of the maximal PL atlases may be used instead (TauCeti.isPLMapAt_iff_of_mem_maximalAtlas).

def TauCeti.IsPLMap {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] (f : M → M') : Prop

A map f : M → M' between charted spaces is piecewise linear when it is piecewise linear at every point.

theorem TauCeti.isPLMapAt_iff {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} : IsPLMapAt I I' f x ↔ ContinuousAt f x ∧ IsPLWithinAt (↑I' ∘ ↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) (Set.range ↑I) (↑I (↑(chartAt H x) x))

A map is PL at x exactly when it is continuous at x and its reading in the preferred charts and the model vector spaces is piecewise linear near the image of x.

theorem TauCeti.isPLMap_iff_forall_isPLMapAt {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} : IsPLMap I I' f ↔ ∀ (x : M), IsPLMapAt I I' f x

A map is PL exactly when it is PL at every point.

theorem TauCeti.IsPLMap.isPLMapAt {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} (h : IsPLMap I I' f) (x : M) : IsPLMapAt I I' f x

A PL map is PL at every point.

theorem TauCeti.IsPLMapAt.continuousAt {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} (h : IsPLMapAt I I' f x) : ContinuousAt f x

A map PL at a point is continuous there.

theorem TauCeti.IsPLMap.continuous {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} (h : IsPLMap I I' f) : Continuous f

A PL map is continuous.

theorem TauCeti.isPLMapAt_iff_of_mem_maximalAtlas {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} {e : OpenPartialHomeomorph M H} {e' : OpenPartialHomeomorph M' H'} (he : e ∈ StructureGroupoid.maximalAtlas M (PLGroupoid I)) (hx : x ∈ e.source) (he' : e' ∈ StructureGroupoid.maximalAtlas M' (PLGroupoid I')) (hy : f x ∈ e'.source) : IsPLMapAt I I' f x ↔ ContinuousAt f x ∧ IsPLWithinAt (↑I' ∘ ↑e' ∘ f ∘ ↑e.symm ∘ ↑I.symm) (Set.range ↑I) (↑I (↑e x))

Chart independence. A map is PL at x exactly when it is continuous at x and its reading in any charts e at x and e' at f x of the maximal PL atlases is piecewise linear near I (e x).

theorem TauCeti.isPLMap_id {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] : IsPLMap I I id

The identity of a charted space is PL.

theorem TauCeti.isPLMap_const {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] (c : M') : IsPLMap I I' fun (x : M) => c

A constant map is PL.

theorem TauCeti.isPLMapAt_of_mem_maximalAtlas {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {e : OpenPartialHomeomorph M H} (he : e ∈ StructureGroupoid.maximalAtlas M (PLGroupoid I)) {x : M} (hx : x ∈ e.source) : IsPLMapAt I I (↑e) x

A chart of the maximal PL atlas is PL on its source.

theorem TauCeti.isPLMapAt_symm_of_mem_maximalAtlas {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {e : OpenPartialHomeomorph M H} (he : e ∈ StructureGroupoid.maximalAtlas M (PLGroupoid I)) {x : H} (hx : x ∈ e.target) : IsPLMapAt I I (↑e.symm) x

The inverse of a chart of the maximal PL atlas is PL on its target.

theorem TauCeti.IsPLMapAt.comp {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {E'' : Type u_5} {H'' : Type u_6} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] {I'' : ModelWithCorners ℝ E'' H''} {M : Type u_7} {M' : Type u_8} {M'' : Type u_9} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace M''] [ChartedSpace H'' M''] {g : M' → M''} {f : M → M'} {x : M} (hg : IsPLMapAt I' I'' g (f x)) (hf : IsPLMapAt I I' f x) : IsPLMapAt I I'' (g ∘ f) x

PL maps compose: if f is PL at x and g is PL at f x, then g ∘ f is PL at x.

theorem TauCeti.IsPLMap.comp {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {E'' : Type u_5} {H'' : Type u_6} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] {I'' : ModelWithCorners ℝ E'' H''} {M : Type u_7} {M' : Type u_8} {M'' : Type u_9} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace M''] [ChartedSpace H'' M''] {g : M' → M''} {f : M → M'} (hg : IsPLMap I' I'' g) (hf : IsPLMap I I' f) : IsPLMap I I'' (g ∘ f)

PL maps compose.

theorem TauCeti.isPLMap_iff_isPLOn_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {f : E → E'} : IsPLMap (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E') f ↔ IsPLOn f Set.univ

Between real normed spaces with their trivial charts, the PL maps are exactly the maps piecewise linear on the whole space.