OAI/NumberTheory/PiExponent/Cohomology/CechZero.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.GeometrySupport.CechZero.sectionZero_restrict line 19
  2. theorem OAI.PiExponent.GeometrySupport.CechZero.sectionZero_injective line 30
  3. theorem OAI.PiExponent.GeometrySupport.CechZero.augmentation_injective line 35
  4. theorem OAI.PiExponent.GeometrySupport.CechZero.augmentation_exists line 44
  5. theorem OAI.PiExponent.GeometrySupport.CechZero.augmentation_comp line 54
  6. abbrev OAI.PiExponent.GeometrySupport.CechZero.schemeFreeOpen line 70
  7. def OAI.PiExponent.GeometrySupport.CechZero.augmentationLinear line 72
  8. theorem OAI.PiExponent.GeometrySupport.CechZero.augmentationLinear_val line 94
  9. def OAI.PiExponent.GeometrySupport.CechZero.sectionsEquiv line 99
  10. theorem OAI.PiExponent.GeometrySupport.CechZero.sectionsEquiv_val line 114
  11. theorem OAI.PiExponent.GeometrySupport.CechZero.sectionsEquiv_symm_restrict line 119
  12. theorem OAI.PiExponent.GeometrySupport.CechZero.sectionsEquiv_comp line 131
  13. theorem OAI.PiExponent.GeometrySupport.CechZero.sectionsEquiv_symm_mapCycles line 139