OAI/AlgebraicGeometry/NumericalDimension/IncidenceSmoothness.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Incidence Smoothness.

  1. structure OAI.NumericalDimensionOne.DivisorAffineAtlas line 21
  2. def OAI.NumericalDimensionOne.DivisorAffineAtlas.cover line 31
  3. instance OAI.NumericalDimensionOne.DivisorAffineAtlas.(instance at line 40) line 40
  4. instance OAI.NumericalDimensionOne.DivisorAffineAtlas.(instance at line 41) line 41
  5. def OAI.NumericalDimensionOne.DivisorAffineAtlas.coordinate line 42
  6. theorem OAI.NumericalDimensionOne.exists_divisorAffineAtlas line 46
  7. lemma OAI.NumericalDimensionOne.idealSheaf_comap_inf_open line 75
  8. lemma OAI.NumericalDimensionOne.idealSheaf_comap_ker_open line 81
  9. lemma OAI.NumericalDimensionOne.idealSheaf_comap_map_open line 88
  10. theorem OAI.NumericalDimensionOne.idealSheaf_open_baseChange line 97
  11. lemma OAI.NumericalDimensionOne.idealSheaf_comap_iInf_open line 112
  12. theorem OAI.NumericalDimensionOne.idealSheaf_finite_glue line 124
  13. lemma OAI.NumericalDimensionOne.idealSheaf_comap_ofIdealTop_open line 142
  14. theorem OAI.NumericalDimensionOne.idealSheaf_finite_openImmersion_glue line 160
  15. def OAI.NumericalDimensionOne.universalLinearSection line 193
  16. lemma OAI.NumericalDimensionOne.universalLinearSection_span_eq line 196
  17. theorem OAI.NumericalDimensionOne.universal_incidence_exists line 213
  18. def OAI.NumericalDimensionOne.eliminationPolynomial line 268
  19. lemma OAI.NumericalDimensionOne.optionEquivLeft_rename_some line 271
  20. def OAI.NumericalDimensionOne.eliminationAlgEquiv line 280
  21. theorem OAI.NumericalDimensionOne.affine_hyperplane_equation_smooth line 289
  22. def OAI.NumericalDimensionOne.universalLinearPolynomial line 298
  23. lemma OAI.NumericalDimensionOne.rename_universal_linear line 300
  24. def OAI.NumericalDimensionOne.universalLinearQuotientEquiv line 311
  25. theorem OAI.NumericalDimensionOne.universal_linear_equation_smooth line 324
  26. theorem OAI.NumericalDimensionOne.affine_subscheme_smooth_of_quotient line 348
  27. lemma OAI.NumericalDimensionOne.linear_equation_ringSmooth_under_equiv line 383
  28. lemma OAI.NumericalDimensionOne.affineSpace_global_coordinates line 402
  29. theorem OAI.NumericalDimensionOne.universal_incidence_chart_smooth line 436
  30. theorem OAI.NumericalDimensionOne.universal_incidence_smooth_over line 463
  31. theorem OAI.NumericalDimensionOne.formallySmooth_over_perfect_subfield line 508