OAI/AlgebraicGeometry/StableCoordinate/DeterminantCharts.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

Explicit affine charts for the determinant ring

These are the a- and d-localizations in Section 5, not the bundle charts in Section 4. The coefficient algebra has independent variables a,d,u.

  1. abbrev OAI.StableCoordinate.DeterminantRing.BaseAway line 21
  2. abbrev OAI.StableCoordinate.DeterminantRing.Chart line 22
  3. abbrev OAI.StableCoordinate.DeterminantRing.AwayA line 23
  4. abbrev OAI.StableCoordinate.DeterminantRing.AwayD line 24
  5. def OAI.StableCoordinate.DeterminantRing.chartVariable line 26
  6. def OAI.StableCoordinate.DeterminantRing.chartInverse line 28
  7. theorem OAI.StableCoordinate.DeterminantRing.chartVariable_mul_inverse line 31
  8. theorem OAI.StableCoordinate.DeterminantRing.chartVariable_isUnit line 35
  9. def OAI.StableCoordinate.DeterminantRing.chartMapA line 38
  10. theorem OAI.StableCoordinate.DeterminantRing.chartMapA_a line 48
  11. theorem OAI.StableCoordinate.DeterminantRing.chartMapA_d line 50
  12. theorem OAI.StableCoordinate.DeterminantRing.chartMapA_b line 52
  13. theorem OAI.StableCoordinate.DeterminantRing.chartMapA_c line 54
  14. theorem OAI.StableCoordinate.DeterminantRing.chartMapA_u line 57
  15. def OAI.StableCoordinate.DeterminantRing.toChartA line 60
  16. theorem OAI.StableCoordinate.DeterminantRing.toChartA_algebraMap line 64
  17. def OAI.StableCoordinate.DeterminantRing.baseToAwayA line 68
  18. theorem OAI.StableCoordinate.DeterminantRing.baseToAwayA_X0 line 71
  19. theorem OAI.StableCoordinate.DeterminantRing.baseToAwayA_X1 line 73
  20. theorem OAI.StableCoordinate.DeterminantRing.baseToAwayA_X2 line 75
  21. def OAI.StableCoordinate.DeterminantRing.coefficientFromChartA line 78
  22. theorem OAI.StableCoordinate.DeterminantRing.coefficientFromChartA_algebraMap line 84
  23. def OAI.StableCoordinate.DeterminantRing.fromChartA line 88
  24. theorem OAI.StableCoordinate.DeterminantRing.fromChartA_X line 91
  25. theorem OAI.StableCoordinate.DeterminantRing.fromChartA_C line 93
  26. theorem OAI.StableCoordinate.DeterminantRing.fromChartA_variable line 95
  27. theorem OAI.StableCoordinate.DeterminantRing.map_invSelf_eq line 99
  28. theorem OAI.StableCoordinate.DeterminantRing.fromChartA_inverse line 106
  29. theorem OAI.StableCoordinate.DeterminantRing.toChartA_inverse line 114
  30. theorem OAI.StableCoordinate.DeterminantRing.localized_c line 120
  31. theorem OAI.StableCoordinate.DeterminantRing.fromChartA_comp_toChartA line 129
  32. theorem OAI.StableCoordinate.DeterminantRing.toChartA_comp_fromChartA line 134
  33. def OAI.StableCoordinate.DeterminantRing.chartEquivA line 144

    Source documentation

    The actual algebra equivalence C[a⁻¹] ≃ k[a,a⁻¹,d,u][b].

    noncomputable def chartEquivA : AwayA k ≃ₐ[k] Chart k 0 :=
…

    Mentions: OAI.StableCoordinate.DeterminantRing.AwayA, OAI.StableCoordinate.DeterminantRing.Chart

  34. def OAI.StableCoordinate.DeterminantRing.chartMapD line 148
  35. theorem OAI.StableCoordinate.DeterminantRing.chartMapD_a line 158
  36. theorem OAI.StableCoordinate.DeterminantRing.chartMapD_d line 160
  37. theorem OAI.StableCoordinate.DeterminantRing.chartMapD_b line 162
  38. theorem OAI.StableCoordinate.DeterminantRing.chartMapD_c line 165
  39. theorem OAI.StableCoordinate.DeterminantRing.chartMapD_u line 167
  40. def OAI.StableCoordinate.DeterminantRing.toChartD line 170
  41. theorem OAI.StableCoordinate.DeterminantRing.toChartD_algebraMap line 174
  42. def OAI.StableCoordinate.DeterminantRing.baseToAwayD line 178
  43. theorem OAI.StableCoordinate.DeterminantRing.baseToAwayD_X0 line 181
  44. theorem OAI.StableCoordinate.DeterminantRing.baseToAwayD_X1 line 183
  45. theorem OAI.StableCoordinate.DeterminantRing.baseToAwayD_X2 line 185
  46. def OAI.StableCoordinate.DeterminantRing.coefficientFromChartD line 188
  47. theorem OAI.StableCoordinate.DeterminantRing.coefficientFromChartD_algebraMap line 194
  48. def OAI.StableCoordinate.DeterminantRing.fromChartD line 198
  49. theorem OAI.StableCoordinate.DeterminantRing.fromChartD_X line 201
  50. theorem OAI.StableCoordinate.DeterminantRing.fromChartD_C line 203
  51. theorem OAI.StableCoordinate.DeterminantRing.fromChartD_variable line 205
  52. theorem OAI.StableCoordinate.DeterminantRing.fromChartD_inverse line 209
  53. theorem OAI.StableCoordinate.DeterminantRing.toChartD_inverse line 217
  54. theorem OAI.StableCoordinate.DeterminantRing.localized_b line 223
  55. theorem OAI.StableCoordinate.DeterminantRing.fromChartD_comp_toChartD line 232
  56. theorem OAI.StableCoordinate.DeterminantRing.toChartD_comp_fromChartD line 237
  57. def OAI.StableCoordinate.DeterminantRing.chartEquivD line 247

    Source documentation

    The actual algebra equivalence C[d⁻¹] ≃ k[a,d,d⁻¹,u][c].

    noncomputable def chartEquivD : AwayD k ≃ₐ[k] Chart k 1 :=
…

    Mentions: OAI.StableCoordinate.DeterminantRing.AwayD, OAI.StableCoordinate.DeterminantRing.Chart

  58. theorem OAI.StableCoordinate.DeterminantRing.chartMapA_comp_baseMap line 251
  59. theorem OAI.StableCoordinate.DeterminantRing.chartMapD_comp_baseMap line 259
  60. theorem OAI.StableCoordinate.DeterminantRing.chartMapA_baseMap line 267
  61. theorem OAI.StableCoordinate.DeterminantRing.chartMapD_baseMap line 271
  62. theorem OAI.StableCoordinate.DeterminantRing.baseMap_injective line 276

    Source documentation

    Algebraic independence of a,d,u in the determinant quotient.

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

    Mentions: OAI.StableCoordinate.DeterminantRing.baseMap

  63. def OAI.StableCoordinate.DeterminantRing.chartMapAOverBase line 285

    Source documentation

    Compatibility with the actual polynomial coefficient algebra.

    noncomputable def chartMapAOverBase : C k →ₐ[Base k] Chart k 0 where
…

    Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.DeterminantRing.Base, OAI.StableCoordinate.DeterminantRing.Chart

  64. def OAI.StableCoordinate.DeterminantRing.chartMapDOverBase line 290

    Source documentation

    Compatibility with the actual polynomial coefficient algebra.

    noncomputable def chartMapDOverBase : C k →ₐ[Base k] Chart k 1 where
…

    Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.DeterminantRing.Base, OAI.StableCoordinate.DeterminantRing.Chart

  65. instance OAI.StableCoordinate.DeterminantRing.coefficientAlgebraA line 294
  66. instance OAI.StableCoordinate.DeterminantRing.coefficientAlgebraD line 296
  67. instance OAI.StableCoordinate.DeterminantRing.coefficientScalarTowerA line 299
  68. instance OAI.StableCoordinate.DeterminantRing.coefficientScalarTowerD line 301
  69. instance OAI.StableCoordinate.DeterminantRing.baseCoefficientScalarTowerA line 304
  70. instance OAI.StableCoordinate.DeterminantRing.baseCoefficientScalarTowerD line 312
  71. def OAI.StableCoordinate.DeterminantRing.chartEquivAOverCoefficients line 321

    Source documentation

    The a-chart equivalence, over its full localized coefficient ring.

    noncomputable def chartEquivAOverCoefficients : AwayA k ≃ₐ[BaseAway k 0] Chart k 0 where
…

    Mentions: OAI.StableCoordinate.DeterminantRing.AwayA, OAI.StableCoordinate.DeterminantRing.BaseAway, OAI.StableCoordinate.DeterminantRing.Chart

  72. def OAI.StableCoordinate.DeterminantRing.chartEquivDOverCoefficients line 329

    Source documentation

    The d-chart equivalence, over its full localized coefficient ring.

    noncomputable def chartEquivDOverCoefficients : AwayD k ≃ₐ[BaseAway k 1] Chart k 1 where
…

    Mentions: OAI.StableCoordinate.DeterminantRing.AwayD, OAI.StableCoordinate.DeterminantRing.BaseAway, OAI.StableCoordinate.DeterminantRing.Chart

  73. theorem OAI.StableCoordinate.DeterminantRing.chartMapA_injective line 337

    Source documentation

    Chart injectivity follows from the domain property, not an assumed chart inclusion.

    theorem chartMapA_injective [IsDomain k] [IsDomain (C k)] :
    Function.Injective (chartMapA k) := by
…

    Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.DeterminantRing.chartMapA

  74. theorem OAI.StableCoordinate.DeterminantRing.chartMapD_injective line 351

    Source documentation

    Chart injectivity follows from the domain property, not an assumed chart inclusion.

    theorem chartMapD_injective [IsDomain k] [IsDomain (C k)] :
    Function.Injective (chartMapD k) := by
…

    Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.DeterminantRing.chartMapD