OAI/GroupTheory/FiniteType/SingularSubdivisionIterate.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingularSubdivision.iterate line 13
  2. lemma OAI.SingularSubdivision.realize_subdiv line 19
  3. lemma OAI.SingularSubdivision.realize_iterate line 26
  4. lemma OAI.SingularSubdivision.iterate_map line 35
  5. lemma OAI.SingularSubdivision.iterate_generator line 44
  6. lemma OAI.SmallChains.affine_small line 59
  7. lemma OAI.SmallChains.eventually_generator_small line 72
  8. def OAI.SmallChains.eventuallySmall line 98
  9. theorem OAI.SmallChains.eventually_small line 110
  10. lemma OAI.SmallChains.iterate_mem line 117
  11. def OAI.SmallChains.obj line 128
  12. def OAI.SmallChains.boundary line 132
  13. lemma OAI.SmallChains.boundary_val line 138
  14. lemma OAI.SmallChains.boundary_sq line 141
  15. def OAI.SmallChains.complex line 149
  16. def OAI.SmallChains.inclusion line 151
  17. lemma OAI.SmallChains.inclusion_apply line 160
  18. lemma OAI.SingularSubdivision.iterate_comm line 168
  19. def OAI.SingularSubdivision.sumPrism line 176
  20. lemma OAI.SingularSubdivision.sumPrism_zero line 182
  21. lemma OAI.SingularSubdivision.iterate_zero line 187
  22. lemma OAI.SingularSubdivision.sumPrism_boundary line 192
  23. lemma OAI.SmallChains.sumPrism_mem line 210
  24. abbrev OAI.ModuleHomology.Cycles line 223
  25. def OAI.ModuleHomology.classMap line 225
  26. lemma OAI.ModuleHomology.classMap_surjective line 228
  27. lemma OAI.ModuleHomology.classMap_zero_iff line 233
  28. lemma OAI.ModuleHomology.classMap_eq_iff line 246
  29. def OAI.ModuleHomology.cyclesMap line 253
  30. lemma OAI.ModuleHomology.cyclesMap_i line 262
  31. lemma OAI.ModuleHomology.cyclesMap_eq line 265
  32. lemma OAI.ModuleHomology.classMap_natural line 271
  33. lemma OAI.ModuleHomology.homologyMap_class line 277
  34. lemma OAI.ModuleHomology.homologyMap_surjective line 281
  35. lemma OAI.ModuleHomology.homologyMap_injective line 292