OAI/GroupTheory/PolycyclicRecognition/Geometry/BoundaryMapFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Continuous boundary maps with one compact shadow

  1. structure OAI.PolycyclicRecognition.BoundaryMapFamily line 12

    Source documentation

    Data constructed by the ray-limit theorem. The compact set is common to all maps in the family and all ambient basepoints.

    structure BoundaryMapFamily {P G S T : Type*} [Group G]
    [One S] [TopologicalSpace S] [One T] [TopologicalSpace T]
    (actS : G →* Equiv.Perm S) (actT : G →* Equiv.Perm T) (f : P → G → G) where
…