OAI/NumberTheory/PiExponent/LocalAlgebra/FiniteGlobalPresentation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.PiExponent.FiniteGlobalPresentation.presentation_map_isFinite line 22
  2. def OAI.PiExponent.FiniteGlobalPresentation.presentationOfIso line 33
  3. theorem OAI.PiExponent.FiniteGlobalPresentation.isFinitePresentation_of_presentation line 40
  4. theorem OAI.PiExponent.FiniteGlobalPresentation.tilde_exists_finitePresentation line 49
  5. theorem OAI.PiExponent.FiniteGlobalPresentation.tilde_finitePresentation line 67
  6. theorem OAI.PiExponent.FiniteGlobalPresentation.spec_kernel_isQuasicoherent line 72
  7. theorem OAI.PiExponent.FiniteGlobalPresentation.spec_exists_finitePresentation_of_sections line 94
  8. theorem OAI.PiExponent.FiniteGlobalPresentation.spec_kernel_exists_finitePresentation line 105
  9. def OAI.PiExponent.FiniteGlobalPresentation.presentationOver_of_restrict line 119
  10. instance OAI.PiExponent.FiniteGlobalPresentation.presentationOver_of_restrict_isFinite line 132
  11. theorem OAI.PiExponent.FiniteGlobalPresentation.isFinitePresentation_of_affine_presentations line 137
  12. theorem OAI.PiExponent.FiniteGlobalPresentation.affine_kernel_exists_finitePresentation line 161
  13. theorem OAI.PiExponent.FiniteGlobalPresentation.free_isFinitePresentation line 191
  14. theorem OAI.PiExponent.FiniteGlobalPresentation.kernel_isFinitePresentation line 207
  15. theorem OAI.PiExponent.FiniteGlobalPresentation.kernel_generators_isFinitePresentation line 223
  16. theorem OAI.PiExponent.FiniteGlobalPresentation.exists_local_finitePresentation line 230
  17. theorem OAI.PiExponent.FiniteGlobalPresentation.isFinitePresentation_of_localPresentations line 250
  18. theorem OAI.PiExponent.FiniteGlobalPresentation.finitePresentation_of_le line 272
  19. def OAI.PiExponent.FiniteGlobalPresentation.restrictIsoOfLE line 287
  20. theorem OAI.PiExponent.FiniteGlobalPresentation.isFinitePresentation_of_locally_iso line 296
  21. theorem OAI.PiExponent.FiniteGlobalPresentation.moduleTwist_isFinitePresentation line 310