OAI/AlgebraicGeometry/NumericalDimension/BirationalExtension.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Birational Extension.

  1. theorem OAI.NumericalDimensionOne.extend_generic_section line 15
  2. theorem OAI.NumericalDimensionOne.isIso_restrict_of_dominant_section line 43
  3. theorem OAI.NumericalDimensionOne.isIso_near_valuation_of_generic_section line 73
  4. theorem OAI.NumericalDimensionOne.isIso_near_codim_one_of_proper_birational line 108
  5. theorem OAI.NumericalDimensionOne.isIso_restrict_iSup line 152
  6. theorem OAI.NumericalDimensionOne.exists_codim_one_partialIso_of_proper_birational line 173
  7. lemma OAI.NumericalDimensionOne.dominant_fromSpecStalk line 218
  8. theorem OAI.NumericalDimensionOne.birational_isIso_stalk_of_quasiFiniteAt line 238
  9. theorem OAI.NumericalDimensionOne.isIso_near_of_proper_birational_quasiFiniteAt line 273
  10. theorem OAI.NumericalDimensionOne.isIso_of_proper_birational_locallyQuasiFinite line 295
  11. lemma OAI.NumericalDimensionOne.stalk_iso_of_restrict_iso line 313
  12. theorem OAI.NumericalDimensionOne.exists_unique_prime_over_of_proper_birational line 321
  13. lemma OAI.NumericalDimensionOne.generic_stalk_algebraMap_surjective line 367
  14. lemma OAI.NumericalDimensionOne.birational_generic_fiber line 370
  15. def OAI.NumericalDimensionOneCurveAux.complexProjectiveSpace line 412
  16. def OAI.NumericalDimensionOneCurveAux.projectiveConstants line 415
  17. def OAI.NumericalDimensionOneCurveAux.complexProjectiveSpaceMap line 423
  18. def OAI.NumericalDimensionOneCurveAux.IsComplexProjective line 428
  19. structure OAI.NumericalDimensionOneCurveAux.ComplexProjectiveVariety line 432
  20. def OAI.NumericalDimensionOneCurveAux.IsSmoothNfold line 441
  21. theorem OAI.NumericalDimensionOneCurveAux.projectiveConstants_bijective line 444
  22. theorem OAI.NumericalDimensionOneCurveAux.complexProjectiveSpace_isProper line 454
  23. theorem OAI.NumericalDimensionOneCurveAux.isProper_of_isComplexProjective line 474