Equivariant overlap recoding

Abstract

The boundary transfer induces a homeomorphism of the associated skew-product path spaces.

Definition 1.1 (Construct the skew-product homeomorphism).

$$\forall U\in Type,V\in Type,I\in Type,J\in Type,H\in Type,group\in \mathrm{Group}\left(H\right),d\in \mathrm{Boundary}\left(U,V,I,J\right),alpha\in U\to H,topologyU\in \mathrm{TopologicalSpace}\left(U\right),topologyV\in \mathrm{TopologicalSpace}\left(V\right),topologyH\in \mathrm{TopologicalSpace}\left(H\right),continuousGroup\in \mathrm{IsTopologicalGroup}\left(H\right),alphaContinuous\in \mathrm{Continuous}\left(alpha\right),\mathrm{Homeomorph}\left(\mathrm{Prod}\left(\mathrm{LeftPath}\left(d\right),H\right),\mathrm{Prod}\left(\mathrm{RightPath}\left(d\right),H\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/EquivariantOverlapRecoding.skewHomeomorph (✓ std3).

Source. Repository-derived.

Commentary.

The path overlap code and the right group-coordinate transfer are constructed together. The inverse reads the preceding half-edge, and both directions are continuous.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/EquivariantOverlapRecoding.skewHomeomorph
• Dependency: D5/S3/ConceptDynamics/Coding/BipartiteOverlapConjugacy