OAI/AlgebraicGeometry/NumericalDimension/PrimeSpecialization.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Prime Specialization.

  1. theorem OAI.NumericalDimensionOne.maximal_comap_of_finiteType line 18
  2. theorem OAI.NumericalDimensionOne.coheight_eq_of_smooth_closed line 36
  3. theorem OAI.NumericalDimensionOne.schemeTheoreticallyDominant_toImage line 80
  4. theorem OAI.NumericalDimensionOne.reduced_image line 90
  5. theorem OAI.NumericalDimensionOne.integral_image line 94
  6. def OAI.NumericalDimensionOne.pointClosure line 115
  7. def OAI.NumericalDimensionOne.pointClosureι line 116
  8. instance OAI.NumericalDimensionOne.pointClosure_integral line 119
  9. instance OAI.NumericalDimensionOne.pointClosure_closedImmersion line 122
  10. lemma OAI.NumericalDimensionOne.pointClosure_range line 125
  11. lemma OAI.NumericalDimensionOne.pointClosure_nontrivial line 130
  12. theorem OAI.NumericalDimensionOne.surface_pointClosure_nontrivial line 167
  13. theorem OAI.NumericalDimensionOne.surface_pointClosure_coheight line 177
  14. theorem OAI.NumericalDimensionOne.surface_prime_normalization_smooth line 188
  15. theorem OAI.NumericalDimensionOne.surface_prime_normalization_proper line 204
  16. lemma OAI.NumericalDimensionOne.isClosed_point_of_isClosed_image line 225
  17. theorem OAI.NumericalDimensionOne.localOrder_eq_normalizedSchemeOrders line 236
  18. theorem OAI.NumericalDimensionOne.finsum_fiberwise line 287
  19. abbrev OAI.NumericalDimensionOne.ClosedCurvePoint line 315
  20. lemma OAI.NumericalDimensionOne.curvePrime_isClosed line 318
  21. def OAI.NumericalDimensionOne.finiteCurvePrimeImage line 321
  22. def OAI.NumericalDimensionOne.finiteCurvePrimeFiberEquiv line 326
  23. def OAI.NumericalDimensionOne.stalkGenerizationAlgebra line 357
  24. lemma OAI.NumericalDimensionOne.open_stalk_generization_tower line 361
  25. lemma OAI.NumericalDimensionOne.functionField_stalkGenerization_tower line 390
  26. theorem OAI.NumericalDimensionOne.isLocalization_stalkGenerization line 405
  27. def OAI.NumericalDimensionOne.generizationPrime line 439
  28. instance OAI.NumericalDimensionOne.generizationPrime_isPrime line 444
  29. lemma OAI.NumericalDimensionOne.generizationPrime_height line 447
  30. lemma OAI.NumericalDimensionOne.generizationPrime_affine line 457
  31. lemma OAI.NumericalDimensionOne.generizationPrime_injective line 469
  32. theorem OAI.NumericalDimensionOne.FactorialUniformizers.order_generator line 491
  33. theorem OAI.NumericalDimensionOne.order_stalk_generator line 534