MappedCancellation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.cancel_mapped_dipole line 22

Source documentation

Two opposite face occurrences sharing one indexed side are removed. The number of faces falls by exactly two, genus zero is retained, the target map on every surviving side is unchanged, and the exact lifted cellular chain is unchanged.

theorem cancel_mapped_dipole (M : PictureMap D) {q : Perm I} {a b : I → D}
    (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)))
    (w : D → A) (hw : ∀ x, w (M.face x) = w x) (hchain : w (a i₀) + w (b i₀) = 0) :
    ∃ R : PictureMap {x : D // ¬ InDipole a b x},
      R.GenusZero ∧ R.Respects (label ∘ Subtype.val) start rev ∧
      (∀ x, (R.face x).val = M.face x.val) ∧
      cycles R.face = cycles M.face - 2 ∧
      ∃ hR : ∀ x, (w ∘ Subtype.val) (R.face x) = (w ∘ Subtype.val) x,
        faceChain R.face (w ∘ Subtype.val) hR = faceChain M.face w hw := by
…

Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap, OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces, OAI.HyperbolicObstruction.PictureSwitch.PictureMap.InDipole, OAI.HyperbolicObstruction.PictureSwitch.cycles, OAI.HyperbolicObstruction.PictureSwitch.faceChain