OAI/AlgebraicGeometry/CharacterVarieties/Foundation/BoundaryReordering.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.list_prod_pointwise_conjugation line 12
2. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.reorder_by_based_paths line 20

   Source documentation

   Each reordering admits basing paths preserving the total boundary word. circle labels are distinct; equal facet labels are irrelevant.

   theorem reorder_by_based_paths {l m : List I} (hp : l.Perm m) (hn : l.Nodup)
       (f : I → G) :
       ∃ z : I → G, (m.map (fun i => z i*f i*(z i)⁻¹)).prod=(l.map f).prod := by
   …

3. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.reorder_by_words line 68

   Source documentation

   Chosen paths may be words in the old boundary generators. Their images under evaluation work in every group and over every coefficient ring.

   theorem reorder_by_words {l m : List I} (hp : l.Perm m) (hn : l.Nodup) :
       ∃ z : I → FreeGroup I,
         ∀ {H : Type*} [Group H] (f : I → H),
           (m.map (fun i => (FreeGroup.lift f) (z i)*f i*
             ((FreeGroup.lift f) (z i))⁻¹)).prod=(l.map f).prod := by
   …

4. theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.fin_reorder_by_words line 84

   Source documentation

   The based words are chosen from the enumeration alone, before evaluating any old solution or any coefficient ring.

   theorem fin_reorder_by_words {n : ℕ} (σ : Equiv.Perm (Fin n)) :
       ∃ z : Fin n → FreeGroup (Fin n),
         ∀ {H : Type*} [Group H] (f : Fin n → H),
           (List.ofFn (fun b => (FreeGroup.lift f) (z (σ b))*f (σ b)*
             ((FreeGroup.lift f) (z (σ b)))⁻¹)).prod=(List.ofFn f).prod := by
   …

5. lemma OAI.IntegralCharacterVarieties.MatrixExpression.Term.eval_transport_iso line 105
6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.wordProduct_eval_raw line 122
7. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryWord_eval_raw line 130
8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryEdge_iso line 136
9. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sideBasis_boundary line 146
10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryEdge_gauge line 158
11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryWord_gauge line 178
12. lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.reverse_product_gauge line 193

    Source documentation

    Directed multiplication with wholly independent intermediate bases.

    lemma reverse_product_gauge (b e : ℕ → G) (n : ℕ) :
        (List.ofFn (fun i : Fin n => b (i.val+1)*e i.val*(b i.val)⁻¹)).reverse.prod=
          b n*(List.ofFn (fun i : Fin n => e i.val)).reverse.prod*(b 0)⁻¹ := by
    …

13. lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.cyclic_reverse_product_gauge line 205