OAI/AlgebraicGeometry/NumericalDimension/RationalPullbacks.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Rational Pullbacks.

  1. lemma OAI.NumericalDimensionOne.order_div line 15
  2. lemma OAI.NumericalDimensionOne.affine_unit_of_zero_orders line 19
  3. lemma OAI.NumericalDimensionOne.local_equation_ratio_unit line 33
  4. lemma OAI.NumericalDimensionOne.order_stalk_unit line 55
  5. lemma OAI.NumericalDimensionOne.pulled_equation_order_eq line 61
  6. theorem OAI.NumericalDimensionOne.exists_cartierPullback line 82
  7. theorem OAI.NumericalDimensionOne.IsCartierPullback.isCartier line 125
  8. theorem OAI.NumericalDimensionOne.IsCartierPullback.unique line 136
  9. theorem OAI.NumericalDimensionOne.IsCartierPullback.add line 145
  10. theorem OAI.NumericalDimensionOne.IsCartierPullback.neg line 162
  11. theorem OAI.NumericalDimensionOne.isCartierPullback_zero line 174
  12. theorem OAI.NumericalDimensionOne.isCartierPullback_principal line 182
  13. def OAI.NumericalDimensionOne.IsPulledCartierRepresentative line 201
  14. lemma OAI.NumericalDimensionOne.image_generic_mem line 225
  15. lemma OAI.NumericalDimensionOne.algebraMap_stalkSpecializes line 230
  16. lemma OAI.NumericalDimensionOne.curve_equation_order_eq line 236
  17. theorem OAI.NumericalDimensionOne.exists_pulledCartierRepresentative line 271
  18. theorem OAI.NumericalDimensionOne.IsPulledCartierRepresentative.isCartier line 310
  19. def OAI.NumericalDimensionOne.complexProjectiveSpace line 330
  20. def OAI.NumericalDimensionOne.projectiveConstants line 333
  21. def OAI.NumericalDimensionOne.complexProjectiveSpaceMap line 341
  22. def OAI.NumericalDimensionOne.IsComplexProjective line 346
  23. structure OAI.NumericalDimensionOne.ComplexProjectiveVariety line 350
  24. def OAI.NumericalDimensionOne.IsSmoothNfold line 359
  25. theorem OAI.NumericalDimensionOne.projectiveConstants_bijective line 362
  26. theorem OAI.NumericalDimensionOne.complexProjectiveSpace_isProper line 372
  27. theorem OAI.NumericalDimensionOne.isProper_of_isComplexProjective line 392
  28. theorem OAI.NumericalDimensionOne.isIntegrallyClosed_of_etale_domain line 406
  29. theorem OAI.NumericalDimensionOne.isIntegrallyClosed_of_smooth_field_domain line 454
  30. theorem OAI.NumericalDimensionOne.integrallyClosed_stalk_of_smooth_field line 488
  31. def OAI.NumericalDimensionOne.alternatingRestrictScalars line 521
  32. def OAI.NumericalDimensionOne.topDifferentialMap line 528
  33. theorem OAI.NumericalDimensionOne.topDifferentialMap_ιMulti line 534
  34. def OAI.NumericalDimensionOne.schemeStalkScalar line 547
  35. def OAI.NumericalDimensionOne.schemeFieldScalar line 552
  36. def OAI.NumericalDimensionOne.schemeStalkAlgebra line 557
  37. def OAI.NumericalDimensionOne.schemeFieldAlgebra line 561
  38. theorem OAI.NumericalDimensionOne.stalk_field_scalar_tower line 564