OAI/AlgebraicGeometry/NumericalDimension/SurfaceSquare.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Surface Square.

  1. lemma OAI.NumericalDimensionOne.projective_coordinate_cover line 17
  2. lemma OAI.NumericalDimensionOne.projectiveAffineMap_coords_injective line 26
  3. lemma OAI.NumericalDimensionOne.projectiveAffineMap_preimage_homogeneous line 43
  4. lemma OAI.NumericalDimensionOne.projectiveField_coordinates line 61
  5. lemma OAI.NumericalDimensionOne.projectiveLocal_coordinatesAt line 99
  6. lemma OAI.NumericalDimensionOne.projective_generic_coordinate_ne_zero line 125
  7. lemma OAI.NumericalDimensionOne.projective_stalk_coordinates line 147
  8. lemma OAI.NumericalDimensionOne.finite_support_selection line 208
  9. def OAI.NumericalDimensionOne.selectedOrdDivisor line 213
  10. lemma OAI.NumericalDimensionOne.selectedOrdDivisor_apply line 218
  11. lemma OAI.NumericalDimensionOne.exists_cartierDivisor_of_local_orders line 224
  12. lemma OAI.NumericalDimensionOne.exists_projective_hyperplane_divisor line 253
  13. lemma OAI.NumericalDimensionOne.projective_stalk_coordinates_full line 300
  14. lemma OAI.NumericalDimensionOne.projective_homogeneous_stalk_value line 349
  15. lemma OAI.NumericalDimensionOne.projective_hyperplane_section line 390
  16. lemma OAI.NumericalDimensionOne.projective_homogeneous_basis line 450
  17. lemma OAI.NumericalDimensionOne.exists_ampleDivisor_of_projective line 505
  18. lemma OAI.NumericalDimensionOne.surface_fixed_square line 535