OAI/AlgebraicGeometry/NumericalDimension/CanonicalForms.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Canonical Forms.

  1. abbrev OAI.NumericalDimensionOne.rationalTopForms line 17
  2. def OAI.NumericalDimensionOne.IsCanonicalDivisorOf line 21
  3. def OAI.NumericalDimensionOne.IsCanonicalDivisor line 33
  4. def OAI.NumericalDimensionOne.divisorSupport line 47
  5. lemma OAI.NumericalDimensionOne.isClosed_divisorSupport line 51
  6. def OAI.NumericalDimensionOne.divisorComplement line 54
  7. def OAI.NumericalDimensionOne.sectionNonvanishing line 57
  8. def OAI.NumericalDimensionOne.IsAmpleDivisor line 60
  9. def OAI.NumericalDimensionOne.divisorSectionsOver line 78
  10. instance OAI.NumericalDimensionOne.projectiveVariety_proper line 98
  11. instance OAI.NumericalDimensionOne.projectiveVariety_locallyNoetherian line 101
  12. instance OAI.NumericalDimensionOne.projectiveVariety_compact line 104
  13. lemma OAI.NumericalDimensionOne.smoothNormal line 107
  14. structure OAI.NumericalDimensionOne.CurveOn line 113
  15. instance OAI.NumericalDimensionOne.curveOn_normal line 119
  16. def OAI.NumericalDimensionOne.complexWeilDegree line 122
  17. def OAI.NumericalDimensionOne.pulledCartierRepresentative line 124
  18. lemma OAI.NumericalDimensionOne.pulledCartierRepresentative_spec line 129
  19. def OAI.NumericalDimensionOne.cartierCurveDegree line 135
  20. def OAI.NumericalDimensionOne.sectionDimension line 152
  21. def OAI.NumericalDimensionOne.divisorSectionLimsup line 156
  22. def OAI.NumericalDimensionOne.kappaSigma line 159
  23. def OAI.NumericalDimensionOne.cartierNumericalVector line 165
  24. def OAI.NumericalDimensionOne.effectiveNumericalCone line 168
  25. def OAI.NumericalDimensionOne.IsPseudoEffective line 173
  26. def OAI.NumericalDimensionOne.IsNefCartier line 176
  27. abbrev OAI.NumericalDimensionOne.QWeilDivisor line 181
  28. def OAI.NumericalDimensionOne.rationalWeilDivisor line 183
  29. def OAI.NumericalDimensionOne.IsQCartierDivisor line 189
  30. def OAI.NumericalDimensionOne.IsQFactorial line 193
  31. def OAI.NumericalDimensionOne.IsAmpleQDivisor line 198
  32. def OAI.NumericalDimensionOne.IsNefQDivisor line 204
  33. def OAI.NumericalDimensionOne.IsQCartierPullback line 210
  34. lemma OAI.NumericalDimensionOne.dominantFunctionFieldMap_section line 227
  35. lemma OAI.NumericalDimensionOne.dominantFunctionFieldMap_scalar line 238
  36. def OAI.NumericalDimensionOne.rationalTopFormPullback line 250
  37. structure OAI.NumericalDimensionOne.NormalProjectiveVariety line 270
  38. def OAI.NumericalDimensionOne.IsBirationalMorphism line 275
  39. structure OAI.NumericalDimensionOne.CanonicalModel line 278
  40. def OAI.NumericalDimensionOne.IsTerminalModel line 290
  41. def OAI.NumericalDimensionOne.IsCurveContracted line 303
  42. def OAI.NumericalDimensionOne.relativeNumericalSpace line 307
  43. def OAI.NumericalDimensionOne.IsElementary line 313
  44. def OAI.NumericalDimensionOne.IsRelativelyAmpleQ line 317
  45. def OAI.NumericalDimensionOne.IsSmallMorphism line 323
  46. theorem OAI.NumericalDimensionOne.isBaseChange_of_basis line 339
  47. theorem OAI.NumericalDimensionOne.topDifferential_isBaseChange line 360
  48. theorem OAI.NumericalDimensionOne.nonempty_topDifferential_basis line 385
  49. theorem OAI.NumericalDimensionOne.nonempty_localized_topDifferential_basis line 398
  50. def OAI.NumericalDimensionOne.schemeOpenScalar line 421
  51. def OAI.NumericalDimensionOne.schemeOpenAlgebra line 426
  52. theorem OAI.NumericalDimensionOne.exists_standard_smooth_chart line 429
  53. theorem OAI.NumericalDimensionOne.open_stalk_scalar_tower line 459
  54. theorem OAI.NumericalDimensionOne.smooth_stalk_differentials_free line 487
  55. theorem OAI.NumericalDimensionOne.nonempty_smooth_canonical_stalk_basis line 507
  56. theorem OAI.NumericalDimensionOne.nonempty_smooth_canonical_field_basis line 538
  57. theorem OAI.NumericalDimensionOne.canonical_stalk_field_isBaseChange line 545
  58. theorem OAI.NumericalDimensionOne.differentialMap_comp line 574
  59. theorem OAI.NumericalDimensionOne.topDifferentialMap_comp line 584
  60. theorem OAI.NumericalDimensionOne.canonicalDivisorOf_smul line 609
  61. lemma OAI.NumericalDimensionOne.basis_singleton_repr line 636
  62. theorem OAI.NumericalDimensionOne.open_field_scalar_tower line 642