OAI/AlgebraicGeometry/NumericalDimension/SmoothParameters.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Smooth Parameters.

  1. theorem OAI.NumericalDimensionOne.LocalSmoothFiber.formallySmooth line 22
  2. theorem OAI.NumericalDimensionOne.DVRParameter.etale_aeval line 46
  3. lemma OAI.NumericalDimensionOne.CurveEtaleChart.polynomial_dimension line 137
  4. theorem OAI.NumericalDimensionOne.CurveEtaleChart.exists_chart line 148
  5. theorem OAI.NumericalDimensionOne.smooth_dimension_one_of_dedekind line 208
  6. theorem OAI.NumericalDimensionOne.integrallyClosed_affine_of_stalks line 241
  7. theorem OAI.NumericalDimensionOne.dedekind_affine_of_stalks line 260
  8. theorem OAI.NumericalDimensionOne.affine_not_isField line 279
  9. theorem OAI.NumericalDimensionOne.smooth_dimension_one_of_normal_curve line 329
  10. theorem OAI.NumericalDimensionOne.coheight_le_one_of_bounded_embedding line 380
  11. theorem OAI.NumericalDimensionOne.strictMono_of_locallyQuasiFinite line 407
  12. theorem OAI.NumericalDimensionOne.coheight_le_of_locallyQuasiFinite line 420
  13. theorem OAI.NumericalDimensionOne.surjective_genericNormalization line 442
  14. theorem OAI.NumericalDimensionOne.smooth_genericNormalization line 457
  15. theorem OAI.NumericalDimensionOne.proper_genericNormalization line 472
  16. theorem OAI.NumericalDimensionOne.EtaleRegular.regular_local line 495
  17. theorem OAI.NumericalDimensionOne.EtaleRegular.regular_ring line 529
  18. theorem OAI.NumericalDimensionOne.regular_stalk_of_smooth_dimension line 559
  19. theorem OAI.NumericalDimensionOne.polynomial_maximal_height line 586