OAI/NumberTheory/PiExponent/Ampleness/GlobalBlowupGluing.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponentSeshadri.Geometry.rees_isBlowup line 11
  2. lemma OAI.PiExponentSeshadri.IdealPullback.specIdeal_comap_toSpec line 22
  3. lemma OAI.PiExponentSeshadri.IdealPullback.comap_isoSpec_inv line 30
  4. abbrev OAI.PiExponentSeshadri.AffineBlowup.scheme line 44
  5. def OAI.PiExponentSeshadri.AffineBlowup.projection line 46
  6. theorem OAI.PiExponentSeshadri.AffineBlowup.isBlowup line 49
  7. abbrev OAI.PiExponentSeshadri.BlowupGluing.baseCover line 62
  8. abbrev OAI.PiExponentSeshadri.BlowupGluing.localCentre line 66
  9. abbrev OAI.PiExponentSeshadri.BlowupGluing.localScheme line 68
  10. abbrev OAI.PiExponentSeshadri.BlowupGluing.localProjection line 71
  11. lemma OAI.PiExponentSeshadri.BlowupGluing.local_isBlowup line 74
  12. lemma OAI.PiExponentSeshadri.BlowupGluing.centre_transition line 78
  13. lemma OAI.PiExponentSeshadri.BlowupGluing.local_invertible line 84
  14. def OAI.PiExponentSeshadri.BlowupGluing.transition line 91
  15. lemma OAI.PiExponentSeshadri.BlowupGluing.transition_projection line 96
  16. lemma OAI.PiExponentSeshadri.BlowupGluing.transition_id line 100
  17. lemma OAI.PiExponentSeshadri.BlowupGluing.transition_comp line 105
  18. def OAI.PiExponentSeshadri.BlowupGluing.diagram line 112
  19. def OAI.PiExponentSeshadri.BlowupGluing.diagramMap line 118
  20. lemma OAI.PiExponentSeshadri.BlowupGluing.diagramMap_equifibered line 122
  21. def OAI.PiExponentSeshadri.BlowupGluing.gluing line 133
  22. abbrev OAI.PiExponentSeshadri.BlowupGluing.scheme line 138
  23. abbrev OAI.PiExponentSeshadri.BlowupGluing.projection line 139
  24. abbrev OAI.PiExponentSeshadri.BlowupGluing.cover line 140
  25. lemma OAI.PiExponentSeshadri.BlowupGluing.cover_projection line 143
  26. lemma OAI.PiExponentSeshadri.BlowupGluing.local_pullback line 147
  27. lemma OAI.PiExponentSeshadri.BlowupGluing.projection_invertible line 157
  28. lemma OAI.PiExponentSeshadri.BlowupGluing.test_invertible line 165
  29. lemma OAI.PiExponentSeshadri.BlowupGluing.hom_ext line 174
  30. theorem OAI.PiExponentSeshadri.BlowupGluing.universal line 196
  31. theorem OAI.PiExponentSeshadri.BlowupGluing.isBlowup line 234