OAI/Geometry/HyperbolicGroups/IndexedWordPicture.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Persistent cell identities on word pictures. Unlike a bare relator witness, this marking remembers which actual cell each interior face uses.

  1. structure OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing line 18
  2. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.outside_face line 30
  3. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.commute_inv line 33
  4. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.reverse_prev line 41
  5. def OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.mirror line 45
  6. def OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.cornerWeight line 72

    Source documentation

    Count one marked corner of every interior face. Exterior corners contribute zero. This uses independent cell coefficients, not the word image.

    def cornerWeight (weight : C → A) (s : Option B.Side) : A :=
…
  7. def OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.chain line 77
  8. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.cornerWeight_opposite line 79
  9. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.mirror_chain line 88