OAI/Geometry/HyperbolicGroups/BoundaryIndex.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.PictureSwitch.boundaryIndex line 18

   Source documentation

   A literal indexed match between two enumerated boundaries. Repeated edge letters are not quotiented: this map uses the unique side positions.

   def boundaryIndex (xs : List D) (ys : List S) (hlen : xs.length = ys.length)
       (x : D) (hx : x ∈ xs) : S :=
   …

2. lemma OAI.HyperbolicObstruction.PictureSwitch.boundaryIndex_get line 22
3. lemma OAI.HyperbolicObstruction.PictureSwitch.boundaryIndex_label line 29
4. lemma OAI.HyperbolicObstruction.PictureSwitch.boundaryIndex_inj line 39
5. lemma OAI.HyperbolicObstruction.PictureSwitch.boundaryIndex_commute line 51
6. theorem OAI.HyperbolicObstruction.PictureSwitch.indexedFaceMap_exists line 67

   Source documentation

   Build a coherent index map by selecting one boundary match PER FACE, not independently per side. This is the coherence step between word van Kampen diagrams and actual cellular pictures.

   theorem indexedFaceMap_exists (f : Perm D) (t : Perm S) (label : D → L) (edge : S → L)
       (h : ∀ x : D, ∃ xs : List D, ∃ ys : List S,
         IsBoundary f xs ∧ x ∈ xs ∧ IsBoundary t ys ∧ xs.map label = ys.map edge) :
       ∃ j : D → S, IndexedFaceMap f t j ∧ ∀ x, edge (j x) = label x := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.IsBoundary, OAI.HyperbolicObstruction.PictureSwitch.IndexedFaceMap