OAI/Geometry/ConjugatePoints/FundamentalGroup.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

Fundamental-group relations and nontrivial fiber classes.

  1. lemma OAI.ThreeManifold.HyperbolicCore.phi_action line 18
  2. lemma OAI.ThreeManifold.HyperbolicCore.psi_action line 21
  3. def OAI.ThreeManifold.HyperbolicCore.phiInv line 24
  4. def OAI.ThreeManifold.HyperbolicCore.psiInv line 25
  5. lemma OAI.ThreeManifold.HyperbolicCore.phi_inv_eq line 26
  6. lemma OAI.ThreeManifold.HyperbolicCore.psi_inv_eq line 31
  7. lemma OAI.ThreeManifold.HyperbolicCore.phi_inv_action line 36
  8. lemma OAI.ThreeManifold.HyperbolicCore.psi_inv_action line 39
  9. lemma OAI.ThreeManifold.HyperbolicCore.phi_maps_right line 43
  10. lemma OAI.ThreeManifold.HyperbolicCore.psi_maps_left line 59
  11. lemma OAI.ThreeManifold.HyperbolicCore.phi_inv_maps_outside line 75
  12. lemma OAI.ThreeManifold.HyperbolicCore.psi_inv_maps_outside line 92
  13. def OAI.ThreeManifold.HyperbolicCore.pairingGenerator line 109
  14. def OAI.ThreeManifold.HyperbolicCore.pairingX line 110
  15. def OAI.ThreeManifold.HyperbolicCore.pairingY line 113
  16. lemma OAI.ThreeManifold.HyperbolicCore.pairingX_nonempty line 117
  17. lemma OAI.ThreeManifold.HyperbolicCore.pairingX_disjoint line 126
  18. lemma OAI.ThreeManifold.HyperbolicCore.pairingY_disjoint line 142
  19. lemma OAI.ThreeManifold.HyperbolicCore.pairingXY_disjoint line 145
  20. lemma OAI.ThreeManifold.HyperbolicCore.pairing_maps_X line 152
  21. lemma OAI.ThreeManifold.HyperbolicCore.pairing_maps_Y line 157
  22. theorem OAI.ThreeManifold.HyperbolicCore.pairing_free line 163
  23. lemma OAI.ThreeManifold.HyperbolicCore.pairingGenerator_mem line 168
  24. def OAI.ThreeManifold.HyperbolicCore.effectiveGenerator line 173
  25. lemma OAI.ThreeManifold.HyperbolicCore.effectiveGenerator_smul line 174
  26. lemma OAI.ThreeManifold.HyperbolicCore.effectiveGenerator_inv_smul line 176
  27. theorem OAI.ThreeManifold.HyperbolicCore.effective_pairing_free line 179
  28. lemma OAI.ThreeManifold.HyperbolicCore.effect_neg_one line 193
  29. def OAI.ThreeManifold.HyperbolicCore.permutationLift line 200
  30. lemma OAI.ThreeManifold.HyperbolicCore.gamma_permutation_mem_range line 203
  31. theorem OAI.ThreeManifold.HyperbolicCore.effective_pairing_surjective line 228
  32. def OAI.ThreeManifold.HyperbolicCore.effectiveFreeEquiv line 234
  33. def OAI.ThreeManifold.HyperbolicCore.surfaceFundamentalGroupEquiv line 238
  34. def OAI.ThreeManifold.HyperbolicCore.horoline line 250
  35. lemma OAI.ThreeManifold.HyperbolicCore.horoline_continuous line 251
  36. lemma OAI.ThreeManifold.HyperbolicCore.horoline_one line 255
  37. def OAI.ThreeManifold.HyperbolicCore.boundaryPath line 261
  38. def OAI.ThreeManifold.HyperbolicCore.boundaryClass line 267
  39. lemma OAI.ThreeManifold.HyperbolicCore.boundaryClass_effect line 270
  40. lemma OAI.ThreeManifold.HyperbolicCore.peripheral_effect line 284
  41. theorem OAI.ThreeManifold.HyperbolicCore.boundaryClass_commutator line 296
  42. def OAI.ThreeManifold.LoopTopology.pair line 316
  43. lemma OAI.ThreeManifold.LoopTopology.pair_mul line 318
  44. lemma OAI.ThreeManifold.LoopTopology.pair_one line 321
  45. lemma OAI.ThreeManifold.LoopTopology.pair_commute line 325
  46. lemma OAI.ThreeManifold.LoopTopology.pair_split line 329
  47. def OAI.ThreeManifold.LoopTopology.leftHom line 332
  48. lemma OAI.ThreeManifold.LoopTopology.map_trans line 337
  49. lemma OAI.ThreeManifold.LoopTopology.fiber_null_transfer line 344
  50. lemma OAI.ThreeManifold.LoopTopology.loop_cast_eq_one_iff line 370
  51. lemma OAI.ThreeManifold.LoopTopology.mapOfEq_eq_one_iff line 374
  52. def OAI.ThreeManifold.GluedConstruction.clippedPiece line 388
  53. lemma OAI.ThreeManifold.GluedConstruction.clippedPiece_continuous line 392
  54. def OAI.ThreeManifold.GluedConstruction.blockMap line 395
  55. lemma OAI.ThreeManifold.GluedConstruction.clippedPiece_fixed line 397
  56. def OAI.ThreeManifold.GluedConstruction.boundarySurface line 403
  57. lemma OAI.ThreeManifold.GluedConstruction.boundarySurface_continuous line 405
  58. lemma OAI.ThreeManifold.GluedConstruction.boundarySurface_height line 407
  59. lemma OAI.ThreeManifold.GluedConstruction.boundarySurface_horoline line 410
  60. def OAI.ThreeManifold.GluedConstruction.torusPoint line 419
  61. lemma OAI.ThreeManifold.GluedConstruction.blockMap_torus line 421
  62. lemma OAI.ThreeManifold.GluedConstruction.gluing_torus line 426
  63. lemma OAI.ThreeManifold.GluedConstruction.blockMap_torus_shear line 435
  64. abbrev OAI.ThreeManifold.GluedConstruction.baseSurface line 445
  65. abbrev OAI.ThreeManifold.GluedConstruction.wholeBase line 446
  66. def OAI.ThreeManifold.GluedConstruction.basePoint line 447
  67. lemma OAI.ThreeManifold.GluedConstruction.boundarySurface_zero line 448
  68. lemma OAI.ThreeManifold.GluedConstruction.blockMap_base line 449
  69. def OAI.ThreeManifold.GluedConstruction.circlePath line 456
  70. def OAI.ThreeManifold.GluedConstruction.circleClass line 462
  71. def OAI.ThreeManifold.GluedConstruction.blockHom line 464
  72. def OAI.ThreeManifold.GluedConstruction.surfaceHom line 466
  73. def OAI.ThreeManifold.GluedConstruction.fiberClass line 468
  74. def OAI.ThreeManifold.GluedConstruction.boundaryImage line 470
  75. lemma OAI.ThreeManifold.GluedConstruction.fiber_commutes_surface line 472
  76. lemma OAI.ThreeManifold.GluedConstruction.boundaryImage_commutator line 475
  77. lemma OAI.ThreeManifold.GluedConstruction.blockHom_mk line 488
  78. lemma OAI.ThreeManifold.GluedConstruction.shear_fiber line 492
  79. lemma OAI.ThreeManifold.GluedConstruction.shear_boundary line 503
  80. lemma OAI.ThreeManifold.GluedConstruction.fibers_commute line 517
  81. theorem OAI.ThreeManifold.GluedConstruction.actual_loop_relations line 521