OAI/Geometry/HyperbolicGroups/PictureFillingAlgebra.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.WordPictures.SymmetricRelator.filling line 14
2. lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.rotate_filling line 20
3. lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.peel line 28

   Source documentation

   The paid step for peeling an actual adjacent relator: its first side is paired to the first outside side. All other new boundary letters stay literal.

   lemma peel {a b : A × Bool} {l r : Word A} {n : ℕ}
       (hp : b = invLetter a) (hr : Homotopy R (b::r) [] 1)
       (h : Homotopy R (r++l) [] n) : Homotopy R (a::l) [] (1+n) := by
   …

   Mentions: OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.invLetter, OAI.HyperbolicObstruction.WordPictures.Homotopy