The PL structure groupoid

Mathlib builds a manifold out of a StructureGroupoid on the model space: contDiffGroupoid n I for smooth manifolds, continuousGroupoid H for topological ones. Between the two sits the piecewise-linear structure, and Mathlib has nothing for it. This file supplies it, in the same shape as contDiffGroupoid: a Pregroupoid whose property is "PL when read in the model through I", and the StructureGroupoid it generates.

Given a model with corners I : ModelWithCorners ℝ E H, a map f : H → H is declared PL on s : Set H when I ∘ f ∘ I.symm is piecewise linear (TauCeti.IsPLOn) on I.symm ⁻¹' s ∩ range I. Reading the property in the model this way — exactly as contDiffPregroupoid does — is what makes the definition apply verbatim to the half-space and quadrant models, so PL manifolds with boundary and with corners come out of the same definition as boundaryless ones, with no separate half-space predicate.

A PL manifold is then a charted space M over H with HasGroupoid M (PLGroupoid I). No new structure is introduced for it, matching Mathlib's treatment of IsManifold.

Main definitions

• TauCeti.PLPregroupoid: the pregroupoid of maps of H that are PL read in the model.
• TauCeti.PLGroupoid: the structure groupoid of PL open partial homeomorphisms of H.

Main results

• TauCeti.PLGroupoid_le_continuousGroupoid: the forgetful inclusion "PL implies Top".
• TauCeti.ofSet_mem_PLGroupoid and the ClosedUnderRestriction (PLGroupoid I) instance: the identity of an open set is PL, so the groupoid is closed under restriction. HasGroupoid does not itself ask for this, but the standard constructions downstream of it do — restricting a chart to an open subset (StructureGroupoid.restr_mem_maximalAtlas) and the charted-space structure an open subset inherits (TopologicalSpace.Opens.instHasGroupoid) both take ClosedUnderRestriction as an instance argument.

There is deliberately no inclusion in the other direction against contDiffGroupoid: a smooth transition map is not literally piecewise affine, and the comparison between the smooth and the PL structures is the Whitehead smoothing theory, not a containment of groupoids.

This is the structure-group track of layer 1 of the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md).

theorem TauCeti.isPLOn_comp_symm {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (s : Set H) : IsPLOn (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I)

Reading a map of H in the model through I turns it into a map between subsets of E; the identity I ∘ I.symm read this way is the identity of range I, and is therefore PL. This is the workhorse behind both the identity axiom of TauCeti.PLPregroupoid and the fact that TauCeti.PLGroupoid is closed under restriction.

def TauCeti.PLPregroupoid {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) : Pregroupoid H

Given a model with corners (E, H), the pregroupoid of PL transformations of H: those maps that are piecewise linear when read in E through I.

def TauCeti.PLGroupoid {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) : StructureGroupoid H

Given a model with corners (E, H), the groupoid of invertible PL transformations of H: the open partial homeomorphisms that are PL, with PL inverse, when read in E through I.

theorem TauCeti.mem_PLGroupoid_iff {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {e : OpenPartialHomeomorph H H} : e ∈ PLGroupoid I ↔ IsPLOn (↑I ∘ ↑e ∘ ↑I.symm) (↑I.symm ⁻¹' e.source ∩ Set.range ↑I) ∧ IsPLOn (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target ∩ Set.range ↑I)

Membership in TauCeti.PLGroupoid, unfolded: both the map and its inverse are PL when read in the model.

theorem TauCeti.PLGroupoid_le_continuousGroupoid {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) : PLGroupoid I ≤ continuousGroupoid H

A PL structure refines the topological structure groupoid.

@[simp]

theorem TauCeti.PLGroupoid_eq_top {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [Subsingleton E] : PLGroupoid I = ⊤

In a zero-dimensional model every coordinate transformation is PL.

instance TauCeti.instHasGroupoidPLGroupoidOfSubsingleton {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Subsingleton E] : HasGroupoid M (PLGroupoid I)

Every atlas over a zero-dimensional model is PL compatible.

theorem TauCeti.ofSet_mem_PLGroupoid {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {s : Set H} (hs : IsOpen s) : OpenPartialHomeomorph.ofSet s hs ∈ PLGroupoid I

The identity of an open set belongs to the PL groupoid.

instance TauCeti.instClosedUnderRestrictionPLGroupoid {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) : ClosedUnderRestriction (PLGroupoid I)

The PL groupoid is closed under restriction: the restriction of a PL chart to an open subset is again PL. This is what the constructions on open subsets of a PL manifold ask for.

A non-affine element of the PL groupoid

The PL groupoid of the trivial model on ℝ contains a homeomorphism that agrees with no affine map. So TauCeti.PLGroupoid is strictly larger than the groupoid of affine transition maps, and the definition above is not a roundabout way of asking for affineness.

noncomputable def TauCeti.doubleRight : ℝ ≃ₜ ℝ

The piecewise-linear homeomorphism of ℝ that is the identity on the non-positive half-line and multiplication by 2 on the non-negative one.

@[simp]

theorem TauCeti.doubleRight_apply (x : ℝ) : doubleRight x = if x ≤ 0 then x else 2 * x

@[simp]

theorem TauCeti.doubleRight_symm_apply (y : ℝ) : doubleRight.symm y = if y ≤ 0 then y else y / 2

theorem TauCeti.doubleRight_mem_PLGroupoid : doubleRight.toOpenPartialHomeomorph ∈ PLGroupoid (modelWithCornersSelf ℝ ℝ)

TauCeti.doubleRight is an element of the PL groupoid of the trivial model on ℝ.

theorem TauCeti.not_exists_continuousAffineMap_eq_doubleRight : ¬∃ (A : ℝ →ᴬ[ℝ] ℝ), ∀ (x : ℝ), doubleRight x = A x

TauCeti.doubleRight agrees with no continuous affine map: it fails to send the midpoint of -1 and 1 to the midpoint of their images.