OAI/NumberTheory/PiExponent/Ampleness/CoherentAffineFinite.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.CoherentAffineFinite.epi_iso_comp_iso line 10
  2. theorem OAI.PiExponent.CoherentAffineFinite.finitePresentation_quasicoherent line 16
  3. theorem OAI.PiExponent.CoherentAffineFinite.spec_sections_finite_of_generators line 20
  4. theorem OAI.PiExponent.CoherentAffineFinite.affine_sections_finite_of_generators line 40
  5. def OAI.PiExponent.CoherentAffineFinite.LocallyFinitelyGenerated line 70
  6. theorem OAI.PiExponent.CoherentAffineFinite.locallyFinitelyGenerated_of_finitePresentation line 74
  7. theorem OAI.PiExponent.CoherentAffineFinite.finite_generators_of_le line 92
  8. theorem OAI.PiExponent.CoherentAffineFinite.affine_open_sections_finite_of_generators line 106
  9. theorem OAI.PiExponent.CoherentAffineFinite.spec_sections_finite_of_localGenerators line 123
  10. theorem OAI.PiExponent.CoherentAffineFinite.LocallyFinitelyGenerated.restrict line 160
  11. theorem OAI.PiExponent.CoherentAffineFinite.affine_sections_finite_of_localGenerators line 180
  12. theorem OAI.PiExponent.CoherentAffineFinite.affine_sections_finite line 205
  13. theorem OAI.PiExponent.CoherentAffineFinite.finite_isoSpec_sections line 210
  14. theorem OAI.PiExponent.CoherentAffineFinite.spec_exists_finite_generators line 239
  15. theorem OAI.PiExponent.CoherentAffineFinite.affine_exists_finite_generators line 266
  16. theorem OAI.PiExponent.CoherentAffineFinite.affine_exists_finite_generators_of_finitePresentation line 288
  17. theorem OAI.PiExponent.CoherentAffineFinite.affine_open_sections_finite line 295