OAI/Geometry/HyperbolicGroups/WalkCell.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget line 23

    Source documentation

    Indexed oriented steps in polygonal cells, with selected cells permitted to have arbitrary closed template walks. In the cone target these are precisely top-cone walks; all fan triangles and decoration disks are frozen. Template vertices retain their occurrence index, while vertex is their actual image in the target one-skeleton. These are incidence definitions, not diagram or normal-form hypotheses.

    structure WalkCellTarget (S : Type v) (C : Type w) (W : Type z) (L : Type k)
    (V : Type t) (A : Type r) [AddCommMonoid A] where
…
  2. structure OAI.HyperbolicObstruction.PictureSwitch.WalkPicture line 50
  3. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.chain line 65
  4. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Simple line 66
  5. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.NoBigon line 68
  6. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Reduced line 70
  7. structure OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Retains line 76

    Source documentation

    Retain every individual surviving step and EVERY frozen face. Only free cone steps may disappear; on frozen faces the original cyclic indexing is retained exactly, not just up to a word or a chain class.

    structure Retains (Q : WalkPicture.{u} T) where
…
  8. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Retains.refl line 84
  9. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Retains.trans line 87
  10. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.respects line 100
  11. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.nonmonogon line 110
  12. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.free_face line 118
  13. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.bigon_opposite line 123
  14. theorem OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.makeSimple line 136

    Source documentation

    The finite splitting producer acts on template vertices, NOT quotient letter vertices. Consequently a top can never acquire a false repeated visit merely because several numerical generator labels coincide.

    theorem makeSimple : ∃ Q : WalkPicture.{u} T,
    Nonempty (P.Retains Q) ∧ Q.Simple ∧ Q.chain = P.chain := by
…