OAI/AlgebraicGeometry/RelativeTriviality/CechBaseChange.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CampanaPeternellSix.ActualCech.baseMap_scalars line 20
  2. def OAI.CampanaPeternellSix.ActualCech.actualUnit line 26
  3. lemma OAI.CampanaPeternellSix.ActualCech.actualUnit_isBaseChange line 39
  4. lemma OAI.CampanaPeternellSix.ActualCech.actualUnit_naturality line 56
  5. lemma OAI.CampanaPeternellSix.ActualCech.iso_ranges_top line 77
  6. lemma OAI.CampanaPeternellSix.ActualCech.trivial_ranges_top line 112
  7. lemma OAI.CampanaPeternellSix.ActualCech.left_affine line 128
  8. lemma OAI.CampanaPeternellSix.ActualCech.right_affine line 130
  9. lemma OAI.CampanaPeternellSix.ActualCech.overlap_affine line 132
  10. lemma OAI.CampanaPeternellSix.ActualCech.left_base_preimage line 138
  11. lemma OAI.CampanaPeternellSix.ActualCech.right_base_preimage line 141
  12. lemma OAI.CampanaPeternellSix.ActualCech.overlap_base_preimage line 144
  13. lemma OAI.CampanaPeternellSix.ActualCech.tensor_actual_cech_vanish_of_trivial_pullback line 150
  14. abbrev OAI.CampanaPeternellSix.ActualCech.globalModule line 187
  15. abbrev OAI.CampanaPeternellSix.ActualCech.pairModule line 188
  16. def OAI.CampanaPeternellSix.ActualCech.sectionPair line 190
  17. def OAI.CampanaPeternellSix.ActualCech.difference line 193
  18. lemma OAI.CampanaPeternellSix.ActualCech.sectionPair_injective line 196
  19. lemma OAI.CampanaPeternellSix.ActualCech.difference_sectionPair line 201
  20. lemma OAI.CampanaPeternellSix.ActualCech.sectionPair_exact line 208
  21. lemma OAI.CampanaPeternellSix.RelativeCech.left_exact_residue_baseChange line 245
  22. lemma OAI.CampanaPeternellSix.RelativeCech.isBaseChange_of_left_exact_at_prime line 307
  23. lemma OAI.CampanaPeternellSix.ActualCech.global_sections_base_change_prime_core line 334
  24. lemma OAI.CampanaPeternellSix.ActualCech.difference_range line 388
  25. lemma OAI.CampanaPeternellSix.ActualCech.flat_overlap_base line 408
  26. lemma OAI.CampanaPeternellSix.ActualCech.difference_surjective_of_cech_zero line 430
  27. theorem OAI.CampanaPeternellSix.ActualCech.global_sections_base_change_at_trivial_fiber line 448