OAI/NumberTheory/PiExponent/Geometry/CurveNormalizationModel.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.CurveNormalizationModel.integralClosureTowerHom line 18
  2. theorem OAI.PiExponent.CurveNormalizationModel.integralClosureTower_isLocalizationAway line 28
  3. theorem OAI.PiExponent.CurveNormalizationModel.integralClosureTower_SpecMap_isOpenImmersion line 44
  4. def OAI.PiExponent.CurveNormalizationModel.parameterLaurentMap line 57
  5. abbrev OAI.PiExponent.CurveNormalizationModel.parameterLaurentAlgebra line 61
  6. theorem OAI.PiExponent.CurveNormalizationModel.parameterLaurentMap_T line 66
  7. theorem OAI.PiExponent.CurveNormalizationModel.parameterLaurentMap_T_inv line 72
  8. theorem OAI.PiExponent.CurveNormalizationModel.parameterLaurent_scalarTower line 77
  9. abbrev OAI.PiExponent.CurveNormalizationModel.parameterLaurentChart line 91
  10. def OAI.PiExponent.CurveNormalizationModel.parameterChartOverlapHom line 96
  11. theorem OAI.PiExponent.CurveNormalizationModel.parameterChartOverlap_isOpenImmersion line 104
  12. theorem OAI.PiExponent.CurveNormalizationModel.parameterLaurentMap_invert line 122
  13. theorem OAI.PiExponent.CurveNormalizationModel.isIntegralElem_comp_equiv line 134
  14. def OAI.PiExponent.CurveNormalizationModel.reciprocalLaurentChartEquiv line 145
  15. def OAI.PiExponent.CurveNormalizationModel.zeroOverlap line 168
  16. instance OAI.PiExponent.CurveNormalizationModel.zeroOverlap_isOpenImmersion line 171
  17. def OAI.PiExponent.CurveNormalizationModel.infinityOverlap line 174
  18. instance OAI.PiExponent.CurveNormalizationModel.infinityOverlap_isOpenImmersion line 179
  19. def OAI.PiExponent.CurveNormalizationModel.parameterCurve line 191
  20. def OAI.PiExponent.CurveNormalizationModel.zeroChartInclusion line 194
  21. def OAI.PiExponent.CurveNormalizationModel.infinityChartInclusion line 197
  22. instance OAI.PiExponent.CurveNormalizationModel.zeroChartInclusion_isOpenImmersion line 201
  23. instance OAI.PiExponent.CurveNormalizationModel.infinityChartInclusion_isOpenImmersion line 205
  24. theorem OAI.PiExponent.CurveNormalizationModel.parameterCurve_overlap_compatibility line 209
  25. theorem OAI.PiExponent.CurveNormalizationModel.parameterCurve_twoChartCover line 214
  26. def OAI.PiExponent.CurveNormalizationModel.zeroChartStalkIso line 232
  27. def OAI.PiExponent.CurveNormalizationModel.infinityChartStalkIso line 240
  28. instance OAI.PiExponent.CurveNormalizationModel.parameterCurve_compactSpace line 249
  29. theorem OAI.PiExponent.CurveNormalizationModel.parameterCurve_genericPoint line 260
  30. instance OAI.PiExponent.CurveNormalizationModel.parameterCurve_irreducibleSpace line 280
  31. instance OAI.PiExponent.CurveNormalizationModel.parameterCurve_isReduced line 283
  32. instance OAI.PiExponent.CurveNormalizationModel.parameterCurve_isIntegral line 292
  33. def OAI.PiExponent.CurveNormalizationModel.parameterCurveFunctionFieldIso line 295
  34. def OAI.PiExponent.CurveNormalizationModel.parameterCurveFunctionFieldEquiv line 305