OAI/AlgebraicGeometry/NumericalDimension/HyperplaneDimension.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Hyperplane Dimension.

  1. theorem OAI.NumericalDimensionOne.exists_smooth_member_strict_specialization line 24
  2. lemma OAI.NumericalDimensionOne.universalLinearSection_map line 74
  3. theorem OAI.NumericalDimensionOne.normalized_incidence_baseChange line 86
  4. theorem OAI.NumericalDimensionOne.smooth_preimage_open_of_comap line 128
  5. inductive OAI.NumericalDimensionOne.IncidenceCutChain line 164
  6. lemma OAI.NumericalDimensionOne.IncidenceCutChain.isClosedImmersion line 179
  7. theorem OAI.NumericalDimensionOne.exists_smooth_complete_intersection_avoiding line 206
  8. theorem OAI.NumericalDimensionOne.height_le_closed_topologicalKrullDim line 321
  9. lemma OAI.NumericalDimensionOne.height_lt_of_closed_dim_lt line 341
  10. theorem OAI.NumericalDimensionOne.exists_generated_complete_intersection_avoiding line 366
  11. theorem OAI.NumericalDimensionOne.ideal_map_comap_closedImmersion line 429
  12. def OAI.NumericalDimensionOne.incidenceIntersectionIdeal line 467
  13. lemma OAI.NumericalDimensionOne.incidenceIntersectionIdeal_comap line 472
  14. theorem OAI.NumericalDimensionOne.IncidenceCutChain.exists_parameters line 485
  15. theorem OAI.NumericalDimensionOne.isIso_pullback_snd_of_range_subset_isoLocus line 524
  16. theorem OAI.NumericalDimensionOne.finiteType_maximal_height line 551
  17. theorem OAI.NumericalDimensionOne.affine_dimension_of_functionField line 595
  18. theorem OAI.NumericalDimensionOne.affine_prime_coheight line 611
  19. theorem OAI.NumericalDimensionOne.affine_closed_point_height line 621
  20. theorem OAI.NumericalDimensionOne.scheme_dimension_of_functionField line 634
  21. def OAI.NumericalDimensionOne.projectiveLinearPolynomial line 682
  22. lemma OAI.NumericalDimensionOne.projectiveLinearPolynomial_homogeneous line 684