OAI/AlgebraicGeometry/SurfaceCones/OriginTensor.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

Coordinate ring of the actual closed fiber of V₀: its literal tensor product with C over S is the plane chart, via evaluation of the fiber coordinate at zero. No blowup/line-bundle isomorphism is assumed globally.

  1. def OAI.SourcePullbackChart.originScalarHom line 24
  2. abbrev OAI.SourcePullbackChart.originTensor line 27
  3. def OAI.SourcePullbackChart.zeroEvaluationAlg line 32
  4. def OAI.SourcePullbackChart.originTensorMap line 36
  5. def OAI.SourcePullbackChart.originTensorInverse line 40
  6. lemma OAI.SourcePullbackChart.originTensor_base line 43
  7. lemma OAI.SourcePullbackChart.originTensor_fiber line 47
  8. lemma OAI.SourcePullbackChart.originTensorInverse_scalar line 51
  9. lemma OAI.SourcePullbackChart.originTensorInverse_zeroEvaluation line 56
  10. lemma OAI.SourcePullbackChart.originTensorMap_tmul line 77
  11. lemma OAI.SourcePullbackChart.originTensor_left_inverse line 82
  12. lemma OAI.SourcePullbackChart.originTensor_right_inverse line 91
  13. def OAI.SourcePullbackChart.originTensorEquiv line 98

    Source documentation

    Closed fiber chart with its actual structural maps, not just an existential abstract isomorphism of rings.

    def originTensorEquiv (i : Fin 3) : originTensor i ≃+* planeChart i :=
…

    Mentions: OAI.SourcePullbackChart.originTensor, OAI.SourcePullbackChart.planeChart

  14. lemma OAI.SourcePullbackChart.originTensorEquiv_direction line 104
  15. abbrev OAI.SourcePullbackChart.originPoint line 124
  16. abbrev OAI.SourcePullbackChart.originFiber line 126
  17. def OAI.SourcePullbackChart.fiberDirection line 128
  18. def OAI.SourcePullbackChart.originFiberIota line 130
  19. instance OAI.SourcePullbackChart.(instance at line 135) line 135
  20. lemma OAI.SourcePullbackChart.originFiberIota_fst line 139
  21. lemma OAI.SourcePullbackChart.originFiberIota_snd line 146
  22. lemma OAI.SourcePullbackChart.originFiberIota_direction line 154
  23. lemma OAI.SourcePullbackChart.originFiberIota_isPullback line 161
  24. lemma OAI.SourcePullbackChart.originFiberIota_opensRange line 185
  25. lemma OAI.SourcePullbackChart.fiberDirection_restrict_isIso line 194
  26. instance OAI.SourcePullbackChart.fiberDirection_isIso line 211
  27. def OAI.SourcePullbackChart.originFiberIso line 216
  28. def OAI.ExplicitCone.projectiveCompletedParameterHom line 224
  29. lemma OAI.ConeCompletion.pow_smul_eq_restrict line 236
  30. def OAI.ConeCompletion.quotientScalarEquiv line 241
  31. lemma OAI.ConeCompletion.quotientScalarEquiv_mk line 247
  32. lemma OAI.ConeCompletion.quotientScalarEquiv_symm_mk line 252
  33. lemma OAI.ConeCompletion.quotientScalarEquiv_transition line 258
  34. lemma OAI.ConeCompletion.quotientScalarEquiv_symm_transition line 268
  35. def OAI.ConeCompletion.scalarEquiv line 277
  36. lemma OAI.ConeCompletion.scalarEquiv_of line 300
  37. lemma OAI.ConeCompletion.scalarEquiv_symm_of line 307
  38. lemma OAI.ConeCompletion.linearMap_ext_on_base line 323
  39. lemma OAI.ConeCompletion.eval_compatible line 351
  40. lemma OAI.ConeCompletion.pow_le_comap line 365
  41. def OAI.ConeCompletion.algebraLevelMap line 369
  42. lemma OAI.ConeCompletion.algebraLevelMap_of line 373
  43. lemma OAI.ConeCompletion.algebraLevelMap_compatible line 379
  44. def OAI.ConeCompletion.completionMap line 390
  45. lemma OAI.ConeCompletion.eval_completionMap line 394
  46. lemma OAI.ConeCompletion.completionMap_of line 399
  47. abbrev OAI.ConeCompletion.J line 414
  48. def OAI.ConeCompletion.tensorMap line 416
  49. lemma OAI.ConeCompletion.tensorMap_tmul line 420
  50. lemma OAI.ConeCompletion.tensorMap_linear_eq line 425
  51. lemma OAI.ConeCompletion.tensorMap_bijective line 454
  52. def OAI.ConeCompletion.tensorEquiv line 462
  53. lemma OAI.ConeCompletion.pow_mul_le line 475
  54. def OAI.ConeCompletion.powerLevelMap line 479
  55. lemma OAI.ConeCompletion.powerLevelMap_compatible line 482
  56. def OAI.ConeCompletion.powerMap line 493
  57. lemma OAI.ConeCompletion.powerMap_of line 497
  58. lemma OAI.ConeCompletion.algHom_ext_on_base line 502
  59. def OAI.ConeCompletion.cofinalEquiv line 511
  60. lemma OAI.ConeCompletion.cofinalEquiv_of line 522
  61. lemma OAI.SectionCompletion.scale_mem line 537
  62. def OAI.SectionCompletion.scaleHom line 545
  63. lemma OAI.SectionCompletion.scaleHom_monomial line 549
  64. lemma OAI.SectionCompletion.monomial_mem_of_scale_stable line 555
  65. lemma OAI.SectionCompletion.scaleHom_parameter line 569
  66. lemma OAI.SectionCompletion.scale_stable_linearIdeal line 576
  67. def OAI.SectionCompletion.cofinalHomogeneousPart line 590
  68. lemma OAI.SectionCompletion.cofinalHomogeneousPart_sum line 600
  69. lemma OAI.SectionCompletion.cofinalHomogeneousPart_eq_zero_of_degree_lt line 608
  70. lemma OAI.SectionCompletion.finite_quotient_degreeIdeal_le line 614
  71. lemma OAI.SectionCompletion.linear_parameter_cofinal line 661
  72. lemma OAI.SectionCompletion.exists_augmentationCompletionEquiv line 681
  73. lemma OAI.SectionCompletion.polynomial_subst_square line 696
  74. lemma OAI.SectionCompletion.map_vars_eq_linearIdeal line 706
  75. lemma OAI.SectionCompletion.map_vars_le_degreeIdeal line 713
  76. lemma OAI.SectionCompletion.polynomial_algebraMap_eq_aeval line 723
  77. theorem OAI.SectionCompletion.exists_canonicalTensorEquiv line 734

    Source documentation

    Canonical base change at the very same degree-one sections.

    theorem exists_canonicalTensorEquiv [CharZero k] [IsAlgClosed k]
    [Algebra.FiniteType k (polynomials T)]
    (hzero : T 0 = LinearMap.range (Algebra.linearMap k K))
    (w : σ → K) (hw : ∀ i, w i ∈ T 1)
    (hfin : (linearPolynomialMap T w hw).Finite) :
    letI : Algebra (MvPolynomial σ k) (polynomials T) :=
…

    Mentions: OAI.SectionCompletion.polynomials, OAI.SectionCompletion.linearPolynomialMap

  78. theorem OAI.ExplicitCone.exists_projectiveTensorEquiv line 819

    Source documentation

    the manuscript, lines 221–239, on the exact normalized Kummer cone and the exact projective Noether-normalization parameters, not an unrelated chosen map.

    theorem exists_projectiveTensorEquiv :
    letI : Algebra (MvPolynomial (Fin 3) ℂ) (SectionCompletion.polynomials pieces) :=
…

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

  79. def OAI.ExplicitCone.projectiveTensorEquiv line 851

    Source documentation

    Canonical algebra equivalence used to interpret the paper's tensor-product cone as the already formalized degreewise completed ring.

    def projectiveTensorEquiv :
    letI : Algebra (MvPolynomial (Fin 3) ℂ) (SectionCompletion.polynomials pieces) :=
…

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

  80. theorem OAI.ExplicitCone.projectiveTensorEquiv_tmul line 861