IndexedFace.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.HyperbolicObstruction.PictureSwitch.IndexedFaceMap line 19
Source documentation
An indexed cellular face map. Commutation records EACH indexed side (not just its edge label); injectivity on a face rules out wrapping a cell twice.
```
structure IndexedFaceMap (f : Perm D) (t : Perm S) (j : D → S) : Prop where
…
```
lemma OAI.HyperbolicObstruction.PictureSwitch.semiconj_perm_pow line 23
lemma OAI.HyperbolicObstruction.PictureSwitch.semiconj_perm_inv line 30
lemma OAI.HyperbolicObstruction.PictureSwitch.semiconj_perm_zpow line 36
lemma OAI.HyperbolicObstruction.PictureSwitch.semiconj_perm_sameCycle line 45
lemma OAI.HyperbolicObstruction.PictureSwitch.IndexedFaceMap.orbit_surjective line 56
Source documentation
Every indexed face maps ONTO its full target side cycle as well.
```
lemma orbit_surjective (a : D) {s : S} (hs : t.SameCycle (j a) s) :
    ∃ b, f.SameCycle a b ∧ j b = s := by
…
```
def OAI.HyperbolicObstruction.PictureSwitch.IndexedFaceMap.orbitEquiv line 61
lemma OAI.HyperbolicObstruction.PictureSwitch.IndexedFaceMap.orbitEquiv_val line 70
theorem OAI.HyperbolicObstruction.PictureSwitch.IndexedFaceMap.opposite_faces line 77
Source documentation
Opposite target sides, including their INDEX, determine opposite complete source face parametrizations. In particular, this derives cancellation data from a cellular map rather than taking opposite copies as an extra normality assumption. Target cycles of opposite orientations are disjoint.
```
theorem opposite_faces [DecidableEq D] [Fintype D]
    (r : Perm S) (hr : r * r = 1)
    (hrev : ∀ s, r (t s) = t⁻¹ (r s))
    (hdisj : ∀ s, ¬ t.SameCycle s (r s))
    (a b : D) (hab : j b = r (j a)) :
    ∃ q : Perm {x : D // f.SameCycle a x},
      ∃ v : {x : D // f.SameCycle a x} → D,
        PictureMap.OppositeFaces f q Subtype.val v ∧
        v ⟨a,SameCycle.rfl⟩ = b ∧ ∀ x, j (v x) = r (j x.val) := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces