OAI/GroupTheory/FiniteType/SingularChains.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingularChains.zeroAugmentation line 11
  2. instance OAI.SingularChains.zeroAugmentation_isIso line 15
  3. lemma OAI.SingularChains.zeroAugmentation_natural line 18
  4. abbrev OAI.CWEquivariant.object line 49
  5. def OAI.CWEquivariant.differential line 50
  6. lemma OAI.CWEquivariant.differential_comp line 52
  7. def OAI.CWEquivariant.complex line 59
  8. lemma OAI.CWEquivariant.complex_exactAt line 62
  9. def OAI.CWEquivariant.onSpace line 76
  10. lemma OAI.CWEquivariant.augmentation_natural line 80
  11. def OAI.CWEquivariant.augLinear line 93
  12. lemma OAI.CWEquivariant.augLinear_smul line 98
  13. def OAI.CWEquivariant.aug line 111
  14. lemma OAI.CWEquivariant.d_aug line 116
  15. lemma OAI.CWEquivariant.aug_epi line 126
  16. lemma OAI.CWEquivariant.aug_exact line 133
  17. abbrev OAI.RegularProductR.Module line 159
  18. def OAI.RegularProductR.rightShift line 161
  19. lemma OAI.RegularProductR.rightShift_single line 164
  20. lemma OAI.RegularProductR.rightShift_one line 168
  21. lemma OAI.RegularProductR.rightShift_mul line 173
  22. def OAI.RegularProductR.representation line 179
  23. abbrev OAI.RegularProductR.rep line 192
  24. lemma OAI.ProductCriterion.rightShift_eq_mul line 201
  25. def OAI.ProductCriterion.evalPair line 211
  26. lemma OAI.ProductCriterion.evalPair_invariant line 215
  27. def OAI.ProductCriterion.coordinate line 228
  28. lemma OAI.ProductCriterion.coordinate_mk_tmul line 238
  29. lemma OAI.ProductCriterion.coordinates_finite_span line 242
  30. lemma OAI.ProductCriterion.map_asAlgebraHom line 269
  31. def OAI.ProductCriterion.tensorMap line 276
  32. lemma OAI.ProductCriterion.coordinate_natural line 280
  33. lemma OAI.ProductCriterion.free_algebra_action line 297
  34. lemma OAI.ProductCriterion.coordinate_free_inverse_single line 302
  35. lemma OAI.ProductCriterion.coordinate_free_inverse_apply line 315
  36. lemma OAI.ProductCriterion.free_coordinates_injective line 328
  37. lemma OAI.ProductCriterion.free_coordinates_surjective line 344
  38. def OAI.ProductCriterion.moduleMap line 359
  39. lemma OAI.ProductCriterion.moduleMap_apply line 362
  40. lemma OAI.ProductCriterion.kernel_fg_of_product_exact line 365
  41. lemma OAI.ProductCriterion.kernel_fg_of_tensor_homology_zero line 408
  42. lemma OAI.ProductCriterion.product_resolution_exact line 420