OAI/AlgebraicGeometry/NumericalDimension/CanonicalExistence.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Canonical Existence.

  1. theorem OAI.NumericalDimensionOne.exists_canonicalDivisor_of_smooth line 18
  2. lemma OAI.NumericalDimensionOne.basis_singleton_coordinate_isUnit line 99
  3. lemma OAI.NumericalDimensionOne.canonical_local_order_unique line 120
  4. theorem OAI.NumericalDimensionOne.canonicalDivisorOf_unique line 167
  5. theorem OAI.NumericalDimensionOne.isCartier_of_isCanonical line 190
  6. lemma OAI.NumericalDimensionOne.canonicalModel_isCartier line 245
  7. def OAI.NumericalDimensionOne.smoothCanonicalClass line 250
  8. instance OAI.NumericalDimensionOne.partialIsoSourceNonempty line 257
  9. instance OAI.NumericalDimensionOne.partialIsoTargetNonempty line 260
  10. instance OAI.NumericalDimensionOne.partialIsoSourceDominant line 263
  11. instance OAI.NumericalDimensionOne.partialIsoTargetDominant line 267
  12. def OAI.NumericalDimensionOne.CompatibleCanonicalData line 273
  13. def OAI.NumericalDimensionOne.NoExtractionOn line 281
  14. def OAI.NumericalDimensionOne.IsKDivisorialContraction line 284
  15. def OAI.NumericalDimensionOne.IsKFlip line 294
  16. def OAI.NumericalDimensionOne.IsCanonicalMMPStep line 308
  17. inductive OAI.NumericalDimensionOne.CanonicalMMPChain line 315
  18. def OAI.NumericalDimensionOne.canonicalModelOfSmooth line 331
  19. def OAI.NumericalDimensionOne.HasEffectiveCanonicalComparison line 348
  20. def OAI.NumericalDimensionOne.HasMinimalModel line 365
  21. theorem OAI.NumericalDimensionOne.normal_birational_quasiFinite_local_bijective line 381
  22. def OAI.NumericalDimensionOne.openImmersionFunctionFieldEquiv line 445
  23. def OAI.NumericalDimensionOne.partialIsoFunctionFieldEquiv line 454
  24. lemma OAI.NumericalDimensionOne.dominantFunctionFieldMap_comp_apply line 462
  25. lemma OAI.NumericalDimensionOne.dominantFunctionFieldMap_id_apply line 484
  26. lemma OAI.NumericalDimensionOne.partialIso_dominantFunctionFieldMap line 497
  27. theorem OAI.NumericalDimensionOne.birational_quasiFinite_stalk_coheight line 513