OAI/AlgebraicGeometry/RelativeTriviality/Cech.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CampanaPeternellSix.ActualCech.coefficientSheaf line 16
  2. abbrev OAI.CampanaPeternellSix.ActualCech.overlapModule line 26
  3. def OAI.CampanaPeternellSix.ActualCech.leftImage line 28
  4. def OAI.CampanaPeternellSix.ActualCech.rightImage line 30
  5. abbrev OAI.CampanaPeternellSix.ActualCech.quotient line 34
  6. def OAI.CampanaPeternellSix.ActualCech.leftInclusion line 40
  7. def OAI.CampanaPeternellSix.ActualCech.rightInclusion line 42
  8. lemma OAI.CampanaPeternellSix.ActualCech.isOpenImmersion_iso_inv_comp line 44
  9. instance OAI.CampanaPeternellSix.ActualCech.(instance at line 48) line 48
  10. instance OAI.CampanaPeternellSix.ActualCech.(instance at line 52) line 52
  11. lemma OAI.CampanaPeternellSix.ActualCech.left_range line 56
  12. lemma OAI.CampanaPeternellSix.ActualCech.right_range line 58
  13. lemma OAI.CampanaPeternellSix.ActualCech.left_image_overlap line 60
  14. lemma OAI.CampanaPeternellSix.ActualCech.right_image_overlap line 68
  15. lemma OAI.CampanaPeternellSix.ActualCech.actual_left_spans line 77
  16. lemma OAI.CampanaPeternellSix.ActualCech.actual_right_spans line 84
  17. lemma OAI.CampanaPeternellSix.ActualCech.scalar_overlap line 92
  18. lemma OAI.CampanaPeternellSix.ActualCech.finite_overlap line 102
  19. instance OAI.CampanaPeternellSix.ActualCech.overlapAction line 110
  20. instance OAI.CampanaPeternellSix.ActualCech.laurentAction line 114
  21. lemma OAI.CampanaPeternellSix.ActualCech.base_smul line 117
  22. instance OAI.CampanaPeternellSix.ActualCech.laurentTower line 126
  23. lemma OAI.CampanaPeternellSix.ActualCech.finite_laurent line 135
  24. lemma OAI.CampanaPeternellSix.ActualCech.laurent_span_top line 148
  25. lemma OAI.CampanaPeternellSix.ActualCech.left_laurent_spans line 166
  26. lemma OAI.CampanaPeternellSix.ActualCech.right_laurent_spans line 170
  27. lemma OAI.CampanaPeternellSix.ActualCech.left_stable line 175
  28. lemma OAI.CampanaPeternellSix.ActualCech.right_stable line 195
  29. theorem OAI.CampanaPeternellSix.ActualCech.finite_actual_cech line 215