OAI/NumberTheory/PiExponent/Cohomology/CechHigher.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.GeometrySupport.CechHigher.intersection line 20
  2. theorem OAI.PiExponent.GeometrySupport.CechHigher.intersectionLE line 22
  3. theorem OAI.PiExponent.GeometrySupport.CechHigher.faceLE line 26
  4. abbrev OAI.PiExponent.GeometrySupport.CechHigher.Cochain line 30
  5. def OAI.PiExponent.GeometrySupport.CechHigher.differential line 33
  6. def OAI.PiExponent.GeometrySupport.CechHigher.HasPrimitives line 37
  7. theorem OAI.PiExponent.GeometrySupport.CechHigher.restrictHom_refl line 41
  8. theorem OAI.PiExponent.GeometrySupport.CechHigher.restrictHom_sum line 47
  9. theorem OAI.PiExponent.GeometrySupport.CechHigher.restrictHom_zsmul line 52
  10. def OAI.PiExponent.GeometrySupport.CechHigher.evaluate line 57
  11. theorem OAI.PiExponent.GeometrySupport.CechHigher.evaluate_differential line 62
  12. theorem OAI.PiExponent.GeometrySupport.CechHigher.differential_squared line 74
  13. def OAI.PiExponent.GeometrySupport.CechHigher.map line 85
  14. theorem OAI.PiExponent.GeometrySupport.CechHigher.map_differential line 88
  15. theorem OAI.PiExponent.GeometrySupport.CechHigher.differential_zero line 95
  16. theorem OAI.PiExponent.GeometrySupport.CechHigher.differential_sub line 101
  17. theorem OAI.PiExponent.GeometrySupport.CechHigher.map_zero line 106
  18. theorem OAI.PiExponent.GeometrySupport.CechHigher.map_sub line 111
  19. theorem OAI.PiExponent.GeometrySupport.CechHigher.map_injective line 117
  20. theorem OAI.PiExponent.GeometrySupport.CechHigher.lift_cochain line 123
  21. theorem OAI.PiExponent.GeometrySupport.CechHigher.lift_kernel_cochain line 134
  22. theorem OAI.PiExponent.GeometrySupport.CechHigher.connecting_cocycle line 143
  23. theorem OAI.PiExponent.GeometrySupport.CechHigher.primitives_of_shortExact line 161
  24. theorem OAI.PiExponent.GeometrySupport.CechHigher.insertLE line 181
  25. def OAI.PiExponent.GeometrySupport.CechHigher.contraction line 189
  26. theorem OAI.PiExponent.GeometrySupport.CechHigher.restrict_cochain_congr line 193
  27. theorem OAI.PiExponent.GeometrySupport.CechHigher.contraction_differential line 200
  28. theorem OAI.PiExponent.GeometrySupport.CechHigher.hasPrimitives_of_containing_member line 223
  29. theorem OAI.PiExponent.GeometrySupport.CechHigher.hasPrimitives_on_chart line 235
  30. def OAI.PiExponent.GeometrySupport.CechHigher.sectionZero line 241
  31. theorem OAI.PiExponent.GeometrySupport.CechHigher.scalar_differential_zero_degree line 244
  32. theorem OAI.PiExponent.GeometrySupport.CechHigher.sectionZero_compatible line 255
  33. theorem OAI.PiExponent.GeometrySupport.CechHigher.glue_zero_cocycle line 291
  34. def OAI.PiExponent.GeometrySupport.CechHigher.augmentation line 299
  35. theorem OAI.PiExponent.GeometrySupport.CechHigher.augmentation_closed line 303
  36. theorem OAI.PiExponent.GeometrySupport.CechHigher.sectionZero_augmentation line 316
  37. theorem OAI.PiExponent.GeometrySupport.CechHigher.shortExact_global_lift line 322
  38. theorem OAI.PiExponent.GeometrySupport.CechHigher.ext_one_eq_zero line 349
  39. theorem OAI.PiExponent.GeometrySupport.CechHigher.ext_succ_eq_zero_of_injective_cech line 366
  40. abbrev OAI.PiExponent.GeometrySupport.CechHigher.schemeFreeOpen line 397
  41. theorem OAI.PiExponent.GeometrySupport.CechHigher.affine_ext_succ_eq_zero_of_injective_cech line 402