OAI/AlgebraicGeometry/NumericalDimension/CompleteIntersections.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Complete Intersections.

  1. theorem OAI.NumericalDimensionOne.projective_hyperplane_local_equations line 25
  2. theorem OAI.NumericalDimensionOne.affine_section_dimension_lower line 93
  3. theorem OAI.NumericalDimensionOne.scheme_section_dimension_lower line 142
  4. theorem OAI.NumericalDimensionOne.projective_section_dimension_lower line 202
  5. theorem OAI.NumericalDimensionOne.height_eq_zero_of_proper_affine line 244
  6. theorem OAI.NumericalDimensionOne.projective_hypersurface_meets_positive_dimension line 254
  7. theorem OAI.NumericalDimensionOne.exists_functionField_dimension line 294
  8. theorem OAI.NumericalDimensionOne.projective_hyperplane_height_lower line 311
  9. theorem OAI.NumericalDimensionOne.projective_intersection_height_lower line 346
  10. theorem OAI.NumericalDimensionOne.projectiveAffineMap_preimage_linear line 389
  11. theorem OAI.NumericalDimensionOne.DivisorProjectiveChart.toMorphism_preimage_linear line 412
  12. theorem OAI.NumericalDimensionOne.IncidenceCutChain.height_le line 447
  13. theorem OAI.NumericalDimensionOne.DivisorAffineAtlas.incidence_member_support line 491
  14. lemma OAI.NumericalDimensionOne.incidenceIntersectionIdeal_mem_support line 545
  15. theorem OAI.NumericalDimensionOne.IncidenceCutChain.exists_height_ge_of_embedding line 562
  16. lemma OAI.NumericalDimensionOne.scheme_topologicalKrullDim_eq line 607
  17. lemma OAI.NumericalDimensionOne.genericPoint_height_eq_dimension line 610
  18. theorem OAI.NumericalDimensionOne.functionField_dimension_of_dimension line 633
  19. theorem OAI.NumericalDimensionOne.exists_closed_point_in_component_interior line 671