WordPictureCell.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PictureSwitch.CellTarget.opposite_inv_next line 22
lemma OAI.HyperbolicObstruction.PictureSwitch.CellTarget.reverse_boundary line 26
lemma OAI.HyperbolicObstruction.PictureSwitch.CellTarget.reverse_boundary_labels line 41

theorem OAI.HyperbolicObstruction.WordPictures.WordPicture.cellular_index line 61

Source documentation

Each relator is represented by its genuine enumerated indexed target boundary. Coherent cellular maps are CONSTRUCTED from this attaching data; side labels need not be injective.

theorem cellular_index
    (hR : ∀ r ∈ R, ∃ ys : List S, IsBoundary T.next ys ∧ ys.map T.edge = r)
    (hw : ∃ ys : List S, IsBoundary T.next ys ∧ ys.map T.edge = w) :
    ∃ j : P.Dart → S, IndexedFaceMap P.pairing.face T.next j ∧
      ∀ x, T.edge (j x) = P.label x := by
…

theorem OAI.HyperbolicObstruction.WordPictures.WordPicture.cellular_picture line 85
Source documentation
An actual mapped cellular picture, with the SAME side pairing and genus, not a new picture-existence or normality assumption. The arbitrary exterior must be supplied as its own target polygon, not confused with a relator.
```
theorem cellular_picture
    (hR : ∀ r ∈ R, ∃ ys : List S, IsBoundary T.next ys ∧ ys.map T.edge = r)
    (hw : ∃ ys : List S, IsBoundary T.next ys ∧ ys.map T.edge = w) :
    ∃ Q : CellPicture T, HEq Q.pairing P.pairing := by
…
```

theorem OAI.HyperbolicObstruction.WordPictures.cellular_picture_existence line 106

Source documentation

Literal null words produce actual indexed target-cell pictures whenever these are the given attaching polygons together with one exterior polygon.

theorem cellular_picture_existence
    (hR : ∀ r ∈ R, ∃ ys : List S, IsBoundary T.next ys ∧ ys.map T.edge = r)
    (hw : ∃ ys : List S, IsBoundary T.next ys ∧ ys.map T.edge = w)
    (h : PresentedGroup.mk (FreeGroup.mk '' R) (FreeGroup.mk w) = 1) :
    Nonempty (CellPicture.{0} T) := by
…