OAI/NumberTheory/PiExponent/Cohomology/ProjectiveMonomialCechHigher.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.ProjectiveMonomialCechHigher.Cochain line 17
  2. def OAI.PiExponent.ProjectiveMonomialCechHigher.differential line 19
  3. theorem OAI.PiExponent.ProjectiveMonomialCechHigher.differential_cons line 22
  4. theorem OAI.PiExponent.ProjectiveMonomialCechHigher.differential_sub line 38
  5. theorem OAI.PiExponent.ProjectiveMonomialCechHigher.differential_zero line 43
  6. theorem OAI.PiExponent.ProjectiveMonomialCechHigher.differential_squared line 48
  7. def OAI.PiExponent.ProjectiveMonomialCechHigher.Regular line 76
  8. def OAI.PiExponent.ProjectiveMonomialCechHigher.insertionSupport line 79
  9. def OAI.PiExponent.ProjectiveMonomialCechHigher.contraction line 84
  10. theorem OAI.PiExponent.ProjectiveMonomialCechHigher.contraction_apply line 92
  11. theorem OAI.PiExponent.ProjectiveMonomialCechHigher.contraction_support_subset line 97
  12. theorem OAI.PiExponent.ProjectiveMonomialCechHigher.contraction_regular line 103
  13. theorem OAI.PiExponent.ProjectiveMonomialCechHigher.differential_apply line 116
  14. theorem OAI.PiExponent.ProjectiveMonomialCechHigher.differential_regular line 121
  15. theorem OAI.PiExponent.ProjectiveMonomialCechHigher.contraction_identity line 138
  16. theorem OAI.PiExponent.ProjectiveMonomialCechHigher.exact_of_pivot line 148
  17. theorem OAI.PiExponent.ProjectiveMonomialCechHigher.nonnegative_twist_cech_exact_all_positive line 163