OAI/GroupTheory/FiniteType/QuotientComplex.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuotientComplex.obj line 16
  2. def OAI.QuotientComplex.differential line 18
  3. lemma OAI.QuotientComplex.differential_mk line 21
  4. lemma OAI.QuotientComplex.differential_shape line 24
  5. lemma OAI.QuotientComplex.differential_comp line 33
  6. def OAI.QuotientComplex.complex line 46
  7. def OAI.QuotientComplex.projection line 52
  8. lemma OAI.QuotientComplex.projection_apply line 59
  9. lemma OAI.QuotientComplex.projection_surjective line 61
  10. lemma OAI.QuotientComplex.projection_zero_iff line 64
  11. def OAI.QuotientComplex.map line 79
  12. lemma OAI.QuotientComplex.map_projection line 88
  13. lemma OAI.SingularSupport.sub_cut_mem line 98
  14. lemma OAI.SingularSubspace.group_mono line 115
  15. lemma OAI.SingularSubspace.group_eq_small line 118
  16. lemma OAI.SingularSubspace.boundary_mem line 124
  17. lemma OAI.SingularSubspace.iterate_mem line 133
  18. lemma OAI.SingularSubspace.sumPrism_mem line 138
  19. lemma OAI.SingularSubspace.map_mem line 143
  20. lemma OAI.SingularSubspace.lift_mem line 152
  21. lemma OAI.SingularSubspace.lift_inclusion_apply line 164
  22. lemma OAI.SingularSubspace.inclusion_lift_apply line 170
  23. lemma OAI.SingularSubspace.inclusion_mem_iff line 174
  24. lemma OAI.SingularSubspace.lift_boundary line 181
  25. def OAI.RelativeChains.complex line 199
  26. def OAI.RelativeChains.projection line 203
  27. lemma OAI.RelativeChains.projection_surjective line 207
  28. lemma OAI.RelativeChains.projection_zero_iff line 210
  29. lemma OAI.RelativeChains.differential_projection line 214
  30. def OAI.RelativeChains.map line 217
  31. lemma OAI.RelativeChains.map_projection line 220
  32. def OAI.RelativeChains.inclusion line 224
  33. lemma OAI.RelativeChains.projection_eq_iff line 232
  34. lemma OAI.RelativeChains.inclusion_projection line 236
  35. lemma OAI.RelativeChains.inclusion_injective line 240
  36. lemma OAI.RelativeChains.cycle_difference line 248
  37. lemma OAI.RelativeChains.iterate_projection_eq line 265