OAI/Geometry/HyperbolicGroups/FrozenWalk.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.HyperbolicObstruction.PictureSwitch.FrozenTarget line 21

    Source documentation

    Additional literal boundary indexing for the cells which are not free macro walks. No normalization property is packaged into this data.

    structure FrozenTarget (T : WalkCellTarget S C W L V A) where
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget

  2. abbrev OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.FrozenDart line 33
  3. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.frozenFace line 35
  4. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.frozenFace_val line 40
  5. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.FrozenMapped line 44

    Source documentation

    Frozen source faces use one complete indexed side cycle, without wrapping. This property is imposed on raw cellular face maps, not on their reducedness.

    def FrozenMapped (B : FrozenTarget T) : Prop :=
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.FrozenTarget

  6. structure OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Survives line 50

    Source documentation

    Retain every surviving step, without changing any surviving frozen face. Unlike the stronger Retains, this permits cancellation of entire frozen faces. Protected outside faces will be retained separately at that boundary.

    structure Survives (Q : WalkPicture.{u} T) where
…
  7. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Retains.survives line 58
  8. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Survives.refl line 62
  9. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Survives.trans line 65
  10. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Survives.frozenMapped line 74
  11. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.opposite_frozen line 94
  12. theorem OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.frozen_opposite_faces line 100

    Source documentation

    Opposite frozen indexed sides determine the COMPLETE opposite faces, inside the ambient mixed free/frozen picture.

    theorem frozen_opposite_faces (B : FrozenTarget T) (hm : P.FrozenMapped B)
    (a b : P.Dart) (ha : T.free (T.kind (P.index a)) = false)
    (hop : P.index b = T.opposite (P.index a)) :
    let a' : P.FrozenDart := ⟨a,ha⟩
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.FrozenTarget