OAI/AlgebraicGeometry/NumericalDimension/SectionCoordinates.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Section Coordinates.

  1. lemma OAI.NumericalDimensionOne.homogeneous_eval₂_scale line 18
  2. def OAI.NumericalDimensionOne.homogeneousAwayEval line 35
  3. lemma OAI.NumericalDimensionOne.homogeneousAwayEval_mk_mul line 39
  4. lemma OAI.NumericalDimensionOne.homogeneousAwayEval_postcomp line 54
  5. lemma OAI.NumericalDimensionOne.homogeneousAwayEval_awayMap line 66
  6. lemma OAI.NumericalDimensionOne.homogeneousAwayEval_fromZero line 80
  7. lemma OAI.NumericalDimensionOne.homogeneousAwayEval_awayMap' line 88
  8. lemma OAI.NumericalDimensionOne.homogeneousAwayEval_scale line 101
  9. lemma OAI.NumericalDimensionOne.homogeneous_chart_morphism_eq line 135
  10. lemma OAI.NumericalDimensionOne.generated_finite_section_cover line 170
  11. lemma OAI.NumericalDimensionOne.cartier_section_basicOpen line 189
  12. structure OAI.NumericalDimensionOne.DivisorProjectiveChart line 210
  13. lemma OAI.NumericalDimensionOne.exists_divisorProjectiveChart line 228
  14. lemma OAI.NumericalDimensionOne.openScalar_generic line 257
  15. lemma OAI.NumericalDimensionOne.openScalar_toSpec line 268
  16. def OAI.NumericalDimensionOne.DivisorProjectiveChart.normalized line 286
  17. lemma OAI.NumericalDimensionOne.DivisorProjectiveChart.normalized_index line 289
  18. def OAI.NumericalDimensionOne.DivisorProjectiveChart.toMorphism line 293
  19. lemma OAI.NumericalDimensionOne.DivisorProjectiveChart.toMorphism_over line 297
  20. lemma OAI.NumericalDimensionOne.DivisorProjectiveChart.generic_normalized line 301
  21. lemma OAI.NumericalDimensionOne.DivisorProjectiveChart.toMorphism_generic line 314
  22. lemma OAI.NumericalDimensionOne.DivisorProjectiveChart.toMorphism_preimage line 323
  23. def OAI.NumericalDimensionOne.DivisorProjectiveChart.toPartialMap line 343
  24. lemma OAI.NumericalDimensionOne.DivisorProjectiveChart.toPartialMap_generic line 353
  25. lemma OAI.NumericalDimensionOne.DivisorProjectiveChart.toRationalMap_eq line 358
  26. lemma OAI.NumericalDimensionOne.covering_partialMaps_extend line 368
  27. theorem OAI.NumericalDimensionOne.generated_cartier_defines_projective_morphism line 402
  28. lemma OAI.NumericalDimensionOne.exists_affine_divisorProjectiveChart line 459
  29. lemma OAI.NumericalDimensionOne.opens_topIso_inv_restrict line 495
  30. lemma OAI.NumericalDimensionOne.divisorProjectiveChart_normalized_transition line 506