OAI/Geometry/HyperbolicGroups/PermEuler.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.sameCycle_le_of_apply line 18
2. lemma OAI.HyperbolicObstruction.PictureSwitch.sameCycle_swap_le line 29
3. lemma OAI.HyperbolicObstruction.PictureSwitch.sameCycle_mul_le line 40
4. lemma OAI.HyperbolicObstruction.PictureSwitch.sameCycle_glue line 47
5. lemma OAI.HyperbolicObstruction.PictureSwitch.potential_step line 54

   Source documentation

   The Euler potential increases by at most one on adjoining a paired side. If the side joins different components, the face cycles merge and the bound is an equality. This is the combinatorial source of the genus inequality.

   lemma potential_step {p : Perm D} {s : Setoid D} (h : SameCycle.setoid p ≤ s)
       (a b : D) :
       cycles (p * swap a b) - 2 * (Nat.card (Quotient (glue s a b)) : ℤ) ≤
         cycles p - 2 * (Nat.card (Quotient s) : ℤ) + 1 := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles, OAI.HyperbolicObstruction.PictureSwitch.glue

6. def OAI.HyperbolicObstruction.PictureSwitch.joins line 77

   Source documentation

   Components after adjoining a finite list of side pairings.

   def joins (s : Setoid D) : List (D × D) → Setoid D
     | [] => s
     | (a,b)::l => joins (glue s a b) l

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.glue

7. def OAI.HyperbolicObstruction.PictureSwitch.swaps line 81
8. lemma OAI.HyperbolicObstruction.PictureSwitch.le_joins line 84
9. lemma OAI.HyperbolicObstruction.PictureSwitch.joins_le line 90
10. lemma OAI.HyperbolicObstruction.PictureSwitch.sameCycle_joins line 98
11. theorem OAI.HyperbolicObstruction.PictureSwitch.potential_list line 107

    Source documentation

    The full finite combinatorial Euler inequality before identifying the final components with a particular surface.

    theorem potential_list {p : Perm D} {s : Setoid D} (h : SameCycle.setoid p ≤ s)
        (l : List (D × D)) :
        cycles (p * swaps l) - 2 * (Nat.card (Quotient (joins s l)) : ℤ) ≤
          cycles p - 2 * (Nat.card (Quotient s) : ℤ) + l.length := by
    …

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles, OAI.HyperbolicObstruction.PictureSwitch.swaps, OAI.HyperbolicObstruction.PictureSwitch.joins