OAI/GroupTheory/PeriodicGroups/Homology/FiniteExtensions.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.Stability.QGroup line 9
  2. structure OAI.SourceBurnside.Stability.RationalExtension line 11
  3. lemma OAI.SourceBurnside.Stability.RationalExtension.inl_central line 18
  4. def OAI.SourceBurnside.Stability.RationalExtension.kernelHom line 21
  5. def OAI.SourceBurnside.Stability.RationalExtension.kernelEquiv line 26
  6. lemma OAI.SourceBurnside.Stability.RationalExtension.kernelEquiv_val line 34
  7. def OAI.SourceBurnside.Stability.RationalExtension.finiteRetraction line 39
  8. theorem OAI.SourceBurnside.Stability.RationalExtension.finiteRetraction_inl line 49
  9. def OAI.SourceBurnside.Stability.RationalExtension.finiteComplementMap line 72
  10. lemma OAI.SourceBurnside.Stability.RationalExtension.finiteComplementMap_bijective line 75
  11. def OAI.SourceBurnside.Stability.RationalExtension.finiteSplitting line 94
  12. lemma OAI.SourceBurnside.Stability.RationalExtension.inl_eq_one_of_finite_order line 102
  13. theorem OAI.SourceBurnside.Stability.RationalExtension.torsion_lift_unique line 110
  14. def OAI.SourceBurnside.Stability.RationalExtension.restrict line 128
  15. def OAI.SourceBurnside.Stability.RationalExtension.liftFinite line 162
  16. lemma OAI.SourceBurnside.Stability.RationalExtension.rightHom_liftFinite line 165
  17. lemma OAI.SourceBurnside.Stability.RationalExtension.liftFinite_finite_order line 169
  18. def OAI.SourceBurnside.Stability.RationalExtension.LocallyFinite line 174
  19. lemma OAI.SourceBurnside.Stability.RationalExtension.exists_torsion_lift line 180
  20. def OAI.SourceBurnside.Stability.RationalExtension.torsionLift line 186
  21. lemma OAI.SourceBurnside.Stability.RationalExtension.rightHom_torsionLift line 188
  22. lemma OAI.SourceBurnside.Stability.RationalExtension.torsionLift_finite_order line 191
  23. def OAI.SourceBurnside.Stability.RationalExtension.locallyFiniteSplitting line 194
  24. theorem OAI.SourceBurnside.Stability.RationalExtension.locallyFiniteSplitting_unique line 210
  25. def OAI.SourceBurnside.Stability.CentralPushout.graphHom line 234
  26. def OAI.SourceBurnside.Stability.CentralPushout.relation line 239
  27. lemma OAI.SourceBurnside.Stability.CentralPushout.relation_central line 242
  28. instance OAI.SourceBurnside.Stability.CentralPushout.relation_normal line 251
  29. def OAI.SourceBurnside.Stability.CentralPushout.Extension line 258
  30. instance OAI.SourceBurnside.Stability.CentralPushout.extensionGroup line 260
  31. def OAI.SourceBurnside.Stability.CentralPushout.canonical line 265
  32. def OAI.SourceBurnside.Stability.CentralPushout.inclusion line 266
  33. def OAI.SourceBurnside.Stability.CentralPushout.projection line 268
  34. lemma OAI.SourceBurnside.Stability.CentralPushout.projection_mk line 273
  35. lemma OAI.SourceBurnside.Stability.CentralPushout.projection_canonical line 274
  36. lemma OAI.SourceBurnside.Stability.CentralPushout.projection_inclusion line 275
  37. lemma OAI.SourceBurnside.Stability.CentralPushout.canonical_kernel line 277
  38. lemma OAI.SourceBurnside.Stability.CentralPushout.mk_pair line 285
  39. lemma OAI.SourceBurnside.Stability.CentralPushout.inclusion_injective line 291
  40. lemma OAI.SourceBurnside.Stability.CentralPushout.exactness line 304
  41. lemma OAI.SourceBurnside.Stability.CentralPushout.inclusion_central line 315
  42. def OAI.SourceBurnside.Stability.CentralPushout.extension line 325
  43. abbrev OAI.SourceBurnside.Stability.LocallyFinite line 346
  44. def OAI.SourceBurnside.Stability.FiniteAverage.average line 351
  45. lemma OAI.SourceBurnside.Stability.FiniteAverage.average_apply line 353
  46. lemma OAI.SourceBurnside.Stability.FiniteAverage.average_action line 357
  47. lemma OAI.SourceBurnside.Stability.FiniteAverage.average_ker line 364
  48. lemma OAI.SourceBurnside.Stability.FiniteAverage.mk_average line 371
  49. lemma OAI.SourceBurnside.Stability.FiniteAverage.intertwining line 377
  50. lemma OAI.SourceBurnside.Stability.FiniteAverage.map_injective line 385
  51. lemma OAI.SourceBurnside.Stability.coinvariant_finite_witness line 395
  52. lemma OAI.SourceBurnside.Stability.locallyFinite_coinvariants_injective line 413
  53. abbrev OAI.SourceBurnside.Stability.RelativeCoinvariants.functor line 446
  54. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.map_mk line 449
  55. instance OAI.SourceBurnside.Stability.RelativeCoinvariants.(instance at line 452) line 452
  56. def OAI.SourceBurnside.Stability.RelativeCoinvariants.unit line 459
  57. def OAI.SourceBurnside.Stability.RelativeCoinvariants.counit line 463
  58. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.unit_apply line 479
  59. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.counit_mk line 481
  60. def OAI.SourceBurnside.Stability.RelativeCoinvariants.adjunction line 484
  61. instance OAI.SourceBurnside.Stability.RelativeCoinvariants.(instance at line 502) line 502
  62. instance OAI.SourceBurnside.Stability.RelativeCoinvariants.(instance at line 503) line 503
  63. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.preservesMonomorphisms line 506
  64. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.preservesHomology line 514
  65. def OAI.SourceBurnside.Stability.RelativeCoinvariants.inductionIso line 529
  66. def OAI.SourceBurnside.Stability.RelativeCoinvariants.projectionRight line 534
  67. def OAI.SourceBurnside.Stability.RelativeCoinvariants.tensorSymmetry line 546
  68. def OAI.SourceBurnside.Stability.RelativeCoinvariants.projection line 551
  69. def OAI.SourceBurnside.Stability.RelativeCoinvariants.quotientProjection line 557
  70. def OAI.SourceBurnside.Stability.RelativeCoinvariants.trivialIso line 563