OAI/Topology/EilenbergGanea/SeedHolonomy.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Exact quaternion monodromy of the fixed presentation seed.

  1. abbrev OAI.EilenbergGanea.SeedSU2 line 15
  2. def OAI.EilenbergGanea.seedGoldenReal line 17
  3. def OAI.EilenbergGanea.seedXQuaternion line 19
  4. def OAI.EilenbergGanea.seedYQuaternion line 20
  5. theorem OAI.EilenbergGanea.seedGoldenReal_quadratic line 23
  6. theorem OAI.EilenbergGanea.seedGoldenReal_cubic line 28
  7. theorem OAI.EilenbergGanea.seedGoldenReal_quartic line 33
  8. theorem OAI.EilenbergGanea.seedX_normSq line 39
  9. theorem OAI.EilenbergGanea.seedY_normSq line 43
  10. def OAI.EilenbergGanea.seedXUnit line 53
  11. def OAI.EilenbergGanea.seedYUnit line 57
  12. theorem OAI.EilenbergGanea.unitQuaternion_quadratic line 61
  13. theorem OAI.EilenbergGanea.unitQuaternion_half_cube line 72
  14. theorem OAI.EilenbergGanea.seedX_square line 83
  15. theorem OAI.EilenbergGanea.seedY_fifth line 95
  16. theorem OAI.EilenbergGanea.seedXYinv_cube line 131
  17. theorem OAI.EilenbergGanea.seed_unit_relations line 138
  18. def OAI.EilenbergGanea.seedRelator line 149
  19. theorem OAI.EilenbergGanea.seedWord_relator line 153
  20. def OAI.EilenbergGanea.seedLetterUnit line 156
  21. theorem OAI.EilenbergGanea.seedRelator_unit line 160
  22. abbrev OAI.EilenbergGanea.SeedPresentationGroup line 167
  23. def OAI.EilenbergGanea.seedMonodromy line 169
  24. theorem OAI.EilenbergGanea.seedMonodromy_nontrivial line 174
  25. def OAI.EilenbergGanea.seedExponentMatrix line 180

    Source documentation

    The source exponent-sum boundary, with rows indexed by its two relators.

    def seedExponentMatrix : Matrix (Fin 2) (Fin 2) ℤ := !![2,-5;-1,3]
  26. theorem OAI.EilenbergGanea.seedExponentMatrix_det line 182