OAI/Algebra/Finitistic/Selection/GroupSelection.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.commutator_transfer line 20

   Source documentation

   The commutator transfer identity establishing independence of the internal index in the paper's central involutions.

   theorem commutator_transfer (x y v u w : G)
       (hu : x*y = u*y*x) (hw : y*v = w*v*y)
       (hxv : Commute x v) (hwu : Commute w u) (hwv : Commute w v) :
       ⁅x,w⁆ = ⁅u,v⁆ := by
   …

2. theorem OAI.LittleFinitistic.central_commutator_involution line 56

   Source documentation

   A central commutator of an involution has order dividing two.

   theorem central_commutator_involution (x y : G) (hx : x*x = 1)
       (hc : Commute x ⁅x,y⁆) : ⁅x,y⁆ * ⁅x,y⁆ = 1 := by
   …

3. structure OAI.LittleFinitistic.SelectionGroupData line 67

   Source documentation

   The relators used for the off-diagonal generators in Section 2. The presentation and its finite-presentation reduction are separate obligations.

   structure SelectionGroupData (G : Type*) [Group G] where
   …

4. theorem OAI.LittleFinitistic.SelectionGroupData.split_transfer line 91
5. theorem OAI.LittleFinitistic.SelectionGroupData.splitting_independent line 112
6. def OAI.LittleFinitistic.SelectionGroupData.centralZ line 121
7. theorem OAI.LittleFinitistic.SelectionGroupData.centralZ_eq line 123
8. theorem OAI.LittleFinitistic.SelectionGroupData.centralZ_commute_U line 127
9. theorem OAI.LittleFinitistic.SelectionGroupData.centralZ_commute_V line 135
10. theorem OAI.LittleFinitistic.SelectionGroupData.centralZ_commute_W line 143
11. theorem OAI.LittleFinitistic.SelectionGroupData.centralZ_involution line 151
12. theorem OAI.LittleFinitistic.SelectionGroupData.centralZ_commute_T line 155
13. inductive OAI.LittleFinitistic.Presentation.Generator line 168
14. abbrev OAI.LittleFinitistic.Presentation.t line 174
15. abbrev OAI.LittleFinitistic.Presentation.u line 175
16. abbrev OAI.LittleFinitistic.Presentation.v line 176
17. abbrev OAI.LittleFinitistic.Presentation.w line 177
18. inductive OAI.LittleFinitistic.Presentation.Equation line 182

    Source documentation

    Explicit equation patterns of the paper's infinite presentation. Diagonal W generators are set to one, so the total-index notation introduces no additional group generators compared with the manuscript.

    inductive Equation : FreeGroup Generator → FreeGroup Generator → Prop where
    …

    Mentions: OAI.LittleFinitistic.Presentation.Generator

19. def OAI.LittleFinitistic.Presentation.relators line 198
20. abbrev OAI.LittleFinitistic.Presentation.AuxiliaryGroup line 199
21. theorem OAI.LittleFinitistic.Presentation.equation_holds line 201
22. def OAI.LittleFinitistic.Presentation.data line 205
23. def OAI.LittleFinitistic.Presentation.z line 232
24. theorem OAI.LittleFinitistic.Presentation.z_involution line 234
25. theorem OAI.LittleFinitistic.Presentation.z_central line 236
26. def OAI.LittleFinitistic.Presentation.evaluate line 252
27. theorem OAI.LittleFinitistic.Presentation.evaluate_equation line 258
28. def OAI.LittleFinitistic.Presentation.ofData line 276
29. theorem OAI.LittleFinitistic.Presentation.ofData_of line 282
30. def OAI.LittleFinitistic.Presentation.shiftData line 285
31. def OAI.LittleFinitistic.Presentation.shiftHom line 307
32. theorem OAI.LittleFinitistic.Presentation.shiftHom_T line 309
33. theorem OAI.LittleFinitistic.Presentation.shiftHom_U line 312
34. theorem OAI.LittleFinitistic.Presentation.shiftHom_V line 316
35. theorem OAI.LittleFinitistic.Presentation.shiftHom_W line 320
36. theorem OAI.LittleFinitistic.Presentation.shiftHom_comp line 324
37. theorem OAI.LittleFinitistic.Presentation.shiftHom_zero line 329
38. def OAI.LittleFinitistic.Presentation.shiftAut line 334
39. theorem OAI.LittleFinitistic.Presentation.shiftAut_z line 345