OAI/AlgebraicGeometry/NumericalDimension/NormalizationRings.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Normalization Rings.

  1. theorem OAI.NumericalDimensionOne.IsPulledCartierRepresentative.exists_effective_local_orders line 20
  2. theorem OAI.NumericalDimensionOne.properCurveDegree_eq_local_orders line 88
  3. theorem OAI.NumericalDimensionOne.fractionField_finite_of_finite line 126
  4. theorem OAI.NumericalDimensionOne.finite_integralClosure_of_finiteType line 153
  5. lemma OAI.NumericalDimensionOne.genericStalk_preimage_eq_top line 193
  6. def OAI.NumericalDimensionOne.genericSectionsIso line 204
  7. lemma OAI.NumericalDimensionOne.genericSectionsIso_app line 209
  8. lemma OAI.NumericalDimensionOne.genericSections_isFractionRing line 234
  9. theorem OAI.NumericalDimensionOne.finite_genericNormalization line 247
  10. theorem OAI.NumericalDimensionOne.genericNormalization_stalk line 300
  11. theorem OAI.NumericalDimensionOne.integral_genericNormalization line 333
  12. theorem OAI.NumericalDimensionOne.dominantFunctionFieldMap_bijective_of_preimmersion line 359
  13. instance OAI.NumericalDimensionOne.dominant_genericPointMap line 367
  14. instance OAI.NumericalDimensionOne.genericNormalization_isIntegral line 376
  15. instance OAI.NumericalDimensionOne.dominant_fromGenericNormalization line 378
  16. theorem OAI.NumericalDimensionOne.genericNormalization_bijective_functionField line 385
  17. def OAI.NumericalDimensionOne.genericNormalizationSectionsEquiv line 411
  18. def OAI.NumericalDimensionOne.affineFiberEquiv line 450
  19. def OAI.NumericalDimensionOne.primesOverAlgEquiv line 505
  20. lemma OAI.NumericalDimensionOne.primesOverAlgEquiv_asIdeal line 537
  21. def OAI.NumericalDimensionOne.integralClosureBaseMap line 554
  22. lemma OAI.NumericalDimensionOne.integralClosureBaseMap_tower line 560
  23. lemma OAI.NumericalDimensionOne.integralClosureBaseMap_isLocalization line 566