OAI/AlgebraicGeometry/SectionFields/EffectiveSystems.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Complete linear systems, rational maps and geometric effective-base definitions.

  1. structure OAI.RelativeDenominators.EffectiveBase.ComplexVariety line 17
  2. instance OAI.RelativeDenominators.EffectiveBase.ComplexVariety.(instance at line 29) line 29
  3. def OAI.RelativeDenominators.EffectiveBase.ComplexVariety.IsNormal line 34
  4. def OAI.RelativeDenominators.EffectiveBase.ComplexVariety.scalarMap line 38
  5. instance OAI.RelativeDenominators.EffectiveBase.ComplexVariety.stalkComplexAlgebra line 43
  6. instance OAI.RelativeDenominators.EffectiveBase.ComplexVariety.functionFieldComplexAlgebra line 46
  7. instance OAI.RelativeDenominators.EffectiveBase.ComplexVariety.stalkFunctionFieldTower line 50
  8. def OAI.RelativeDenominators.EffectiveBase.projectiveSpace line 69
  9. def OAI.RelativeDenominators.EffectiveBase.constantToDegreeZero line 73
  10. def OAI.RelativeDenominators.EffectiveBase.projectiveSpaceStructural line 81
  11. def OAI.RelativeDenominators.EffectiveBase.ComplexVariety.IsProjective line 87
  12. def OAI.RelativeDenominators.EffectiveBase.IsProjectiveMorphism line 92
  13. structure OAI.RelativeDenominators.EffectiveBase.Contraction line 98
  14. def OAI.RelativeDenominators.EffectiveBase.rationalize line 108
  15. def OAI.RelativeDenominators.EffectiveBase.exteriorPullback line 112
  16. abbrev OAI.RelativeDenominators.EffectiveBase.RationalTopForms line 122
  17. def OAI.RelativeDenominators.EffectiveBase.RegularAt line 127
  18. def OAI.RelativeDenominators.EffectiveBase.IsDivisorOfForm line 135
  19. structure OAI.RelativeDenominators.EffectiveBase.BirationalModel line 143
  20. def OAI.RelativeDenominators.EffectiveBase.fieldPullback line 157
  21. def OAI.RelativeDenominators.EffectiveBase.IsLogCanonical line 167
  22. def OAI.RelativeDenominators.EffectiveBase.CoefficientsIn line 179
  23. def OAI.RelativeDenominators.EffectiveBase.sectionSpace line 184
  24. def OAI.RelativeDenominators.EffectiveBase.IsBig line 191
  25. def OAI.RelativeDenominators.EffectiveBase.IsSectionBasis line 197
  26. def OAI.RelativeDenominators.EffectiveBase.coordinatesEvaluation line 205
  27. theorem OAI.RelativeDenominators.EffectiveBase.coordinates_irrelevant_eq_top line 213
  28. def OAI.RelativeDenominators.EffectiveBase.projectiveGenericPoint line 229
  29. def OAI.RelativeDenominators.EffectiveBase.IsCompleteSystemMap line 237
  30. def OAI.RelativeDenominators.EffectiveBase.BirationallyEquivalentMaps line 249
  31. def OAI.RelativeDenominators.EffectiveBase.IsIitakaFibration line 261
  32. def OAI.RelativeDenominators.EffectiveBase.RecoversBaseAndIitaka line 273