OAI/GroupTheory/GroupCohomology/CyclicResidue.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Nonzero cyclic cohomology classes in a Laurent monomial line.

  1. abbrev OAI.LowerSphereCyclic.Cyclic line 11
  2. def OAI.LowerSphereCyclic.sigma line 13
  3. def OAI.LowerSphereCyclic.residueKappa line 15
  4. lemma OAI.LowerSphereCyclic.residueKappa_mul line 18
  5. def OAI.LowerSphereCyclic.cyclicCochain line 25
  6. lemma OAI.LowerSphereCyclic.cyclicCochain_is_cocycle line 31
  7. lemma OAI.LowerSphereCyclic.sigma_pow_p line 44
  8. lemma OAI.LowerSphereCyclic.residueKappa_sigma line 48
  9. lemma OAI.LowerSphereCyclic.residueKappa_sigma_pow line 52
  10. lemma OAI.LowerSphereCyclic.cyclicCochain_at_sigma line 57
  11. lemma OAI.LowerSphereCyclic.cyclicCochain_sum line 66
  12. lemma OAI.LowerSphereCyclic.coboundary_sum line 74
  13. lemma OAI.LowerSphereCyclic.cyclicCochain_not_coboundary line 84
  14. theorem OAI.LowerSphereCyclic.cyclic_detection line 96
  15. def OAI.LowerSphereCyclic.binomialCocycle line 104
  16. def OAI.LowerSphereCyclic.binomialClass line 109
  17. theorem OAI.LowerSphereCyclic.binomialClass_ne_zero line 114
  18. def OAI.LowerSphereCyclic.residueLine line 121
  19. def OAI.LowerSphereCyclic.residueLineMap line 124
  20. def OAI.LowerSphereCyclic.firstResidue line 127
  21. def OAI.LowerSphereCyclic.gradedCochain line 130
  22. lemma OAI.LowerSphereCyclic.residueLineMap_val line 135
  23. def OAI.LowerSphereCyclic.residueLineCoeff line 140
  24. lemma OAI.LowerSphereCyclic.residueLineCoeff_map line 145
  25. lemma OAI.LowerSphereCyclic.gradedCochain_val line 151
  26. lemma OAI.LowerSphereCyclic.gradedCochain_coeff line 173
  27. lemma OAI.LowerSphereCyclic.gradedCochain_is_cocycle line 178
  28. lemma OAI.LowerSphereCyclic.gradedCochain_not_coboundary line 189
  29. theorem OAI.LowerSphereCyclic.cyclic_residue_detection line 203
  30. def OAI.LowerSphereCyclic.gradedBinomialCocycle line 220
  31. def OAI.LowerSphereCyclic.gradedBinomialClass line 226
  32. theorem OAI.LowerSphereCyclic.gradedBinomialClass_ne_zero line 232