DipoleSwitch.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces line 21
Source documentation
Two oppositely oriented face boundaries, including their particular cyclic parametrizations. The two occurrences are disjoint, even if the target cell or some target boundary vertices coincide.
```
structure OppositeFaces (f : Perm D) (q : Perm I) (a b : I → D) : Prop where
…
```
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.paired_reverse line 31
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.dipole_sameVertex line 34
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.dipole_switch_pairs line 52
Source documentation
The elementary cancellation switch pairs the next two boundary sides, while retaining every already paired side of the two cancellation faces.
```
lemma dipole_switch_pairs (hF : OppositeFaces M.face q a b) (k : I) :
    (M.switch (a k) (M.edge (b k))).edge (a k) = b k ∧
      ∀ j, M.edge (a j) = b j → (M.switch (a k) (M.edge (b k))).edge (a j) = b j := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces
theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.isolate_dipole line 85
Source documentation
A complete dipole can be separated by finitely many genuine crosswise side-pairing switches. This is the producer behind cancellation in a minimal mapped sphere/disk picture. It preserves genus zero, the face permutation and all original oriented side labels; it does NOT presuppose a normal picture.
```
theorem isolate_dipole (hF : OppositeFaces M.face q a b) (i₀ : I)
    (hseed : M.edge (a i₀) = b i₀) {label : D → L} {start : L → V} {rev : L → L}
    (hM : M.Respects label start rev) (hG : M.GenusZero)
    (hinv : ∀ l, rev (rev l) = l) (hop : ∀ i, label (b i) = rev (label (a i))) :
    ∃ N : PictureMap D, N.face = M.face ∧ N.Respects label start rev ∧ N.GenusZero ∧
      (∀ i, M.edge (a i) = b i → N.edge (a i) = b i) ∧ ∀ i, N.edge (a i) = b i := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces, OAI.HyperbolicObstruction.PictureSwitch.PictureMap