OAI/GroupTheory/SimpleAmenable/Simplicial/DiagonalResolution.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DiagonalResolution.D line 8
  2. abbrev OAI.DiagonalResolution.A line 9
  3. abbrev OAI.DiagonalResolution.Z line 10
  4. abbrev OAI.DiagonalResolution.free line 11
  5. def OAI.DiagonalResolution.pre line 13
  6. lemma OAI.DiagonalResolution.ι_pre line 20
  7. lemma OAI.DiagonalResolution.pre_id line 25
  8. lemma OAI.DiagonalResolution.pre_comp line 32
  9. def OAI.DiagonalResolution.preDiag line 42
  10. def OAI.DiagonalResolution.chains line 45
  11. def OAI.DiagonalResolution.augmentation line 52
  12. def OAI.DiagonalResolution.augmented line 69
  13. def OAI.DiagonalResolution.complex line 74
  14. instance OAI.DiagonalResolution.projective line 77
  15. def OAI.DiagonalResolution.zeroSimplex line 83
  16. lemma OAI.DiagonalResolution.shift_δ₀ line 85
  17. lemma OAI.DiagonalResolution.shift_δ_succ line 91
  18. lemma OAI.DiagonalResolution.shift_σ_succ line 97
  19. lemma OAI.DiagonalResolution.shift_δ₁ line 103
  20. abbrev OAI.DiagonalResolution.augmentedAt line 109
  21. def OAI.DiagonalResolution.extraAt line 111
  22. def OAI.DiagonalResolution.pi line 155
  23. def OAI.DiagonalResolution.atIso line 158
  24. def OAI.DiagonalResolution.singleAtIso line 164
  25. instance OAI.DiagonalResolution.pi_quasiIso line 170
  26. def OAI.DiagonalResolution.resolution line 191