OAI/AlgebraicGeometry/NumericalDimension/NormalizationStalks.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Normalization Stalks.

  1. def OAI.NumericalDimensionOne.localizedPrimesOverEquiv line 22
  2. def OAI.NumericalDimensionOne.genericNormalizationFiberEquiv line 67
  3. lemma OAI.NumericalDimensionOne.genericNormalizationFiberEquiv_symm_asIdeal line 115
  4. def OAI.NumericalDimensionOne.integralClosureToNormal line 148
  5. lemma OAI.NumericalDimensionOne.integralClosureToNormal_map line 159
  6. lemma OAI.NumericalDimensionOne.integralClosureToNormal_injective line 163
  7. theorem OAI.NumericalDimensionOne.LocalizationTower.atPrime_of_localized_base line 183
  8. theorem OAI.NumericalDimensionOne.normal_overring_isLocalization_integralClosure line 214
  9. def OAI.NumericalDimensionOne.birationalStalkToField line 259
  10. theorem OAI.NumericalDimensionOne.birationalStalk_isFractionRing line 264
  11. theorem OAI.NumericalDimensionOne.birationalStalk_tower line 274
  12. theorem OAI.NumericalDimensionOne.finite_birational_stalk_normalization line 292
  13. def OAI.NumericalDimensionOne.fiberStalkMap line 344
  14. lemma OAI.NumericalDimensionOne.fiberStalkMap_self line 348
  15. lemma OAI.NumericalDimensionOne.fiberStalkMap_germ line 352
  16. lemma OAI.NumericalDimensionOne.fiberStalkMap_isLocalHom line 363
  17. lemma OAI.NumericalDimensionOne.birationalFiberStalk_tower line 373
  18. lemma OAI.NumericalDimensionOne.finite_birational_fiberStalk_normalization line 383
  19. lemma OAI.NumericalDimensionOne.subalgebraFractionMap_eq line 412
  20. lemma OAI.NumericalDimensionOne.integralClosureToNormal_comp_base line 439
  21. theorem OAI.NumericalDimensionOne.genericNormalization_stalk_atPrime line 467
  22. theorem OAI.NumericalDimensionOne.finite_integralClosure_localization line 561
  23. theorem OAI.NumericalDimensionOne.finite_integralClosure_stalk line 599