OAI/AlgebraicGeometry/NumericalDimension/ProjectiveCoordinates.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Projective Coordinates.

  1. lemma OAI.NumericalDimensionOne.ord_positive_of_nonunit line 16
  2. lemma OAI.NumericalDimensionOne.pullback_section_orders line 29
  3. lemma OAI.NumericalDimensionOne.exists_affine_nonzero_vanishing_section line 69
  4. lemma OAI.NumericalDimensionOne.exists_birational_local_equation line 102
  5. lemma OAI.NumericalDimensionOne.order_pow line 137
  6. lemma OAI.NumericalDimensionOne.exists_birational_local_equation_dominating line 146
  7. lemma OAI.NumericalDimensionOne.exists_positive_exceptional_weight line 177
  8. lemma OAI.NumericalDimensionOne.surfaceIntersection_supported_eq line 238
  9. lemma OAI.NumericalDimensionOne.weighted_symmetric_quadratic_le line 263
  10. lemma OAI.NumericalDimensionOne.negative_row_quadratic_bound line 309
  11. lemma OAI.NumericalDimensionOne.partialIso_extending_injOn line 345
  12. lemma OAI.NumericalDimensionOne.finite_contracted_primes line 359
  13. lemma OAI.NumericalDimensionOne.exceptional_uniform_negative_square line 392
  14. lemma OAI.NumericalDimensionOne.surface_fixed_square_from_ample line 442
  15. def OAI.NumericalDimensionOne.projectiveChartConstants line 506
  16. lemma OAI.NumericalDimensionOne.projectiveChartRatio_self line 509
  17. lemma OAI.NumericalDimensionOne.projectiveChart_eval_homogeneous line 517
  18. lemma OAI.NumericalDimensionOne.projectiveChart_hom_reconstruct line 563