Products of piecewise-linear maps

Pairing two piecewise-affine maps refines their finite polyhedral covers by intersections. Localizing this construction gives pairing and products of PL maps, and characterizes PL maps into a product by their components. The product theorem supplies PL coordinate changes for product manifolds, including products of models with boundary and corners.

Reference: C. Rourke and B. Sanderson, Introduction to Piecewise-Linear Topology, Chapters 1–2. The affine pieces use Mathlib's ContinuousAffineMap.prod.

theorem TauCeti.IsPiecewiseAffineOn.prodMk {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] {f : E → F} {g : E → G} {s : Set E} (hf : IsPiecewiseAffineOn f s) (hg : IsPiecewiseAffineOn g s) : IsPiecewiseAffineOn (fun (x : E) => (f x, g x)) s

Pairing two piecewise-affine maps on the same set is piecewise affine.

@[simp]

theorem TauCeti.isPiecewiseAffineOn_prod_iff {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] {f : E → F × G} {s : Set E} : IsPiecewiseAffineOn f s ↔ IsPiecewiseAffineOn (fun (x : E) => (f x).1) s ∧ IsPiecewiseAffineOn (fun (x : E) => (f x).2) s

A map into a product is piecewise affine exactly when both components are.

theorem TauCeti.IsPiecewiseAffineOn.prodMap {E : Type u_1} {F : Type u_2} {G : Type u_3} {D : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] [AddCommGroup D] [Module ℝ D] [TopologicalSpace D] {f : E → F} {g : G → D} {s : Set E} {t : Set G} (hf : IsPiecewiseAffineOn f s) (hg : IsPiecewiseAffineOn g t) : IsPiecewiseAffineOn (Prod.map f g) (s ×ˢ t)

Products of piecewise-affine maps are piecewise affine on product sets.

theorem TauCeti.IsPLOn.prodMk {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] {f : E → F} {g : E → G} {s : Set E} (hf : IsPLOn f s) (hg : IsPLOn g s) : IsPLOn (fun (x : E) => (f x, g x)) s

Pairing two PL maps on the same set is PL.

@[simp]

theorem TauCeti.isPLOn_prod_iff {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] {f : E → F × G} {s : Set E} : IsPLOn f s ↔ IsPLOn (fun (x : E) => (f x).1) s ∧ IsPLOn (fun (x : E) => (f x).2) s

A map into a product is PL exactly when both components are.

theorem TauCeti.IsPLOn.prodMap {E : Type u_1} {F : Type u_2} {G : Type u_3} {D : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] [AddCommGroup D] [Module ℝ D] [TopologicalSpace D] {f : E → F} {g : G → D} {s : Set E} {t : Set G} (hf : IsPLOn f s) (hg : IsPLOn g t) : IsPLOn (Prod.map f g) (s ×ˢ t)

Products of PL maps are PL on product sets. No finiteness or openness assumption on the domains is needed.