OAI/AlgebraicGeometry/SurfaceCones/SpecCoordinates.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

Coordinate maps for checking the source-chart evaluation glue.

  1. def OAI.AlgebraicGeometry.Scheme.coordinateMap line 14
  2. lemma OAI.AlgebraicGeometry.Scheme.coordinateMap_injective line 17
  3. lemma OAI.AlgebraicGeometry.Scheme.coordinateMap_comp line 23
  4. lemma OAI.AlgebraicGeometry.Scheme.coordinateMap_precomp line 30
  5. lemma OAI.HomogeneousLocalization.awayMap_ratio_transition line 51
  6. lemma OAI.SectionCompletion.dehomogenize_homogeneous line 83
  7. lemma OAI.SectionCompletion.scheme_chart_transition line 91
  8. lemma OAI.SourcePullbackChart.blowupIota_blowdown line 133
  9. lemma OAI.SourcePullbackChart.coneEvaluation_homogeneous line 165
  10. lemma OAI.SourcePullbackChart.fiberParameter_relation line 179
  11. lemma OAI.SourcePullbackChart.pullbackIota_base line 189
  12. lemma OAI.SourcePullbackChart.surfaceMap_compatible line 195
  13. lemma OAI.SourcePullbackChart.baseMap_compatible line 209
  14. lemma OAI.SourcePullbackChart.fiberParameter_compatible line 223
  15. lemma OAI.SourcePullbackChart.homogeneous_evaluation_calculation line 240
  16. lemma OAI.SourcePullbackChart.map_mul_pow line 245
  17. lemma OAI.SourcePullbackChart.map_coneEvaluation_homogeneous line 249
  18. lemma OAI.SourcePullbackChart.evaluation_homogeneous_compatible line 258
  19. lemma OAI.SourcePullbackChart.evaluation_compatible line 280

    Source documentation

    Compatibility of the local evaluations under any two maps into source charts whose actual source maps agree. In particular this applies on overlaps.

    lemma evaluation_compatible {Z : Scheme} (i j : Fin 3)
    (α : Z ⟶ Spec (.of (pullbackChart i))) (β : Z ⟶ Spec (.of (pullbackChart j)))
    (hαβ : α ≫ pullbackIota i = β ≫ pullbackIota j) :
    α ≫ Spec.map (CommRingCat.ofHom (coneEvaluation i)) =
      β ≫ Spec.map (CommRingCat.ofHom (coneEvaluation j)) := by
…

    Mentions: OAI.SourcePullbackChart.pullbackChart, OAI.SourcePullbackChart.pullbackIota, OAI.SourcePullbackChart.coneEvaluation

  20. def OAI.SourcePullbackChart.coneMorphism line 299

    Source documentation

    The source's cone-evaluation morphism before completion, constructed by honest gluing on the literal W₀ = X ×[P²] V₀.

    def coneMorphism : KummerSourceModel.W₀ ⟶ Spec (.of sectionRing) :=
…

    Mentions: OAI.KummerSourceModel.W₀, OAI.SourcePullbackChart.sectionRing

  21. lemma OAI.SourcePullbackChart.pullbackIota_coneMorphism line 305
  22. lemma OAI.SourcePullbackChart.coneMorphism_parameters line 310

    Source documentation

    The glued evaluation is a morphism over the exact polynomial parameters.

    @[reassoc] lemma coneMorphism_parameters :
    coneMorphism ≫ Spec.map (CommRingCat.ofHom parameterMap.toRingHom) =
      KummerSourceModel.g₀ ≫ KummerSourceModel.blowdown := by
…

    Mentions: OAI.SourcePullbackChart.coneMorphism, OAI.KummerSourceModel.g₀, OAI.KummerSourceModel.blowdown

  23. lemma OAI.SourcePullbackChart.tensorChart_isPullback line 333
  24. lemma OAI.SourcePullbackChart.sourceChart_isPullback line 350
  25. lemma OAI.SourcePullbackChart.pullbackIota_opensRange line 358
  26. lemma OAI.SourcePullbackChart.blowdown_mem line 378
  27. lemma OAI.SourcePullbackChart.blowdown_preimage_le_chart line 384
  28. lemma OAI.SourcePullbackChart.coneMorphism_preimage_le_chart line 405
  29. lemma OAI.SourcePullbackChart.coneMorphism_restrict_isIso line 416

    Source documentation

    The full inverse image of a cone puncture, not just an auxiliary chart, is the same punctured affine scheme.

    lemma coneMorphism_restrict_isIso (i : Fin 3) :
    IsIso (coneMorphism ∣_ PrimeSpectrum.basicOpen (coneSection i)) := by
…

    Mentions: OAI.SourcePullbackChart.coneMorphism, OAI.SourcePullbackChart.coneSection

  30. def OAI.SourcePullbackChart.conePuncturedOpen line 424
  31. instance OAI.SourcePullbackChart.(instance at line 427) line 427
  32. instance OAI.SourcePullbackChart.surfaceChart_domain line 449
  33. instance OAI.SourcePullbackChart.pullbackChart_domain line 458
  34. instance OAI.SourcePullbackChart.uncompleted_reduced line 463
  35. instance OAI.SourcePullbackChart.uncompleted_noetherian line 470
  36. abbrev OAI.SourcePullbackChart.sourcePuncture line 474
  37. lemma OAI.SourcePullbackChart.chartPuncture_nonempty line 476
  38. lemma OAI.SourcePullbackChart.sourcePuncture_dense line 495
  39. instance OAI.SourcePullbackChart.sourcePuncture_dominant line 506
  40. instance OAI.SourcePullbackChart.sourcePuncture_schematicallyDominant line 510
  41. def OAI.SourcePullbackChart.zeroEvaluation line 533

    Source documentation

    Set the genuine fiber coordinate to zero.

    def zeroEvaluation (i : Fin 3) : chart i →+* planeChart i :=
…

    Mentions: OAI.SourcePullbackChart.chart, OAI.SourcePullbackChart.planeChart

  42. lemma OAI.SourcePullbackChart.zeroEvaluation_direction line 536
  43. lemma OAI.SourcePullbackChart.zeroEvaluation_fiber line 544
  44. lemma OAI.SourcePullbackChart.zeroEvaluation_base line 552
  45. lemma OAI.SourcePullbackChart.zeroEvaluation_surjective line 563
  46. lemma OAI.SourcePullbackChart.origin_image_principal line 566
  47. def OAI.SourcePullbackChart.pullbackBaseMap line 592
  48. def OAI.SourcePullbackChart.pullbackZeroEvaluation line 598
  49. lemma OAI.SourcePullbackChart.pullbackZeroEvaluation_surface line 601
  50. lemma OAI.SourcePullbackChart.pullbackZeroEvaluation_fiber line 606
  51. lemma OAI.SourcePullbackChart.pullbackZeroEvaluation_base line 611
  52. def OAI.SourcePullbackChart.pullbackZeroAlg line 630
  53. lemma OAI.SourcePullbackChart.pullbackZeroEvaluation_surjective line 634
  54. lemma OAI.SourcePullbackChart.pullbackZeroEvaluation_kernel line 638
  55. lemma OAI.SourcePullbackChart.fiberParameter_regular line 648
  56. def OAI.SourcePullbackChart.pullbackZeroQuotient line 656

    Source documentation

    The exact quotient at the zero section, with its S-algebra map.

    def pullbackZeroQuotient (i : Fin 3) :
    (pullbackChart i ⧸ RingHom.ker (pullbackZeroEvaluation i)) ≃ₐ[S] surfaceChart i :=
…

    Mentions: OAI.SourcePullbackChart.pullbackChart, OAI.SourcePullbackChart.pullbackZeroEvaluation, OAI.SourcePullbackChart.S, OAI.SourcePullbackChart.surfaceChart

  57. abbrev OAI.OriginScalarBaseChange.S line 672
  58. abbrev OAI.OriginScalarBaseChange.A line 673
  59. lemma OAI.OriginScalarBaseChange.constantCoeff_polynomial line 678
  60. def OAI.OriginScalarBaseChange.evaluation line 683
  61. abbrev OAI.OriginScalarBaseChange.tensor line 689
  62. def OAI.OriginScalarBaseChange.tensorEvaluation line 691
  63. lemma OAI.OriginScalarBaseChange.tensor_X_zero line 697
  64. lemma OAI.OriginScalarBaseChange.tensor_constant line 710
  65. lemma OAI.OriginScalarBaseChange.tensorEvaluation_tmul line 735
  66. def OAI.OriginScalarBaseChange.equiv line 742

    Source documentation

    Exact origin scalar base change, including its canonical maps.

    def equiv : tensor σ k D ≃+* D :=
…

    Mentions: OAI.OriginScalarBaseChange.tensor

  67. lemma OAI.OriginScalarBaseChange.equiv_tmul line 762
  68. instance OAI.MvPowerSeries.flat_polynomial line 778
  69. abbrev OAI.ScalarQuotientBaseChange.ideal line 793
  70. def OAI.ScalarQuotientBaseChange.equiv line 795
  71. lemma OAI.ScalarQuotientBaseChange.equiv_tmul line 800
  72. abbrev OAI.SourcePullbackChart.completedSourceChart line 834
  73. def OAI.SourcePullbackChart.completedFiberParameter line 842
  74. abbrev OAI.SourcePullbackChart.completedZeroIdeal line 844
  75. lemma OAI.SourcePullbackChart.completedZeroIdeal_eq line 850
  76. def OAI.SourcePullbackChart.completedZeroQuotient line 855

    Source documentation

    The zero-section quotient remains exactly D_i after completion.

    def completedZeroQuotient (i : Fin 3) :
    (completedSourceChart i ⧸ completedZeroIdeal i) ≃+* surfaceChart i :=
…

    Mentions: OAI.SourcePullbackChart.completedSourceChart, OAI.SourcePullbackChart.completedZeroIdeal, OAI.SourcePullbackChart.surfaceChart

  77. def OAI.SourcePullbackChart.completedZeroEvaluation line 861
  78. lemma OAI.SourcePullbackChart.completedZeroEvaluation_tmul line 864
  79. lemma OAI.SourcePullbackChart.completedZeroEvaluation_surjective line 873
  80. lemma OAI.SourcePullbackChart.completedZeroEvaluation_kernel line 876
  81. lemma OAI.SourcePullbackChart.completedFiberParameter_regular line 883
  82. instance OAI.SourcePullbackChart.completedZeroIdeal_prime line 887