OAI/GroupTheory/FiniteType/PresentationGeometryRose.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PresentationGeometry.Rose.monodromyRepresentation line 13
  2. theorem OAI.PresentationGeometry.Rose.monodromyRepresentation_generator line 19
  3. theorem OAI.PresentationGeometry.Rose.monodromyRepresentation_comp line 36
  4. theorem OAI.PresentationGeometry.Rose.freeToFundamental_injective line 46
  5. def OAI.PresentationGeometry.Rose.freeGroupEquiv line 65
  6. theorem OAI.PresentationGeometry.Rose.monodromy_word line 76
  7. def OAI.PresentationGeometry.Rose.liftedRelator line 94
  8. theorem OAI.PresentationGeometry.Rose.liftedRelator_proj line 106
  9. theorem OAI.PresentationGeometry.AttachingLoops.onCircle_naturality line 117
  10. def OAI.PresentationGeometry.AttachingLoops.boundaryCircle line 132
  11. def OAI.PresentationGeometry.AttachingLoops.liftedRelatorsOnCircle line 138
  12. def OAI.PresentationGeometry.AttachingLoops.relatorSection line 143
  13. theorem OAI.PresentationGeometry.AttachingLoops.relatorSection_proj line 146
  14. def OAI.PresentationGeometry.PresentationComplex.coveringCore line 161
  15. theorem OAI.PresentationGeometry.PresentationComplex.coveringCore_old_coordChange line 166
  16. theorem OAI.PresentationGeometry.PresentationComplex.mem_coveringCore_old line 171
  17. theorem OAI.PresentationGeometry.PresentationComplex.basepoint_mem_coveringCore line 176
  18. theorem OAI.PresentationGeometry.PresentationComplex.map_range_old_chart line 180
  19. theorem OAI.PresentationGeometry.PresentationComplex.monodromy_generator line 186
  20. def OAI.PresentationGeometry.PresentationComplex.monodromyRepresentation line 232
  21. theorem OAI.PresentationGeometry.PresentationComplex.monodromyRepresentation_generator line 237
  22. theorem OAI.PresentationGeometry.PresentationComplex.monodromyRepresentation_comp line 257
  23. theorem OAI.PresentationGeometry.PresentationComplex.presentedToFundamental_injective line 272
  24. def OAI.PresentationGeometry.PresentationComplex.presentationEquiv line 302
  25. theorem OAI.PresentationGeometry.PresentationComplex.presentationTheorem line 307
  26. def OAI.PresentationGeometry.PresentationComplex.DeckGroup line 315
  27. instance OAI.PresentationGeometry.PresentationComplex.(instance at line 316) line 316
  28. instance OAI.PresentationGeometry.PresentationComplex.(instance at line 317) line 317
  29. instance OAI.PresentationGeometry.PresentationComplex.(instance at line 318) line 318
  30. def OAI.PresentationGeometry.PresentationComplex.regularGenerators line 320
  31. theorem OAI.PresentationGeometry.PresentationComplex.lift_regularGenerators line 322
  32. theorem OAI.PresentationGeometry.PresentationComplex.regular_relators line 329
  33. def OAI.PresentationGeometry.PresentationComplex.universalCore line 334
  34. abbrev OAI.PresentationGeometry.PresentationComplex.UniversalSpace line 336
  35. def OAI.PresentationGeometry.PresentationComplex.universalBasepoint line 338
  36. theorem OAI.PresentationGeometry.PresentationComplex.universalCovering line 341
  37. theorem OAI.PresentationGeometry.PresentationComplex.universalCovering_surjective line 343
  38. theorem OAI.PresentationGeometry.PresentationComplex.regular_monodromyRepresentation line 346
  39. theorem OAI.PresentationGeometry.PresentationComplex.regular_monodromy_bijective line 360
  40. instance OAI.PresentationGeometry.PresentationComplex.universalSpace_simplyConnected line 378
  41. theorem OAI.PresentationGeometry.exists_word_presentation line 389
  42. theorem OAI.PresentationGeometry.exists_finite_presentation_start line 417