OAI/AlgebraicGeometry/Seshadri/Blowup/Gluing.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MaximalSeshadri.BlowupGluing.baseCover line 14
  2. abbrev OAI.MaximalSeshadri.BlowupGluing.localCentre line 18
  3. abbrev OAI.MaximalSeshadri.BlowupGluing.localScheme line 20
  4. abbrev OAI.MaximalSeshadri.BlowupGluing.localProjection line 23
  5. lemma OAI.MaximalSeshadri.BlowupGluing.local_isBlowup line 26
  6. lemma OAI.MaximalSeshadri.BlowupGluing.centre_transition line 30
  7. lemma OAI.MaximalSeshadri.BlowupGluing.local_invertible line 36
  8. def OAI.MaximalSeshadri.BlowupGluing.transition line 43
  9. lemma OAI.MaximalSeshadri.BlowupGluing.transition_projection line 48
  10. lemma OAI.MaximalSeshadri.BlowupGluing.transition_id line 52
  11. lemma OAI.MaximalSeshadri.BlowupGluing.transition_comp line 57
  12. def OAI.MaximalSeshadri.BlowupGluing.diagram line 64
  13. def OAI.MaximalSeshadri.BlowupGluing.diagramMap line 70
  14. lemma OAI.MaximalSeshadri.BlowupGluing.diagramMap_equifibered line 74
  15. def OAI.MaximalSeshadri.BlowupGluing.gluing line 85
  16. abbrev OAI.MaximalSeshadri.BlowupGluing.scheme line 90
  17. abbrev OAI.MaximalSeshadri.BlowupGluing.projection line 91
  18. abbrev OAI.MaximalSeshadri.BlowupGluing.cover line 92
  19. lemma OAI.MaximalSeshadri.BlowupGluing.cover_projection line 95
  20. lemma OAI.MaximalSeshadri.BlowupGluing.local_pullback line 99
  21. lemma OAI.MaximalSeshadri.BlowupGluing.projection_invertible line 111
  22. lemma OAI.MaximalSeshadri.BlowupGluing.test_invertible line 119
  23. lemma OAI.MaximalSeshadri.BlowupGluing.hom_ext line 128
  24. theorem OAI.MaximalSeshadri.BlowupGluing.universal line 150
  25. theorem OAI.MaximalSeshadri.BlowupGluing.isBlowup line 186
  26. lemma OAI.MaximalSeshadri.InvertibleLocal.regular_map_flat line 196
  27. lemma OAI.MaximalSeshadri.InvertibleLocal.invertible_flat_pullback line 206
  28. lemma OAI.MaximalSeshadri.Geometry.IsBlowup.flat_baseChange line 237
  29. lemma OAI.MaximalSeshadri.Geometry.IsBlowup.flat_baseChangeSquare line 257
  30. lemma OAI.MaximalSeshadri.ReesGrading.generators_adjoin_of_span line 279
  31. lemma OAI.MaximalSeshadri.ReesGrading.generators_adjoin_zero_of_span line 298
  32. lemma OAI.MaximalSeshadri.ReesGrading.iSup_basicOpen_of_span line 314
  33. def OAI.MaximalSeshadri.ReesGrading.generatorCover line 320