OAI/RingTheory/BassTrace/ExteriorChains.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Alternating functions on vertex labels extend to genuine linear maps on exterior chains.

  1. abbrev OAI.BassTrace.Chains.contraction line 16
  2. lemma OAI.BassTrace.Chains.contraction_square line 19
  3. lemma OAI.BassTrace.Chains.contraction_one line 23
  4. lemma OAI.BassTrace.Chains.contraction_ι line 27
  5. lemma OAI.BassTrace.Chains.contraction_ι_mul line 31
  6. lemma OAI.BassTrace.Chains.cone_contraction line 36
  7. lemma OAI.BassTrace.Chains.contraction_map line 42
  8. lemma OAI.BassTrace.Chains.contraction_ιMulti_succ line 54
  9. lemma OAI.BassTrace.Chains.contraction_ιMulti line 62
  10. lemma OAI.BassTrace.Chains.contraction_mem_exteriorPower line 84
  11. abbrev OAI.BassTrace.Chains.Vectors line 109
  12. abbrev OAI.BassTrace.Chains.Algebra line 111
  13. abbrev OAI.BassTrace.Chains.Degree line 113
  14. def OAI.BassTrace.Chains.augmentation line 115
  15. def OAI.BassTrace.Chains.boundary line 118
  16. lemma OAI.BassTrace.Chains.augmentation_single line 121
  17. lemma OAI.BassTrace.Chains.boundary_square line 125
  18. lemma OAI.BassTrace.Chains.vertex_contraction line 128
  19. lemma OAI.BassTrace.Chains.exists_filler line 133
  20. abbrev OAI.BassTrace.Oriented.Degree line 155
  21. def OAI.BassTrace.Oriented.wedge line 157
  22. lemma OAI.BassTrace.Oriented.wedge_perm line 160
  23. lemma OAI.BassTrace.Oriented.wedge_eq_zero_of_not_injective line 165
  24. structure OAI.BassTrace.Oriented.AltFunction line 171
  25. instance OAI.BassTrace.Oriented.(instance at line 176) line 176
  26. abbrev OAI.BassTrace.Oriented.basis line 181
  27. lemma OAI.BassTrace.Oriented.basis_eq_wedge line 184
  28. lemma OAI.BassTrace.Oriented.exists_sorted_perm line 189
  29. def OAI.BassTrace.Oriented.AltFunction.lift line 211
  30. lemma OAI.BassTrace.Oriented.AltFunction.lift_wedge line 214
  31. lemma OAI.BassTrace.Oriented.linearMap_ext_wedge line 223
  32. lemma OAI.BassTrace.Oriented.span_wedges line 230
  33. def OAI.BassTrace.ChainHomotopy.average line 248
  34. lemma OAI.BassTrace.ChainHomotopy.average_perm line 251
  35. lemma OAI.BassTrace.ChainHomotopy.average_augmentation line 257
  36. def OAI.BassTrace.ChainHomotopy.cone line 261
  37. lemma OAI.BassTrace.ChainHomotopy.cone_coe line 269
  38. def OAI.BassTrace.ChainHomotopy.d line 272
  39. lemma OAI.BassTrace.ChainHomotopy.d_coe line 276
  40. lemma OAI.BassTrace.ChainHomotopy.d_square line 279
  41. lemma OAI.BassTrace.ChainHomotopy.d_cone_cycle line 283
  42. def OAI.BassTrace.ChainHomotopy.coneFunction line 293
  43. def OAI.BassTrace.ChainHomotopy.coneLift line 304
  44. lemma OAI.BassTrace.ChainHomotopy.coneLift_wedge line 307
  45. lemma OAI.BassTrace.ChainHomotopy.d_coneLift line 312
  46. lemma OAI.BassTrace.ChainHomotopy.d_wedge line 323