Inverses of simplicial piecewise-affine maps

A map affine on each simplex of a finite cover has a piecewise-affine inverse on its image, provided each simplex's vertex images are affinely independent. The inverse need only be supplied as a function with the left inverse law; continuity and PL regularity follow from the simplex formulas. This is the inverse regularity criterion used when identifying polyhedra by subdivisions.

The finite-cover conclusion gives TauCeti.IsPLOn by TauCeti.IsPiecewiseAffineOn.isPLOn and restricts to chart domains by TauCeti.IsPLOn.mono. This is the local map predicate used by TauCeti.PLPregroupoid and TauCeti.PLGroupoid in TauCeti.Geometry.Manifold.PLGroupoid.

The image simplices give the polyhedral cover, and affine interpolation on their vertices gives the inverse formulas. The ambient target is finite dimensional; the source may be any topological real vector space. The simplices and their images may have positive codimension or be empty. No intersection condition between the simplices is needed.

Reference: Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapters 1--2.

theorem TauCeti.isPiecewiseAffineOn_inverse_of_finite_simplex_cover {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : E → F} {g : F → E} {ι : Type u_3} [Finite ι] (s : ι → Set E) (A : ι → E →ᴬ[ℝ] F) (heq : ∀ (i : ι), Set.EqOn f (⇑(A i)) ((convexHull ℝ) (s i))) (hind : ∀ (i : ι), AffineIndependent ℝ Subtype.val) (hgf : ∀ x ∈ ⋃ (i : ι), (convexHull ℝ) (s i), g (f x) = x) : IsPiecewiseAffineOn g (f '' ⋃ (i : ι), (convexHull ℝ) (s i))

An inverse of a simplexwise affine map is piecewise affine on the image of a finite simplex cover. Nondegeneracy is required only for the image vertices of each individual simplex; neither full-dimensional simplices nor a normed or finite-dimensional source are required.