OAI/AlgebraicGeometry/SurfaceCones/KummerProjChart.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExplicitCone.sectionCoefficient_mem_piece line 10
  2. abbrev OAI.ExplicitCone.projBaseSection line 21
  3. abbrev OAI.ExplicitCone.projBaseChart line 23
  4. def OAI.ExplicitCone.projBaseChartEquiv line 28

    Source documentation

    The actual degree-zero homogeneous localization in Proj of the WHOLE normalized cone, not a surrogate affine model, is the literal smooth H-chart.

    def projBaseChartEquiv : projBaseChart ≃ₐ[ℂ] sectionChart :=
…

    Mentions: OAI.ExplicitCone.projBaseChart, OAI.ExplicitCone.sectionChart

  5. theorem OAI.ExplicitCone.projBaseChart_regular line 33
  6. theorem OAI.ExplicitCone.projBaseChart_smooth line 37
  7. lemma OAI.ExplicitCone.functionField_trdeg line 41
  8. theorem OAI.ExplicitCone.sectionChart_dimension line 48
  9. theorem OAI.ExplicitCone.projBaseChart_dimension line 53
  10. def OAI.ExplicitCone.projBaseOpenIso line 59

    Source documentation

    A genuine scheme isomorphism from the distinguished basic open of the actual Proj of normalized coefficients to the explicit Kummer H-chart.

    def projBaseOpenIso :
    (Proj.basicOpen (SectionCompletion.homogeneous pieces) projBaseSection).toScheme ≅
      Spec (CommRingCat.of sectionChart) :=
…

    Mentions: OAI.SectionCompletion.homogeneous, OAI.ExplicitCone.pieces, OAI.ExplicitCone.projBaseSection, OAI.ExplicitCone.sectionChart

  11. lemma OAI.SmallCM.finite_normalization_in_field_of_finite_type line 72
  12. lemma OAI.GradedNormalization.finite_polynomial_normalization line 112
  13. lemma OAI.GradedNormalization.normal_polynomial_normalization line 123
  14. lemma OAI.GradedNormalization.monomial_algebra_scale line 138
  15. lemma OAI.GradedNormalization.positive_monomial_constantCoeff line 149
  16. lemma OAI.ExplicitCone.polynomialGenerator_eq_monomial line 168
  17. lemma OAI.ExplicitCone.polynomialAlgebra_scale line 172
  18. lemma OAI.ExplicitCone.polynomialAlgebra_constantCoeff line 180
  19. lemma OAI.GradedNormalization.polynomial_piece_eq line 193
  20. lemma OAI.GradedNormalization.polynomialPiece_finiteType line 204
  21. lemma OAI.GradedNormalization.polynomialPiece_normalIn line 214
  22. theorem OAI.proper_comp_iso line 224
  23. lemma OAI.ExplicitCone.zero_piece line 230
  24. instance OAI.ExplicitCone.completedRing_isLocalRing line 233
  25. instance OAI.ExplicitCone.normalizedPolynomialsFiniteType line 236
  26. abbrev OAI.ExplicitCone.projectiveSurface line 241

    Source documentation

    Actual proper Proj of the entire normalized coefficient algebra.

    abbrev projectiveSurface : Scheme := SectionCompletion.proj pieces

    Mentions: OAI.SectionCompletion.proj, OAI.ExplicitCone.pieces

  27. def OAI.ExplicitCone.degreeZeroEquiv line 243
  28. def OAI.ExplicitCone.degreeZeroSpecIso line 248
  29. def OAI.ExplicitCone.projectiveSurfaceToComplex line 253
  30. instance OAI.ExplicitCone.projectiveSurfaceProper line 256
  31. def OAI.SectionChartSeries.localSeries line 273
  32. lemma OAI.SectionChartSeries.map_localSeries line 276
  33. def OAI.SectionChartSeries.hom line 284
  34. lemma OAI.SectionChartSeries.hom_injective line 315
  35. lemma OAI.SectionChartSeries.coeff_hom line 322
  36. def OAI.SectionGenerated.genSeries line 334
  37. lemma OAI.SectionGenerated.hasSubst line 336
  38. lemma OAI.SectionGenerated.monomial_subst line 343
  39. lemma OAI.SectionGenerated.coeff_subst line 355
  40. lemma OAI.SectionGenerated.coeff_subst_fiber line 374
  41. lemma OAI.SectionGenerated.exists_subst_of_coeff_span line 383
  42. lemma OAI.SectionGenerated.subst_mem line 416
  43. def OAI.SectionGenerated.substHom line 434
  44. lemma OAI.SectionGenerated.substHom_surjective line 440
  45. lemma OAI.SectionGenerated.isNoetherianRing line 453
  46. lemma OAI.precomplete_of_surjective line 463
  47. lemma OAI.complete_local_of_surjective line 478
  48. lemma OAI.mvPowerSeries_constantCoeff_zero_mem_vars line 490
  49. lemma OAI.mvPowerSeries_vars_eq_maximal line 525
  50. lemma OAI.SectionGenerated.adicComplete line 549
  51. lemma OAI.HomogeneousGeneration.exists_positive_generators line 573
  52. def OAI.HomogeneousGeneration.spanPiece line 611

    Source documentation

    Multiplicative homogeneous monomials describing every degree-n coefficient.

    def spanPiece {σ : Type} (v : σ → L) (d : σ → ℕ) (n : ℕ) : Submodule k L :=
…
  53. lemma OAI.HomogeneousGeneration.monomial_prod line 615
  54. lemma OAI.HomogeneousGeneration.coeff_mem_span line 627
  55. lemma OAI.HomogeneousGeneration.piece_eq_span line 651
  56. lemma OAI.SectionCompletion.finite_positive_presentation line 684
  57. abbrev OAI.CompletedCartierChart.seriesMap line 723
  58. abbrev OAI.CompletedCartierChart.constants line 724
  59. def OAI.CompletedCartierChart.chart line 726
  60. def OAI.CompletedCartierChart.sourceHom line 729
  61. def OAI.CompletedCartierChart.constantHom line 733
  62. def OAI.CompletedCartierChart.evaluation line 737
  63. lemma OAI.CompletedCartierChart.evaluation_constant line 741
  64. lemma OAI.CompletedCartierChart.evaluation_surjective line 746
  65. lemma OAI.CompletedCartierChart.variable_mem line 749
  66. def OAI.CompletedCartierChart.parameter line 767
  67. lemma OAI.CompletedCartierChart.parameter_ne_zero line 770
  68. lemma OAI.CompletedCartierChart.evaluation_parameter line 776
  69. lemma OAI.CompletedCartierChart.span_parameter_le_ker line 781
  70. lemma OAI.CompletedCartierChart.source_generator line 787
  71. lemma OAI.CompletedCartierChart.source_generator_mem_span line 814
  72. lemma OAI.CompletedCartierChart.source_sub_constant_mem_span_of_generators line 824
  73. lemma OAI.CompletedCartierChart.source_sub_constant_mem_span line 854
  74. lemma OAI.CompletedCartierChart.generators_sup_top line 864
  75. lemma OAI.CompletedCartierChart.sub_constant_mem_span line 871
  76. lemma OAI.CompletedCartierChart.ker_evaluation line 892
  77. def OAI.CompletedCartierChart.exceptionalEquiv line 903
  78. lemma OAI.ExplicitCone.actualCompletion_noetherian line 915