OAI/GroupTheory/SimpleAmenable/Homology/PiSSet.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiSSet.obj line 13
  2. def OAI.PiSSet.proj line 18
  3. def OAI.PiSSet.lift line 21
  4. lemma OAI.PiSSet.lift_proj line 24
  5. def OAI.PiSSet.incl line 25
  6. lemma OAI.PiSSet.incl_self line 28
  7. lemma OAI.PiSSet.incl_other line 31
  8. def OAI.PiSSet.finSuccIso line 35
  9. def OAI.PiSSet.finZeroIso line 47
  10. lemma OAI.PiSSet.fin_connected line 54
  11. lemma OAI.PiSSet.finSucc_fst line 61
  12. lemma OAI.PiSSet.finSucc_snd line 63
  13. lemma OAI.PiSSet.biprod_element_ext line 65
  14. lemma OAI.PiSSet.homology_ext line 75
  15. def OAI.PiSSet.homologyPi line 115
  16. def OAI.PiSSet.homologyProj line 118
  17. lemma OAI.PiSSet.homologyProj_isIso line 122
  18. abbrev OAI.ComponentTranslation.P line 155
  19. def OAI.ComponentTranslation.repr line 156
  20. lemma OAI.ComponentTranslation.repr_component line 158
  21. abbrev OAI.ComponentTranslation.property line 159
  22. abbrev OAI.ComponentTranslation.Fiber line 160
  23. def OAI.ComponentTranslation.reprMul line 161
  24. def OAI.ComponentTranslation.reprOne line 163
  25. def OAI.ComponentTranslation.translate line 165
  26. def OAI.ComponentTranslation.translateOne line 169
  27. def OAI.ComponentTranslation.translateComp line 174
  28. lemma OAI.ComponentTranslation.homology_one line 181
  29. lemma OAI.ComponentTranslation.homology_comp line 187
  30. def OAI.ComponentTranslation.homologyDiagram line 195