OAI/NumberTheory/SiegelZeros/Intersection/TorusProjectiveClosure.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.affineSpecFunctionFieldAlgebra line 39
  2. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.affineSpecFunctionField_isFractionRing line 43
  3. abbrev OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.NormalizationRing line 47
  4. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizationRing_integrallyClosed line 49
  5. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizationRing_fractionRing line 53
  6. abbrev OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.AffineNormalization line 57
  7. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.affineNormalization_integral line 59
  8. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.affineNormalizationMap line 61
  9. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.affineNormalizationMap_integral line 65
  10. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.affineNormalizationMap_universallyClosed line 69
  11. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.affineNormalization_stalk_integrallyClosed line 72
  12. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizationFunctionFieldEquiv line 84
  13. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizationFunctionFieldEquiv_algebraMap line 89
  14. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizationOriginalFunctionFieldEquiv line 96
  15. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.toImage_ker_eq_bot line 109
  16. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.image_integral line 117
  17. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.image_integral_instance line 127
  18. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.image_range_eq_closure line 129
  19. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.image_proper line 133
  20. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.imageFunctionFieldEquiv line 135
  21. abbrev OAI.SiegelZeros.W58.AmbientPolynomial line 147
  22. def OAI.SiegelZeros.W58.coordinateProduct line 149
  23. abbrev OAI.SiegelZeros.W58.TorusRing line 151
  24. def OAI.SiegelZeros.W58.coordinate line 153
  25. theorem OAI.SiegelZeros.W58.coordinate_isUnit line 156
  26. def OAI.SiegelZeros.W58.identityEvaluation line 161
  27. theorem OAI.SiegelZeros.W58.identityEvaluation_coordinate line 166
  28. theorem OAI.SiegelZeros.W58.identityEvaluation_polynomial line 170
  29. theorem OAI.SiegelZeros.W58.ambient_dimension line 177
  30. theorem OAI.SiegelZeros.W58.torus_dimension_le_four line 180
  31. abbrev OAI.SiegelZeros.W58.GenericLocalRing line 188
  32. abbrev OAI.SiegelZeros.W58.GenericCotangent line 190
  33. theorem OAI.SiegelZeros.W58.generic_local_dimension line 193
  34. theorem OAI.SiegelZeros.W58.generic_local_dimension_le_four line 197
  35. abbrev OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.TorusSubvarietyRing line 212
  36. abbrev OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.TorusSubvariety line 214
  37. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusSubvariety_integral line 216
  38. abbrev OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.NormalizedTorusSubvariety line 218
  39. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedTorusSubvariety_integral line 220
  40. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedTorusSubvariety_stalk_integrallyClosed line 223
  41. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusNormalizationFunctionFieldEquiv line 227
  42. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusCoordinateFunction line 231
  43. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusCoordinateFunction_ne_zero line 236
  44. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedTorusCoordinateFunction line 241
  45. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedTorusCoordinateFunction_identification line 245
  46. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.normalizedTorusCoordinateFunction_ne_zero line 250
  47. theorem OAI.SiegelZeros.W58.torus_formallySmooth line 262
  48. theorem OAI.SiegelZeros.W58.torus_essFiniteType line 265
  49. theorem OAI.SiegelZeros.W58.torus_noetherian line 268
  50. theorem OAI.SiegelZeros.W58.generic_local_formallySmooth line 271
  51. theorem OAI.SiegelZeros.W58.generic_local_essFiniteType line 275
  52. theorem OAI.SiegelZeros.W58.generic_local_noetherian line 279
  53. theorem OAI.SiegelZeros.W58.generic_cotangent_finite line 283
  54. theorem OAI.SiegelZeros.W58.generic_residue_formallySmooth line 288
  55. theorem OAI.SiegelZeros.W58.generic_regular_iff_cotangent_dimension line 305
  56. theorem OAI.SiegelZeros.W58.smooth_kaehler_localization_injective line 316
  57. abbrev OAI.SiegelZeros.W17.ProjectiveChart.ProjectivePolynomial line 331
  58. abbrev OAI.SiegelZeros.W17.ProjectiveChart.AffinePolynomial line 332
  59. abbrev OAI.SiegelZeros.W17.ProjectiveChart.grading line 333
  60. instance OAI.SiegelZeros.W17.ProjectiveChart.gradingGradedRing line 335
  61. abbrev OAI.SiegelZeros.W17.ProjectiveChart.ChartRing line 337
  62. abbrev OAI.SiegelZeros.W17.ProjectiveChart.FullLocalization line 338
  63. def OAI.SiegelZeros.W17.ProjectiveChart.degreeZeroConstants line 340
  64. theorem OAI.SiegelZeros.W17.ProjectiveChart.degreeZeroConstants_bijective line 347
  65. def OAI.SiegelZeros.W17.ProjectiveChart.degreeZeroEquiv line 357
  66. instance OAI.SiegelZeros.W17.ProjectiveChart.finiteType_over_degreeZero line 360
  67. def OAI.SiegelZeros.W17.ProjectiveChart.chartConstants line 366
  68. instance OAI.SiegelZeros.W17.ProjectiveChart.chartAlgebra line 370
  69. def OAI.SiegelZeros.W17.ProjectiveChart.polynomialDehom line 372
  70. theorem OAI.SiegelZeros.W17.ProjectiveChart.polynomialDehom_zeroCoordinate line 376
  71. theorem OAI.SiegelZeros.W17.ProjectiveChart.polynomialDehom_coordinate line 379
  72. theorem OAI.SiegelZeros.W17.ProjectiveChart.polynomialDehom_C line 384
  73. def OAI.SiegelZeros.W17.ProjectiveChart.localizationDehom line 388
  74. theorem OAI.SiegelZeros.W17.ProjectiveChart.localizationDehom_algebraMap line 391
  75. theorem OAI.SiegelZeros.W17.ProjectiveChart.localizationDehom_fraction line 395
  76. def OAI.SiegelZeros.W17.ProjectiveChart.chartDehomRingHom line 404
  77. theorem OAI.SiegelZeros.W17.ProjectiveChart.chartDehom_fraction line 407
  78. theorem OAI.SiegelZeros.W17.ProjectiveChart.chartDehom_constants line 414
  79. def OAI.SiegelZeros.W17.ProjectiveChart.chartDehom line 420
  80. def OAI.SiegelZeros.W17.ProjectiveChart.chartCoordinate line 424
  81. theorem OAI.SiegelZeros.W17.ProjectiveChart.chartDehom_coordinate line 429
  82. def OAI.SiegelZeros.W17.ProjectiveChart.chartPolynomialMap line 433
  83. theorem OAI.SiegelZeros.W17.ProjectiveChart.chartDehom_comp_chartPolynomialMap line 436
  84. theorem OAI.SiegelZeros.W17.ProjectiveChart.chartDehom_surjective line 441
  85. theorem OAI.SiegelZeros.W17.ProjectiveChart.polynomialDehom_eq_zero_of_homogeneous line 447
  86. theorem OAI.SiegelZeros.W17.ProjectiveChart.chartDehom_injective line 455
  87. def OAI.SiegelZeros.W17.ProjectiveChart.chartEquiv line 468
  88. theorem OAI.SiegelZeros.W17.ProjectiveChart.chartEquiv_coordinate line 471
  89. abbrev OAI.SiegelZeros.W17.ProjectiveChart.projectiveSpace line 476
  90. abbrev OAI.SiegelZeros.W17.ProjectiveChart.affineSpace line 477
  91. def OAI.SiegelZeros.W17.ProjectiveChart.affineChartIso line 479
  92. def OAI.SiegelZeros.W17.ProjectiveChart.affineChartEmbedding line 482
  93. instance OAI.SiegelZeros.W17.ProjectiveChart.affineChartEmbedding_isOpenImmersion line 486
  94. theorem OAI.SiegelZeros.W17.ProjectiveChart.affineChartEmbedding_opensRange line 490
  95. def OAI.SiegelZeros.W17.ProjectiveChart.projectiveToBase line 502
  96. instance OAI.SiegelZeros.W17.ProjectiveChart.projectiveToBase_isProper line 505
  97. theorem OAI.SiegelZeros.W17.ProjectiveChart.affineChartEmbedding_toBase line 512
  98. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.projectiveSpace_locallyNoetherian line 535
  99. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusAffineEmbedding line 538
  100. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusAffineEmbedding_open line 543
  101. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusSubvarietyEmbedding line 548
  102. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusSubvarietyEmbedding_immersion line 552
  103. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusSubvarietyEmbedding_quasiCompact line 558
  104. abbrev OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.TorusProjectiveClosure line 561
  105. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusProjectiveClosure_integral line 563
  106. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusProjectiveClosureToBase line 565
  107. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusProjectiveClosure_proper line 569
  108. instance OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusProjectiveClosure_locallyNoetherian line 572
  109. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusProjectiveClosure_range line 577
  110. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.torusProjectiveClosureFunctionFieldEquiv line 582