OAI/RepresentationTheory/GraphModels/Bundles.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Projective Hilbert bundles and exact induction.

  1. structure OAI.GermBundles.ScalarCocycle line 12
  2. structure OAI.GermBundles.ProjectiveBundle line 26
  3. def OAI.GermBundles.Intertwines line 40
  4. theorem OAI.GermBundles.relabel_pi_apply line 52
  5. theorem OAI.GermBundles.relabel_pi_right line 62
  6. def OAI.GermBundles.relabel line 72
  7. theorem OAI.GermBundles.relabel_apply line 116
  8. theorem OAI.GermBundles.relabel_single line 122
  9. structure OAI.GermBundles.FibreSystem line 145
  10. def OAI.GermBundles.FibreSystem.toBundle line 153
  11. def OAI.GermBundles.ScalarCocycle.restrict line 196
  12. structure OAI.GermBundles.ProjectiveRepresentation line 202
  13. structure OAI.GermBundles.CosetSection line 210
  14. def OAI.GermBundles.chooseCosetSection line 215
  15. def OAI.GermBundles.CosetSection.correction line 225
  16. theorem OAI.GermBundles.CosetSection.correction_val line 231
  17. theorem OAI.GermBundles.CosetSection.repr_mul_correction line 234
  18. theorem OAI.GermBundles.CosetSection.correction_one line 239
  19. theorem OAI.GermBundles.CosetSection.correction_mul line 244
  20. def OAI.GermBundles.CosetSection.phase line 250
  21. theorem OAI.GermBundles.CosetSection.phase_one line 253
  22. theorem OAI.GermBundles.cocycle_transport_phase line 257
  23. theorem OAI.GermBundles.CosetSection.phase_mul line 279
  24. def OAI.GermBundles.circleUnitary line 291
  25. theorem OAI.GermBundles.circleUnitary_apply line 301
  26. def OAI.GermBundles.CosetSection.inducedUnitary line 303
  27. theorem OAI.GermBundles.CosetSection.inducedUnitary_apply line 307
  28. theorem OAI.GermBundles.CosetSection.inducedUnitary_one line 311
  29. theorem OAI.GermBundles.CosetSection.inducedUnitary_mul line 316
  30. def OAI.GermBundles.CosetSection.change line 326
  31. theorem OAI.GermBundles.CosetSection.repr_mul_change line 329
  32. theorem OAI.GermBundles.CosetSection.change_correction line 333
  33. theorem OAI.GermBundles.cocycle_change_phase line 339
  34. def OAI.GermBundles.CosetSection.changeUnitary line 361
  35. theorem OAI.GermBundles.CosetSection.changeUnitary_apply line 366
  36. theorem OAI.GermBundles.CosetSection.change_phase line 371
  37. theorem OAI.GermBundles.CosetSection.changeUnitary_intertwines line 382
  38. def OAI.GermBundles.CosetSection.inducedFibreSystem line 407
  39. def OAI.GermBundles.CosetSection.inducedBundle line 416
  40. theorem OAI.GermBundles.CosetSection.inducedBundle_single line 421
  41. def OAI.GermBundles.CosetSection.changeBundleUnitary line 427
  42. theorem OAI.GermBundles.CosetSection.changeBundleUnitary_single line 432
  43. theorem OAI.GermBundles.CosetSection.changeBundleUnitary_intertwines line 438
  44. theorem OAI.GermBundles.exact_projective_induction line 460