OAI/RingTheory/BassTrace/ChainMaps.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Alternating functions on vertex labels act on oriented exterior chains.

  1. def OAI.BassTrace.ChainHomotopy.vertexMap line 17
  2. def OAI.BassTrace.ChainHomotopy.relabel line 19
  3. lemma OAI.BassTrace.ChainHomotopy.vertexMap_single line 22
  4. lemma OAI.BassTrace.ChainHomotopy.relabel_wedge line 26
  5. lemma OAI.BassTrace.Fundamental.term_eq_sorted line 41
  6. def OAI.BassTrace.Fundamental.simplexMap line 56
  7. lemma OAI.BassTrace.Fundamental.simplexMap_range line 64
  8. lemma OAI.BassTrace.Fundamental.chain_relabel line 75
  9. def OAI.BassTrace.Sparse.restrictComplex line 93
  10. lemma OAI.BassTrace.Sparse.restrictComplex_le line 104
  11. lemma OAI.BassTrace.Sparse.restrictComplex_finite line 107
  12. lemma OAI.BassTrace.Fundamental.faceChain_eq_restrict line 121
  13. theorem OAI.BassTrace.Fundamental.boundary_chain_restrictions line 132
  14. lemma OAI.BassTrace.Fundamental.faces_one_of_space_singleton line 146
  15. theorem OAI.BassTrace.Fundamental.augmentation_chain line 169
  16. instance OAI.BassTrace.Oriented.(instance at line 198) line 198
  17. structure OAI.BassTrace.ChainHomotopy.Complex line 217
  18. def OAI.BassTrace.ChainHomotopy.Complex.chains line 222
  19. lemma OAI.BassTrace.ChainHomotopy.Complex.wedge_mem line 226
  20. lemma OAI.BassTrace.ChainHomotopy.Complex.d_mem line 230
  21. lemma OAI.BassTrace.ChainHomotopy.Complex.coneLift_fills line 248
  22. def OAI.BassTrace.ChainHomotopy.homotopy line 261
  23. lemma OAI.BassTrace.ChainHomotopy.homotopy_equation line 266
  24. lemma OAI.BassTrace.ChainHomotopy.vertexMap_average line 302
  25. lemma OAI.BassTrace.ChainHomotopy.augmentation_vertexMap line 306
  26. lemma OAI.BassTrace.ChainHomotopy.relabel_coe line 315
  27. lemma OAI.BassTrace.ChainHomotopy.relabel_cone line 328
  28. lemma OAI.BassTrace.ChainHomotopy.d_relabel line 333
  29. lemma OAI.BassTrace.ChainHomotopy.relabel_id line 340
  30. lemma OAI.BassTrace.ChainHomotopy.relabel_comp line 345
  31. lemma OAI.BassTrace.ChainHomotopy.coneLift_natural line 351
  32. lemma OAI.BassTrace.ChainHomotopy.homotopy_natural line 362
  33. def OAI.BassTrace.ChainHomotopy.exteriorRepresentation line 384
  34. def OAI.BassTrace.ChainHomotopy.Complex.IsInvariant line 397
  35. lemma OAI.BassTrace.ChainHomotopy.Complex.relabel_mem line 400
  36. def OAI.BassTrace.ChainHomotopy.Complex.subrepresentation line 413
  37. abbrev OAI.BassTrace.ChainHomotopy.Complex.representation line 418
  38. def OAI.BassTrace.ChainHomotopy.Complex.relations line 422
  39. lemma OAI.BassTrace.ChainHomotopy.coinvariant_cocycle_comparison line 427