OAI/AlgebraicGeometry/StableCoordinate/LaurentPresentation.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

The localized graded presentation

This file constructs the actual algebra equivalence G[p⁻¹] ≃ₐ[k] (B k)[T;T⁻¹] from Section 3. No domain hypothesis is needed for this explicit coordinate calculation.

  1. def OAI.StableCoordinate.LaurentPresentation.xG line 22
  2. def OAI.StableCoordinate.LaurentPresentation.yG line 23
  3. def OAI.StableCoordinate.LaurentPresentation.zG line 24
  4. theorem OAI.StableCoordinate.LaurentPresentation.quadric_identity line 26
  5. theorem OAI.StableCoordinate.LaurentPresentation.quadricG line 35
  6. def OAI.StableCoordinate.LaurentPresentation.baseMap line 49

    Source documentation

    The source's degree-zero quadric algebra maps into its graded presentation.

    noncomputable def baseMap : B k →ₐ[k] G k :=
…
  7. theorem OAI.StableCoordinate.LaurentPresentation.baseMap_bX line 58
  8. theorem OAI.StableCoordinate.LaurentPresentation.baseMap_sB line 63
  9. theorem OAI.StableCoordinate.LaurentPresentation.baseMap_f0 line 66
  10. theorem OAI.StableCoordinate.LaurentPresentation.baseMap_g0 line 70
  11. abbrev OAI.StableCoordinate.LaurentPresentation.Laurent line 73
  12. abbrev OAI.StableCoordinate.LaurentPresentation.Localized line 74
  13. def OAI.StableCoordinate.LaurentPresentation.localMap line 76
  14. def OAI.StableCoordinate.LaurentPresentation.localParameter line 79
  15. def OAI.StableCoordinate.LaurentPresentation.fromLaurent line 85
  16. theorem OAI.StableCoordinate.LaurentPresentation.fromLaurent_C line 93
  17. theorem OAI.StableCoordinate.LaurentPresentation.fromLaurent_T line 97
  18. theorem OAI.StableCoordinate.LaurentPresentation.fromLaurent_T_one line 101
  19. theorem OAI.StableCoordinate.LaurentPresentation.fromLaurent_T_neg_one line 105
  20. def OAI.StableCoordinate.LaurentPresentation.laurentValues line 110
  21. theorem OAI.StableCoordinate.LaurentPresentation.cancel_T line 115
  22. theorem OAI.StableCoordinate.LaurentPresentation.value_x line 123
  23. theorem OAI.StableCoordinate.LaurentPresentation.value_y line 132
  24. theorem OAI.StableCoordinate.LaurentPresentation.value_z line 142
  25. theorem OAI.StableCoordinate.LaurentPresentation.laurentValues_relation line 151
  26. def OAI.StableCoordinate.LaurentPresentation.toLaurentBase line 175
  27. theorem OAI.StableCoordinate.LaurentPresentation.toLaurentBase_gX line 184
  28. theorem OAI.StableCoordinate.LaurentPresentation.toLaurentBase_parameter_isUnit line 189
  29. def OAI.StableCoordinate.LaurentPresentation.toLaurent line 193
  30. theorem OAI.StableCoordinate.LaurentPresentation.toLaurent_localMap line 197
  31. theorem OAI.StableCoordinate.LaurentPresentation.toLaurentBase_xG line 202
  32. theorem OAI.StableCoordinate.LaurentPresentation.toLaurentBase_yG line 206
  33. theorem OAI.StableCoordinate.LaurentPresentation.toLaurentBase_zG line 211
  34. theorem OAI.StableCoordinate.LaurentPresentation.toLaurentBase_comp_baseMap line 215
  35. theorem OAI.StableCoordinate.LaurentPresentation.toLaurentBase_baseMap line 224
  36. theorem OAI.StableCoordinate.LaurentPresentation.parameter_cancel line 228
  37. theorem OAI.StableCoordinate.LaurentPresentation.fromLaurent_comp_toLaurentBase line 236
  38. theorem OAI.StableCoordinate.LaurentPresentation.fromLaurent_toLaurentBase line 255
  39. theorem OAI.StableCoordinate.LaurentPresentation.toLaurent_invSelf line 259
  40. theorem OAI.StableCoordinate.LaurentPresentation.laurent_hom_ext line 275
  41. theorem OAI.StableCoordinate.LaurentPresentation.toLaurent_comp_fromLaurent line 290
  42. theorem OAI.StableCoordinate.LaurentPresentation.fromLaurent_comp_toLaurent line 303
  43. def OAI.StableCoordinate.LaurentPresentation.equiv line 313

    Source documentation

    The exact Laurent presentation of the localized graded hypersurface.

    noncomputable def equiv : Localized k ≃ₐ[k] Laurent k :=
…

    Mentions: OAI.StableCoordinate.LaurentPresentation.Localized, OAI.StableCoordinate.LaurentPresentation.Laurent

  44. theorem OAI.StableCoordinate.LaurentPresentation.equiv_apply line 317
  45. theorem OAI.StableCoordinate.LaurentPresentation.equiv_symm_apply line 318
  46. theorem OAI.StableCoordinate.LaurentPresentation.equiv_localMap_gX line 321

    Source documentation

    Every source generator has the required explicit Laurent image.

    @[simp] theorem equiv_localMap_gX (i : Fin 5) :
    equiv k (localMap k (gX k i)) = laurentValues k i := by simp

    Mentions: OAI.StableCoordinate.LaurentPresentation.equiv, OAI.StableCoordinate.LaurentPresentation.localMap, OAI.StableCoordinate.LaurentPresentation.laurentValues

  47. theorem OAI.StableCoordinate.LaurentPresentation.equiv_localMap_baseMap line 325

    Source documentation

    The quadric subalgebra becomes precisely the constant Laurent polynomials.

    @[simp] theorem equiv_localMap_baseMap (r : B k) :
    equiv k (localMap k (baseMap k r)) = LaurentPolynomial.C r := by simp

    Mentions: OAI.StableCoordinate.LaurentPresentation.equiv, OAI.StableCoordinate.LaurentPresentation.localMap, OAI.StableCoordinate.LaurentPresentation.baseMap

  48. theorem OAI.StableCoordinate.LaurentPresentation.baseMap_injective line 329

    Source documentation

    Injectivity of the degree-zero quadric map follows from its constant Laurent image.

    theorem baseMap_injective : Function.Injective (baseMap k) := by
…

    Mentions: OAI.StableCoordinate.LaurentPresentation.baseMap