Piecewise-linear homeomorphisms of weak polyhedra

This file packages a homeomorphism between the weak polyhedra of two precomplexes together with ambient coordinate formulas that are piecewise linear on their realised coordinate images. The package is independent of any particular subdivision construction, so stellar moves and other realization-level constructions can reuse the same relation and its symmetry and composition laws.

@[reducible, inline]

abbrev PreAbstractSimplicialComplex.realizedCoords {ι : Type u_1} (A : PreAbstractSimplicialComplex ι) : Set (ι → ℝ)

The ambient coordinate image of the weak polyhedron of A.

def PreAbstractSimplicialComplex.PLHomeomorphic {ι : Type u_1} {κ : Type u_2} (A : PreAbstractSimplicialComplex ι) (B : PreAbstractSimplicialComplex κ) : Prop

A and B have homeomorphic weak polyhedra via some e such that e and e.symm extend to maps between their ambient coordinate spaces that are piecewise linear on the respective coordinate images. The complexes may have different vertex types.

theorem PreAbstractSimplicialComplex.plHomeomorphic_iff {ι : Type u_1} {κ : Type u_2} {A : PreAbstractSimplicialComplex ι} {B : PreAbstractSimplicialComplex κ} : A.PLHomeomorphic B ↔ ∃ (e : { x : ⊤.Realization // (↑x).support ∈ A } ≃ₜ { x : ⊤.Realization // (↑x).support ∈ B }) (f : (ι → ℝ) → κ → ℝ) (g : (κ → ℝ) → ι → ℝ), TauCeti.IsPLOn f A.realizedCoords ∧ TauCeti.IsPLOn g B.realizedCoords ∧ (∀ (x : { x : ⊤.Realization // (↑x).support ∈ A }), f ⇑↑↑x = ⇑↑↑(e x)) ∧ ∀ (y : { x : ⊤.Realization // (↑x).support ∈ B }), g ⇑↑↑y = ⇑↑↑(e.symm y)

The witness characterization of PLHomeomorphic.

theorem PreAbstractSimplicialComplex.PLHomeomorphic.intro {ι : Type u_1} {κ : Type u_2} {A : PreAbstractSimplicialComplex ι} {B : PreAbstractSimplicialComplex κ} (e : { x : ⊤.Realization // (↑x).support ∈ A } ≃ₜ { x : ⊤.Realization // (↑x).support ∈ B }) (f : (ι → ℝ) → κ → ℝ) (g : (κ → ℝ) → ι → ℝ) (hf : TauCeti.IsPLOn f A.realizedCoords) (hg : TauCeti.IsPLOn g B.realizedCoords) (he : ∀ (x : { x : ⊤.Realization // (↑x).support ∈ A }), f ⇑↑↑x = ⇑↑↑(e x)) (heinv : ∀ (y : { x : ⊤.Realization // (↑x).support ∈ B }), g ⇑↑↑y = ⇑↑↑(e.symm y)) : A.PLHomeomorphic B

Construct a PLHomeomorphic witness from its homeomorphism and coordinate formulas.

theorem PreAbstractSimplicialComplex.PLHomeomorphic.refl {ι : Type u_1} (A : PreAbstractSimplicialComplex ι) : A.PLHomeomorphic A

Reflexivity of PLHomeomorphic.

theorem PreAbstractSimplicialComplex.PLHomeomorphic.symm {ι : Type u_1} {κ : Type u_2} {A : PreAbstractSimplicialComplex ι} {B : PreAbstractSimplicialComplex κ} (h : A.PLHomeomorphic B) : B.PLHomeomorphic A

Symmetry of PLHomeomorphic.

theorem PreAbstractSimplicialComplex.PLHomeomorphic.trans {ι : Type u_1} {κ : Type u_2} {ν : Type u_3} {A : PreAbstractSimplicialComplex ι} {B : PreAbstractSimplicialComplex κ} {C : PreAbstractSimplicialComplex ν} (hAB : A.PLHomeomorphic B) (hBC : B.PLHomeomorphic C) : A.PLHomeomorphic C

Transitivity of PLHomeomorphic.