OAI/NumberTheory/PiExponent/Cohomology/CechLinear.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.GeometrySupport.CechLinear.schemeFreeOpen line 19
  2. def OAI.PiExponent.GeometrySupport.CechLinear.freeOpenHomAddCommGroup line 21
  3. def OAI.PiExponent.GeometrySupport.CechLinear.higherCochainAddCommGroup line 25
  4. def OAI.PiExponent.GeometrySupport.CechLinear.freeOpenHomModule line 32
  5. def OAI.PiExponent.GeometrySupport.CechLinear.Cochain line 38
  6. instance OAI.PiExponent.GeometrySupport.CechLinear.cochainAddCommGroup line 41
  7. instance OAI.PiExponent.GeometrySupport.CechLinear.cochainGlobalModule line 45
  8. instance OAI.PiExponent.GeometrySupport.CechLinear.cochainModule line 52
  9. def OAI.PiExponent.GeometrySupport.CechLinear.differentialLinear line 58
  10. theorem OAI.PiExponent.GeometrySupport.CechLinear.differentialLinear_apply line 89
  11. def OAI.PiExponent.GeometrySupport.CechLinear.cycles line 92
  12. theorem OAI.PiExponent.GeometrySupport.CechLinear.mem_cycles line 95
  13. def OAI.PiExponent.GeometrySupport.CechLinear.boundaryToCycles line 98
  14. theorem OAI.PiExponent.GeometrySupport.CechLinear.boundaryToCycles_val line 102
  15. def OAI.PiExponent.GeometrySupport.CechLinear.mapLinear line 108
  16. theorem OAI.PiExponent.GeometrySupport.CechLinear.mapLinear_apply line 120
  17. theorem OAI.PiExponent.GeometrySupport.CechLinear.mapLinear_comp line 123
  18. theorem OAI.PiExponent.GeometrySupport.CechLinear.mapLinear_zero line 130
  19. theorem OAI.PiExponent.GeometrySupport.CechLinear.mapLinear_differential line 137
  20. def OAI.PiExponent.GeometrySupport.CechLinear.mapCycles line 142
  21. theorem OAI.PiExponent.GeometrySupport.CechLinear.mapCycles_val line 152
  22. theorem OAI.PiExponent.GeometrySupport.CechLinear.mapCycles_boundary line 155
  23. theorem OAI.PiExponent.GeometrySupport.CechLinear.boundaryToCycles_surjective line 163
  24. def OAI.PiExponent.GeometrySupport.CechLinear.primitive line 170
  25. theorem OAI.PiExponent.GeometrySupport.CechLinear.boundaryToCycles_primitive line 175
  26. theorem OAI.PiExponent.GeometrySupport.CechLinear.primitive_spec line 182