OAI/Geometry/HyperbolicGroups/DipoleRemove.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.InDipole line 21

   Source documentation

   The darts of the two particular face occurrences being cancelled.

   def InDipole (a b : I → D) (x : D) : Prop := (∃ i, a i = x) ∨ ∃ i, b i = x
   …

2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces.range_a_invariant line 27
3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces.range_b_invariant line 36
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces.inDipole_face line 43
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces.a_sameCycle line 46
6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces.b_sameCycle line 55
7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces.not_sameCycle_ab line 64
8. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces.dipoleClassesEquiv line 71

   Source documentation

   Exactly the two face classes, not an arbitrary assumed two-cell subset.

   def dipoleClassesEquiv [Fintype D] [Fintype I] (i₀ : I) : Bool ≃
       Quotient ((SameCycle.setoid f).comap (Subtype.val : {x // InDipole a b x} → D)) := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.InDipole

9. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces.cycles_dipole line 95
10. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.inDipole_edge line 107
11. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.removeDipole line 121

    Source documentation

    Delete the isolated dipole; every unremoved face and dart retains its original index, and every surviving side pairing is unchanged.

    def removeDipole (hF : OppositeFaces M.face q a b) (hp : ∀ i, M.edge (a i) = b i) :
        PictureMap {x : D // ¬ InDipole a b x} :=
    …

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

12. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.removeDipole_genusZero line 125
13. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.removeDipole_faces line 134
14. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.restrict_respects line 142