OAI/GroupTheory/PeriodicGroups/Homology/FiniteNormalHomology.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SourceBurnside.Stability.FiniteNormal.averageEnd line 15
2. lemma OAI.SourceBurnside.Stability.FiniteNormal.averageEnd_natural line 30
3. lemma OAI.SourceBurnside.Stability.FiniteNormal.averageEnd_trivial line 35
4. def OAI.SourceBurnside.Stability.FiniteNormal.averageChain line 47
5. lemma OAI.SourceBurnside.Stability.FiniteNormal.averageChain_π line 51
6. def OAI.SourceBurnside.Stability.FiniteNormal.averageHomotopy line 62
7. lemma OAI.SourceBurnside.Stability.FiniteNormal.averageBalanced line 67
8. lemma OAI.SourceBurnside.Stability.FiniteNormal.averageTensor_zero line 86
9. theorem OAI.SourceBurnside.Stability.FiniteNormal.homology_isZero line 93
10. lemma OAI.SourceBurnside.Stability.FiniteNormal.averageEnd_zero_of_neg line 107
11. abbrev OAI.SourceBurnside.Stability.scalarRep line 125
12. lemma OAI.SourceBurnside.Stability.SignHomology.isZero_of_finite_normal line 134
13. lemma OAI.SourceBurnside.Stability.SignHomology.isZero_of_quotient line 144
14. lemma OAI.SourceBurnside.Stability.SignHomology.product_isZero line 152
15. abbrev OAI.SourceBurnside.Stability.FrameStabilizer.V line 176
16. abbrev OAI.SourceBurnside.Stability.FrameStabilizer.G line 177
17. abbrev OAI.SourceBurnside.Stability.FrameStabilizer.rho line 178
18. lemma OAI.SourceBurnside.Stability.FrameStabilizer.independent_action line 180
19. abbrev OAI.SourceBurnside.Stability.FrameStabilizer.index line 184
20. abbrev OAI.SourceBurnside.Stability.FrameStabilizer.A line 188
21. abbrev OAI.SourceBurnside.Stability.FrameStabilizer.b line 190
22. abbrev OAI.SourceBurnside.Stability.FrameStabilizer.right line 191
23. def OAI.SourceBurnside.Stability.FrameStabilizer.base line 193
24. lemma OAI.SourceBurnside.Stability.FrameStabilizer.base_coe line 201
25. lemma OAI.SourceBurnside.Stability.FrameStabilizer.stabilizer_eq line 204
26. def OAI.SourceBurnside.Stability.FrameStabilizer.stabilizerEquiv line 218
27. lemma OAI.SourceBurnside.Stability.FrameStabilizer.monomial line 221
28. abbrev OAI.SourceBurnside.Stability.FrameStabilizer.characterS line 225
29. def OAI.SourceBurnside.Stability.FrameStabilizer.characterK line 226
30. lemma OAI.SourceBurnside.Stability.FrameStabilizer.characterK_spec line 229
31. lemma OAI.SourceBurnside.Stability.FrameStabilizer.perm_kernel_character line 239
32. lemma OAI.SourceBurnside.Stability.FrameStabilizer.transitive line 258
33. def OAI.SourceBurnside.Stability.FrameStabilizer.characterP line 295
34. lemma OAI.SourceBurnside.Stability.FrameStabilizer.characterP_comp line 300
35. lemma OAI.SourceBurnside.Stability.FrameStabilizer.characterP_swap line 307
36. lemma OAI.SourceBurnside.Stability.FrameStabilizer.characterK_homology_isZero line 344
37. lemma OAI.SourceBurnside.Stability.FrameStabilizer.characterS_homology_isZero line 360
38. lemma OAI.SourceBurnside.Stability.FrameStabilizer.chains_homology_isZero line 372
39. abbrev OAI.SourceBurnside.Stability.H2FrameEdge.chains line 397
40. def OAI.SourceBurnside.Stability.H2FrameEdge.augmentation line 400
41. lemma OAI.SourceBurnside.Stability.H2FrameEdge.chains_acyclic line 405
42. lemma OAI.SourceBurnside.Stability.H2FrameEdge.augmentation_isIso line 423
43. def OAI.SourceBurnside.Stability.MonomialTrivial.scalarIso line 456
44. def OAI.SourceBurnside.Stability.MonomialTrivial.seed line 461
45. def OAI.SourceBurnside.Stability.MonomialTrivial.induced line 472
46. lemma OAI.SourceBurnside.Stability.MonomialTrivial.induced_mk line 475
47. lemma OAI.SourceBurnside.Stability.MonomialTrivial.scalar_property line 481
48. lemma OAI.SourceBurnside.Stability.MonomialTrivial.indMap_mk line 485
49. lemma OAI.SourceBurnside.Stability.MonomialTrivial.scalar_comp line 489
50. lemma OAI.SourceBurnside.Stability.MonomialTrivial.induced_isIso line 510
51. lemma OAI.SourceBurnside.Stability.MonomialTrivial.seed_homology_isIso line 521
52. def OAI.SourceBurnside.Stability.UnorderedStabilizer.complementary line 552
53. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.complementary_val line 566
54. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.projection_complementary line 573
55. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.projection_surjective line 578
56. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.projection_kernel_eq line 585
57. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.projection_locallyFinite line 591
58. lemma OAI.SourceBurnside.Stability.UnorderedStabilizer.complementary_homology_isIso line 596
59. lemma OAI.SourceBurnside.Stability.trivial_map_factorization line 614
60. lemma OAI.SourceBurnside.Stability.SingletonFrameEdge.base_singleton line 649
61. lemma OAI.SourceBurnside.Stability.SingletonFrameEdge.fixed line 652
62. abbrev OAI.SourceBurnside.Stability.SingletonFrameEdge.seed line 667
63. def OAI.SourceBurnside.Stability.SingletonFrameEdge.lift line 669
64. def OAI.SourceBurnside.Stability.SingletonFrameEdge.blockHom line 673
65. lemma OAI.SourceBurnside.Stability.SingletonFrameEdge.blockHom_val line 675
66. lemma OAI.SourceBurnside.Stability.SingletonFrameEdge.seed_augmentation line 678
67. lemma OAI.SourceBurnside.Stability.SingletonFrameEdge.lift_homology_isIso line 688
68. lemma OAI.SourceBurnside.Stability.SingletonFrameEdge.seed_homology_isIso line 695
69. lemma OAI.SourceBurnside.Stability.SingletonFrameEdge.composite line 699
70. lemma OAI.SourceBurnside.Stability.SingletonFrameEdge.block_h2_isIso line 706