OAI/RepresentationTheory/ProjectiveInduction/CosetTransport.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

Projective coset transport and subgroup graph orbit calculations.

  1. structure OAI.TwistedCorrespondences.ScalarCocycle line 13
  2. instance OAI.TwistedCorrespondences.ScalarCocycle.(instance at line 24) line 24
  3. theorem OAI.TwistedCorrespondences.ScalarCocycle.one_left line 26
  4. theorem OAI.TwistedCorrespondences.ScalarCocycle.one_right line 27
  5. theorem OAI.TwistedCorrespondences.ScalarCocycle.cocycle line 29
  6. theorem OAI.TwistedCorrespondences.ScalarCocycle.ext line 32
  7. def OAI.TwistedCorrespondences.ScalarCocycle.trivial line 38
  8. theorem OAI.TwistedCorrespondences.ScalarCocycle.trivial_apply line 44
  9. def OAI.TwistedCorrespondences.ScalarCocycle.pullback line 46
  10. theorem OAI.TwistedCorrespondences.ScalarCocycle.pullback_apply line 52
  11. def OAI.TwistedCorrespondences.ScalarCocycle.mul line 55
  12. theorem OAI.TwistedCorrespondences.ScalarCocycle.mul_apply line 67
  13. def OAI.TwistedCorrespondences.ScalarCocycle.inv line 70
  14. theorem OAI.TwistedCorrespondences.ScalarCocycle.inv_apply line 77
  15. theorem OAI.TwistedCorrespondences.ScalarCocycle.inv_apply_coe line 80
  16. def OAI.TwistedCorrespondences.ScalarCocycle.joint line 83
  17. theorem OAI.TwistedCorrespondences.ScalarCocycle.joint_apply line 86
  18. theorem OAI.TwistedCorrespondences.ScalarCocycle.joint_apply_coe line 90
  19. theorem OAI.TwistedCorrespondences.ScalarCocycle.joint_mixed line 95
  20. theorem OAI.TwistedCorrespondences.ScalarCocycle.joint_mixed_rev line 98
  21. def OAI.TwistedCorrespondences.ScalarCocycle.matchedRatio line 101
  22. theorem OAI.TwistedCorrespondences.ScalarCocycle.matchedRatio_apply line 105
  23. structure OAI.TwistedCorrespondences.ProjectiveUnitaryRepresentation line 111
  24. def OAI.TwistedCorrespondences.ProjectiveUnitaryRepresentation.pullback line 122
  25. def OAI.TwistedCorrespondences.ProjectiveUnitaryRepresentation.joint line 128
  26. def OAI.TwistedCorrespondences.graphHom line 149
  27. theorem OAI.TwistedCorrespondences.graphHom_apply line 152
  28. def OAI.TwistedCorrespondences.graphSubgroup line 155
  29. theorem OAI.TwistedCorrespondences.mem_graphSubgroup line 158
  30. theorem OAI.TwistedCorrespondences.graph_kernel_left line 161
  31. theorem OAI.TwistedCorrespondences.graph_kernel_right line 168
  32. theorem OAI.TwistedCorrespondences.graph_map_fst line 174
  33. theorem OAI.TwistedCorrespondences.graph_map_snd line 185
  34. theorem OAI.TwistedCorrespondences.joint_pullback_graph line 197
  35. theorem OAI.TwistedCorrespondences.graph_multiplier line 203
  36. theorem OAI.TwistedCorrespondences.exists_graph_of_coordinate_kernels line 215
  37. theorem OAI.TwistedCorrespondences.stabilizer_is_graph line 263
  38. theorem OAI.TwistedCorrespondences.graph_cosets_free_left line 279
  39. theorem OAI.TwistedCorrespondences.graph_cosets_free_right line 297
  40. def OAI.TwistedCorrespondences.leftCosetOrbitRel line 315
  41. theorem OAI.TwistedCorrespondences.leftCosetOrbitRel_iff line 319
  42. def OAI.TwistedCorrespondences.sndCosetProjection line 322
  43. theorem OAI.TwistedCorrespondences.sndCosetProjection_mk line 329
  44. theorem OAI.TwistedCorrespondences.sndCosetProjection_smul line 333
  45. theorem OAI.TwistedCorrespondences.sndCosetProjection_eq_iff line 342
  46. def OAI.TwistedCorrespondences.leftCosetOrbitEquiv line 365
  47. theorem OAI.TwistedCorrespondences.graph_left_orbit_count line 384
  48. theorem OAI.TwistedCorrespondences.snd_finiteIndex_of_finite_orbits line 391
  49. def OAI.TwistedCorrespondences.rightCosetOrbitRel line 398
  50. theorem OAI.TwistedCorrespondences.rightCosetOrbitRel_iff line 402
  51. def OAI.TwistedCorrespondences.fstCosetProjection line 405
  52. theorem OAI.TwistedCorrespondences.fstCosetProjection_mk line 412
  53. theorem OAI.TwistedCorrespondences.fstCosetProjection_smul line 416
  54. theorem OAI.TwistedCorrespondences.fstCosetProjection_eq_iff line 425
  55. def OAI.TwistedCorrespondences.rightCosetOrbitEquiv line 448
  56. theorem OAI.TwistedCorrespondences.graph_right_orbit_count line 467
  57. theorem OAI.TwistedCorrespondences.fst_finiteIndex_of_finite_orbits line 474
  58. theorem OAI.TwistedCorrespondences.finiteIndex_graph_of_coordinate_kernels line 481
  59. theorem OAI.TwistedCorrespondences.ScalarCocycle.induction_scalar line 497
  60. def OAI.TwistedCorrespondences.circleSmul line 526
  61. theorem OAI.TwistedCorrespondences.circleSmul_apply line 536
  62. structure OAI.TwistedCorrespondences.CosetSection line 539
  63. def OAI.TwistedCorrespondences.CosetSection.choose line 547
  64. def OAI.TwistedCorrespondences.CosetSection.correction line 557
  65. theorem OAI.TwistedCorrespondences.CosetSection.correction_coe line 565
  66. theorem OAI.TwistedCorrespondences.CosetSection.correction_one line 568
  67. theorem OAI.TwistedCorrespondences.CosetSection.correction_mul line 573
  68. def OAI.TwistedCorrespondences.CosetSection.transportScalar line 579
  69. theorem OAI.TwistedCorrespondences.CosetSection.transportScalar_one line 582
  70. theorem OAI.TwistedCorrespondences.CosetSection.transportScalar_mul line 586
  71. def OAI.TwistedCorrespondences.CosetSection.transport line 604
  72. theorem OAI.TwistedCorrespondences.CosetSection.transport_apply line 609
  73. theorem OAI.TwistedCorrespondences.CosetSection.transport_one line 615
  74. theorem OAI.TwistedCorrespondences.CosetSection.transport_mul line 621