OAI/GroupTheory/PeriodicGroups/Homology/RelativeHomology.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SourceBurnside.Stability.RelativeCoinvariants.quotientResolution line 13
2. def OAI.SourceBurnside.Stability.RelativeCoinvariants.homologyIso line 23
3. def OAI.SourceBurnside.Stability.BarMap.component line 41
4. lemma OAI.SourceBurnside.Stability.BarMap.component_single line 45
5. def OAI.SourceBurnside.Stability.BarMap.chain line 53
6. lemma OAI.SourceBurnside.Stability.BarMap.diagonal_inv_single line 82
7. lemma OAI.SourceBurnside.Stability.BarMap.augmentation_single line 102
8. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.inductionIso_one line 122
9. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.tensorSymmetry_mk line 129
10. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.tensorSymmetry_inv_mk line 133
11. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.tensor_map_mk line 137
12. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.quotientProjection_mk line 142
13. def OAI.SourceBurnside.Stability.RelativeCoinvariants.barComparisonComponent line 162
14. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.barComparisonComponent_mk line 167
15. def OAI.SourceBurnside.Stability.RelativeCoinvariants.barComparison line 170
16. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.barComparison_π line 182
17. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.barComparison_homology_isIso line 204
18. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.chainsIso_single line 225
19. def OAI.SourceBurnside.Stability.RelativeCoinvariants.projectionChain line 231
20. def OAI.SourceBurnside.Stability.RelativeCoinvariants.comparisonTensor line 236
21. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.barComparison_free line 241
22. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.tensor_comparison_free line 247
23. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.projection_single line 256
24. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.tensor_comparison_chains line 264
25. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.comparison_single line 272
26. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.quotient_chain_compare line 280
27. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.quotient_map_isIso line 300
28. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.equiv_map_isIso line 335
29. lemma OAI.SourceBurnside.Stability.RelativeCoinvariants.surjective_map_isIso line 345
30. abbrev OAI.SourceBurnside.Stability.RationalHomology.map line 372
31. lemma OAI.SourceBurnside.Stability.RationalHomology.map_id line 376
32. lemma OAI.SourceBurnside.Stability.RationalHomology.map_comp line 378
33. lemma OAI.SourceBurnside.Stability.RationalHomology.equiv_isIso line 383
34. lemma OAI.SourceBurnside.Stability.RationalHomology.surjective_isIso line 386
35. lemma OAI.SourceBurnside.Stability.VectorFactor.exists_factor line 400
36. abbrev OAI.SourceBurnside.Stability.RationalBar.T line 417
37. abbrev OAI.SourceBurnside.Stability.RationalBar.C1 line 418
38. abbrev OAI.SourceBurnside.Stability.RationalBar.C2 line 419
39. abbrev OAI.SourceBurnside.Stability.RationalBar.C3 line 420
40. abbrev OAI.SourceBurnside.Stability.RationalBar.d2 line 421
41. abbrev OAI.SourceBurnside.Stability.RationalBar.d3 line 422
42. abbrev OAI.SourceBurnside.Stability.RationalBar.Z2 line 423
43. abbrev OAI.SourceBurnside.Stability.RationalBar.B2 line 424
44. abbrev OAI.SourceBurnside.Stability.RationalBar.H2 line 425
45. abbrev OAI.SourceBurnside.Stability.RationalBar.π line 426
46. def OAI.SourceBurnside.Stability.RationalBar.Cocycles line 428
47. lemma OAI.SourceBurnside.Stability.RationalBar.cocycle_iff line 432
48. lemma OAI.SourceBurnside.Stability.RationalBar.cocycle_vanish line 433
49. lemma OAI.SourceBurnside.Stability.RationalBar.exists_evaluation line 439
50. def OAI.SourceBurnside.Stability.RationalBar.evaluation line 446
51. lemma OAI.SourceBurnside.Stability.RationalBar.evaluation_cycle line 447
52. lemma OAI.SourceBurnside.Stability.RationalBar.cocycle_of_cycle_restriction line 450
53. lemma OAI.SourceBurnside.Stability.RationalBar.evaluation_surjective line 462
54. lemma OAI.SourceBurnside.Stability.RationalBar.evaluation_zero_iff line 471
55. lemma OAI.SourceBurnside.Stability.RationalBar.evaluation_ext line 498
56. def OAI.SourceBurnside.Stability.RationalBar.evaluationMap line 504
57. abbrev OAI.SourceBurnside.Stability.RationalBar.map2 line 519
58. abbrev OAI.SourceBurnside.Stability.RationalBar.map3 line 521
59. lemma OAI.SourceBurnside.Stability.RationalBar.map2_d3 line 524
60. def OAI.SourceBurnside.Stability.RationalBar.pull line 527
61. lemma OAI.SourceBurnside.Stability.RationalBar.evaluation_natural line 535
62. lemma OAI.SourceBurnside.Stability.RationalBar.extend line 547
63. lemma OAI.SourceBurnside.Stability.RationalBar.pull_coboundary_iff line 567
64. def OAI.SourceBurnside.Stability.RationalBar.value line 585
65. lemma OAI.SourceBurnside.Stability.RationalBar.identity line 587
66. lemma OAI.SourceBurnside.Stability.RationalBar.value_one_left line 598
67. lemma OAI.SourceBurnside.Stability.RationalBar.value_one_right line 602
68. lemma OAI.SourceBurnside.Stability.RationalBar.value_inv line 606
69. def OAI.SourceBurnside.Stability.RationalBar.Extension line 611
70. instance OAI.SourceBurnside.Stability.RationalBar.extensionGroup line 613
71. def OAI.SourceBurnside.Stability.RationalBar.inclusion line 631
72. def OAI.SourceBurnside.Stability.RationalBar.projection line 639
73. def OAI.SourceBurnside.Stability.RationalBar.extension line 644
74. lemma OAI.SourceBurnside.Stability.RationalBar.pull_value line 671
75. lemma OAI.SourceBurnside.Stability.RationalBar.coboundary_value line 677
76. lemma OAI.SourceBurnside.Stability.RationalBar.relation_value line 685
77. def OAI.SourceBurnside.Stability.RationalBar.morphism line 693
78. lemma OAI.SourceBurnside.Stability.RationalBar.morphism_inclusion line 707
79. lemma OAI.SourceBurnside.Stability.RationalBar.morphism_projection line 717
80. def OAI.SourceBurnside.Stability.RationalExtension.chosenSection line 731
81. lemma OAI.SourceBurnside.Stability.RationalExtension.projection_section line 732
82. def OAI.SourceBurnside.Stability.RationalExtension.factor line 735
83. lemma OAI.SourceBurnside.Stability.RationalExtension.factor_mul line 739
84. lemma OAI.SourceBurnside.Stability.RationalExtension.factor_identity line 747
85. lemma OAI.SourceBurnside.Stability.RationalExtension.factor_one line 760
86. def OAI.SourceBurnside.Stability.RationalExtension.cochain line 764
87. lemma OAI.SourceBurnside.Stability.RationalExtension.cochain_single line 765
88. def OAI.SourceBurnside.Stability.RationalExtension.cocycle line 768
89. lemma OAI.SourceBurnside.Stability.RationalExtension.cocycle_value line 783
90. def OAI.SourceBurnside.Stability.RationalExtension.modelHom line 787
91. lemma OAI.SourceBurnside.Stability.RationalExtension.modelHom_inclusion line 801
92. lemma OAI.SourceBurnside.Stability.RationalExtension.modelHom_projection line 805
93. def OAI.SourceBurnside.Stability.RationalExtension.modelEquiv line 809