OAI/RingTheory/Multiplicity/AlternatingCechAlt.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Lech.AlternatingCech.Alt line 20
  2. abbrev OAI.Lech.AlternatingCech.basis line 21
  3. def OAI.Lech.AlternatingCech.evaluation line 22
  4. lemma OAI.Lech.AlternatingCech.evaluation_injective line 27
  5. def OAI.Lech.AlternatingCech.epsilon line 33
  6. lemma OAI.Lech.AlternatingCech.epsilon_basis line 34
  7. def OAI.Lech.AlternatingCech.delta line 37
  8. lemma OAI.Lech.AlternatingCech.evaluation_delta line 49
  9. def OAI.Lech.AlternatingCech.extra line 61
  10. lemma OAI.Lech.AlternatingCech.evaluation_extra line 66
  11. lemma OAI.Lech.AlternatingCech.delta_square line 74
  12. lemma OAI.Lech.AlternatingCech.extra_delta line 77
  13. lemma OAI.Lech.AlternatingCech.eq_zero_above_card line 85
  14. def OAI.Lech.AlternatingCech.cochains line 93
  15. lemma OAI.Lech.AlternatingCech.delta_mem line 96
  16. theorem OAI.Lech.AlternatingCech.exact line 106
  17. def OAI.Lech.AlternatingCech.differential line 133
  18. lemma OAI.Lech.AlternatingCech.differential_square line 135
  19. def OAI.Lech.AlternatingCech.complex line 141
  20. lemma OAI.Lech.AlternatingCech.complex_d line 148
  21. lemma OAI.Lech.AlternatingCech.complex_bounded line 153
  22. lemma OAI.Lech.AlternatingCech.complex_exactAt line 160
  23. lemma OAI.Lech.AlternatingCech.extra_delta_zero line 173
  24. lemma OAI.Lech.AlternatingCech.differential_injective line 183
  25. lemma OAI.Lech.AlternatingCech.complex_exactAt_zero line 203
  26. theorem OAI.Lech.AlternatingCech.complex_acyclic line 214
  27. def OAI.Lech.AlternatingCech.sortedCoordinates line 229
  28. lemma OAI.Lech.AlternatingCech.sortedCoordinates_apply line 232
  29. lemma OAI.Lech.AlternatingCech.tuple_sort line 239
  30. lemma OAI.Lech.AlternatingCech.sorted_intersection line 258
  31. lemma OAI.Lech.AlternatingCech.mem_cochains_iff_sorted line 267
  32. def OAI.Lech.AlternatingCech.cochainsSorted line 292
  33. def OAI.Lech.AlternatingCech.vertexMap line 315
  34. lemma OAI.Lech.AlternatingCech.vertexMap_basis line 318
  35. def OAI.Lech.AlternatingCech.pullback line 320
  36. lemma OAI.Lech.AlternatingCech.pullback_eval line 325
  37. lemma OAI.Lech.AlternatingCech.pullback_delta line 330
  38. def OAI.Lech.AlternatingCech.prism line 342
  39. lemma OAI.Lech.AlternatingCech.prism_succ line 350
  40. lemma OAI.Lech.AlternatingCech.pullback_zero line 358
  41. lemma OAI.Lech.AlternatingCech.pullback_extra_sorted_zero line 363
  42. lemma OAI.Lech.AlternatingCech.prism_identity_step line 377
  43. lemma OAI.Lech.AlternatingCech.prism_identity line 406
  44. lemma OAI.Lech.AlternatingCech.sortedCoordinates_eq_evaluation line 422
  45. lemma OAI.Lech.AlternatingCech.evaluation_mem_of_sorted line 425
  46. lemma OAI.Lech.AlternatingCech.prism_local line 441
  47. lemma OAI.Lech.AlternatingCech.prism_mem line 479