OAI/AlgebraicGeometry/RelativeTriviality/Charts.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CampanaPeternellSix.RelativeLineCharts.CoordinateRing line 15
  2. abbrev OAI.CampanaPeternellSix.RelativeLineCharts.grading line 16
  3. def OAI.CampanaPeternellSix.RelativeLineCharts.scheme line 21
  4. abbrev OAI.CampanaPeternellSix.RelativeLineCharts.x₀ line 23
  5. abbrev OAI.CampanaPeternellSix.RelativeLineCharts.x₁ line 24
  6. lemma OAI.CampanaPeternellSix.RelativeLineCharts.x₀_mem line 26
  7. lemma OAI.CampanaPeternellSix.RelativeLineCharts.x₁_mem line 27
  8. abbrev OAI.CampanaPeternellSix.RelativeLineCharts.ChartRing line 30
  9. abbrev OAI.CampanaPeternellSix.RelativeLineCharts.FullChartRing line 31
  10. def OAI.CampanaPeternellSix.RelativeLineCharts.constants line 33
  11. instance OAI.CampanaPeternellSix.RelativeLineCharts.chartAlgebra line 40
  12. def OAI.CampanaPeternellSix.RelativeLineCharts.coordinate line 44
  13. def OAI.CampanaPeternellSix.RelativeLineCharts.fromPoly line 48
  14. def OAI.CampanaPeternellSix.RelativeLineCharts.dehom line 50
  15. lemma OAI.CampanaPeternellSix.RelativeLineCharts.dehom_x₀ line 53
  16. lemma OAI.CampanaPeternellSix.RelativeLineCharts.dehom_x₁ line 54
  17. lemma OAI.CampanaPeternellSix.RelativeLineCharts.dehom_C line 55
  18. def OAI.CampanaPeternellSix.RelativeLineCharts.fullDehom line 58
  19. def OAI.CampanaPeternellSix.RelativeLineCharts.toPoly line 61
  20. lemma OAI.CampanaPeternellSix.RelativeLineCharts.toPoly_mk line 64
  21. lemma OAI.CampanaPeternellSix.RelativeLineCharts.toPoly_algebraMap line 71
  22. lemma OAI.CampanaPeternellSix.RelativeLineCharts.toPoly_coordinate line 77
  23. def OAI.CampanaPeternellSix.RelativeLineCharts.toPolyAlg line 80
  24. lemma OAI.CampanaPeternellSix.RelativeLineCharts.toPoly_fromPoly line 84
  25. lemma OAI.CampanaPeternellSix.RelativeLineCharts.zero_degree_constant line 90
  26. lemma OAI.CampanaPeternellSix.RelativeLineCharts.coordinate_power line 97
  27. lemma OAI.CampanaPeternellSix.RelativeLineCharts.variables_generate line 111
  28. def OAI.CampanaPeternellSix.RelativeLineCharts.polynomialRange line 123
  29. lemma OAI.CampanaPeternellSix.RelativeLineCharts.fromPoly_surjective line 129
  30. theorem OAI.CampanaPeternellSix.RelativeLineCharts.chart_polynomial_equiv line 147
  31. def OAI.CampanaPeternellSix.RelativeLineCharts.chartEquiv line 168
  32. lemma OAI.CampanaPeternellSix.RelativeLineCharts.chartEquiv_constant line 170
  33. lemma OAI.CampanaPeternellSix.RelativeLineCharts.chartEquiv_coordinate line 174
  34. lemma OAI.CampanaPeternellSix.RelativeLineCharts.chartEquiv_fromPoly line 177
  35. abbrev OAI.CampanaPeternellSix.RelativeLineCharts.RightChartRing line 185
  36. def OAI.CampanaPeternellSix.RelativeLineCharts.rightCoordinate line 187
  37. def OAI.CampanaPeternellSix.RelativeLineCharts.swapVariables line 190
  38. lemma OAI.CampanaPeternellSix.RelativeLineCharts.swapVariables_x₀ line 194
  39. lemma OAI.CampanaPeternellSix.RelativeLineCharts.swapVariables_x₁ line 196
  40. lemma OAI.CampanaPeternellSix.RelativeLineCharts.swapVariables_C line 198
  41. lemma OAI.CampanaPeternellSix.RelativeLineCharts.swapVariables_comp line 201
  42. def OAI.CampanaPeternellSix.RelativeLineCharts.leftToRight line 212
  43. def OAI.CampanaPeternellSix.RelativeLineCharts.rightToLeft line 218
  44. lemma OAI.CampanaPeternellSix.RelativeLineCharts.rightToLeft_leftToRight line 224
  45. lemma OAI.CampanaPeternellSix.RelativeLineCharts.leftToRight_rightToLeft line 229
  46. def OAI.CampanaPeternellSix.RelativeLineCharts.chartSwap line 234
  47. lemma OAI.CampanaPeternellSix.RelativeLineCharts.chartSwap_coordinate line 240
  48. lemma OAI.CampanaPeternellSix.RelativeLineCharts.chartSwap_constant line 244
  49. def OAI.CampanaPeternellSix.RelativeLineCharts.rightChartEquiv line 253
  50. lemma OAI.CampanaPeternellSix.RelativeLineCharts.rightChartEquiv_coordinate line 255
  51. def OAI.CampanaPeternellSix.RelativeLineCharts.leftOpen line 267
  52. def OAI.CampanaPeternellSix.RelativeLineCharts.rightOpen line 268
  53. abbrev OAI.CampanaPeternellSix.RelativeLineCharts.OverlapRing line 269
  54. def OAI.CampanaPeternellSix.RelativeLineCharts.leftRestrict line 271
  55. theorem OAI.CampanaPeternellSix.RelativeLineCharts.standard_cover line 275
  56. instance OAI.CampanaPeternellSix.RelativeLineCharts.overlapAlgebra line 287
  57. instance OAI.CampanaPeternellSix.RelativeLineCharts.overlapLocalization line 289
  58. def OAI.CampanaPeternellSix.RelativeLineCharts.overlapEquiv line 294
  59. lemma OAI.CampanaPeternellSix.RelativeLineCharts.overlapEquiv_restrict line 299
  60. theorem OAI.CampanaPeternellSix.RelativeLineCharts.overlap_laurent_equiv line 305
  61. def OAI.CampanaPeternellSix.RelativeLineCharts.rightRestrict line 310
  62. lemma OAI.CampanaPeternellSix.RelativeLineCharts.restrict_coordinates_inverse line 313
  63. lemma OAI.CampanaPeternellSix.RelativeLineCharts.overlapEquiv_rightCoordinate line 321
  64. lemma OAI.CampanaPeternellSix.RelativeLineCharts.restrict_constants line 333
  65. lemma OAI.CampanaPeternellSix.RelativeLineCharts.overlapEquiv_right_fromPoly line 344
  66. lemma OAI.CampanaPeternellSix.RelativeLineCharts.overlapEquiv_rightRestrict line 362
  67. theorem OAI.CampanaPeternellSix.RelativeLineCharts.right_chart_laurent_equiv line 372
  68. lemma OAI.CampanaPeternellSix.RelativeLineCharts.overlap_eq_basic line 377
  69. def OAI.CampanaPeternellSix.RelativeLineCharts.leftSectionsIso line 380
  70. def OAI.CampanaPeternellSix.RelativeLineCharts.rightSectionsIso line 382
  71. def OAI.CampanaPeternellSix.RelativeLineCharts.overlapSectionsIso line 384
  72. def OAI.CampanaPeternellSix.RelativeLineCharts.leftSectionEquiv line 389
  73. def OAI.CampanaPeternellSix.RelativeLineCharts.rightSectionEquiv line 391
  74. def OAI.CampanaPeternellSix.RelativeLineCharts.overlapSectionEquiv line 393
  75. lemma OAI.CampanaPeternellSix.RelativeLineCharts.leftSections_restrict line 396
  76. lemma OAI.CampanaPeternellSix.RelativeLineCharts.rightSections_restrict line 409
  77. theorem OAI.CampanaPeternellSix.RelativeLineCharts.standard_section_restrictions line 424