OAI/AlgebraicGeometry/SurfaceCones/HomogeneousEvaluation.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Homogeneous fractions and evaluation in a field.

  1. def OAI.HomogeneousEvaluation.evaluate line 12
  2. lemma OAI.HomogeneousEvaluation.evaluate_mk line 16
  3. lemma OAI.HomogeneousEvaluation.evaluate_awayMap line 23
  4. abbrev OAI.SourceSymmetry.projSection_degree line 41
  5. abbrev OAI.SourceSymmetry.projPairChart line 44
  6. lemma OAI.SourceSymmetry.projChartEquiv_localizationElem line 47
  7. def OAI.SourceSymmetry.projPairChartEquiv line 68

    Source documentation

    The homogeneous product chart is the common field-principal open.

    def projPairChartEquiv (s t : SectionIndex) (hs : Good s) :
    projPairChart s t ≃+* coefficientOverlap s t :=
…

    Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.Good, OAI.SourceSymmetry.projPairChart, OAI.SourceSymmetry.coefficientOverlap

  8. lemma OAI.SourceSymmetry.projPairChartEquiv_awayMap line 77
  9. abbrev OAI.SourceSymmetry.projEval line 85

    Source documentation

    The same evaluation at one used in constructing the section ring.

    abbrev projEval (f : SectionCompletion.polynomials pieces)
    (hf : SectionCompletion.evaluateOne pieces f ≠ 0) : Away grading f →+* L :=
…

    Mentions: OAI.SectionCompletion.polynomials, OAI.SectionCompletion.evaluateOne, OAI.SourceSymmetry.grading

  10. lemma OAI.SourceSymmetry.projEval_awayMap line 89
  11. lemma OAI.SourceSymmetry.projSection_eval_ne_zero line 98
  12. lemma OAI.SourceSymmetry.projEval_eq_chart line 102
  13. lemma OAI.SourceSymmetry.projPairEval_eq line 106
  14. lemma OAI.SourceSymmetry.projPairChartEquiv_awayMap_right line 125
  15. instance OAI.SourceSymmetry.pairChartEquiv_isIso line 148
  16. lemma OAI.SourceSymmetry.pairChart_left_square line 160
  17. lemma OAI.SourceSymmetry.pairChart_right_square line 170
  18. lemma OAI.AlgebraicGeometry.Proj.awayMap_awayι_fixed_degree line 192
  19. abbrev OAI.SourceSymmetry.projPairDegree line 206
  20. lemma OAI.SourceSymmetry.pair_left_away_spec line 209
  21. lemma OAI.SourceSymmetry.pair_right_away_spec line 215
  22. lemma OAI.AlgebraicGeometry.specChart_square line 230
  23. def OAI.AlgebraicGeometry.openIsoOfOpensRange line 237
  24. def OAI.SourceSymmetry.coefficientOverlapIota line 253

    Source documentation

    The common open inclusion into the projective surface.

    def coefficientOverlapIota (s t : SectionIndex) (hs : Good s) :
    Spec (CommRingCat.of (coefficientOverlap s t)) ⟶ projectiveSurface :=
…

    Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.Good, OAI.SourceSymmetry.coefficientOverlap

  25. lemma OAI.SourceSymmetry.coefficientIota_eq line 258
  26. instance OAI.SourceSymmetry.coefficientOverlapIota_open line 263
  27. lemma OAI.SourceSymmetry.coefficientOverlapIota_left line 276
  28. lemma OAI.SourceSymmetry.coefficientOverlapIota_right line 284
  29. lemma OAI.SourceSymmetry.coefficientOverlapIota_opensRange line 292
  30. def OAI.SourceSymmetry.coefficientOverlapIso line 299

    Source documentation

    The scheme overlap. This isomorphism is

    def coefficientOverlapIso (s t : SectionIndex) (hs : Good s) :
    Spec (CommRingCat.of (coefficientOverlap s t)) ≅
      (Proj.basicOpen grading (projSection s) ⊓ Proj.basicOpen grading (projSection t)).toScheme :=
…

    Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.Good, OAI.SourceSymmetry.coefficientOverlap, OAI.SourceSymmetry.grading, OAI.SourceSymmetry.projSection

  31. lemma OAI.ActualCotangent.openIso_hom line 317
  32. lemma OAI.ActualCotangent.homEquiv_id line 320
  33. lemma OAI.ActualCotangent.restrictDerivation_postcomp line 324
  34. lemma OAI.ActualCotangent.derivation_postcomp_comp line 333
  35. lemma OAI.ActualCotangent.restrict_homEquiv line 339
  36. lemma OAI.ActualCotangent.openIso_derivation line 350
  37. lemma OAI.ActualCotangent.affineIso_inv line 381
  38. lemma OAI.ActualCotangent.affineIso_inv_adjoint line 384
  39. lemma OAI.ActualCotangent.affineIso_inv_D line 392
  40. lemma OAI.ActualCotangent.openIso_D line 421
  41. lemma OAI.ActualCotangent.openIso_inv_D line 427
  42. lemma OAI.ActualCotangent.eqToIso_inv_D line 434
  43. lemma OAI.ActualSections.iso_trans_inv_apply line 451
  44. lemma OAI.ActualSections.affine_global_app line 463
  45. lemma OAI.ActualSections.tilde_unit_top line 465
  46. lemma OAI.ActualSections.iso_chain_inv_apply line 478
  47. lemma OAI.ActualSections.iso_inv_apply_congr line 486
  48. lemma OAI.ActualSections.affine_map_unit line 490
  49. lemma OAI.ActualCotangent.openAffineIso_eq line 510
  50. lemma OAI.ActualCotangent.affineIso_inv_D_section line 516
  51. def OAI.ActualSections.moduleApply line 535
  52. def OAI.ActualSections.isoInv line 536
  53. lemma OAI.ActualSections.isoInv_trans line 537
  54. lemma OAI.ActualSections.isoInv_chain line 539
  55. lemma OAI.ActualSections.isoInv_congr line 544
  56. lemma OAI.ActualSections.isoInv_val line 550
  57. lemma OAI.ActualCotangent.affineInv_eval_D line 565
  58. lemma OAI.ActualCotangent.eqToIso_eval_D line 569
  59. lemma OAI.ActualCotangent.openInv_eval_D line 574
  60. lemma OAI.ActualCotangent.openAffineIso_inv_D_wrapped line 592
  61. lemma OAI.ActualCotangent.openAffineIso_inv_D line 629
  62. def OAI.ActualExterior.wedgeSection line 651

    Source documentation

    The wedge of sections, followed by the sheafification map.

    def wedgeSection (M : X.Modules) (n : ℕ) (U : X.Opens) (z : Fin n → Γ(M,U)) :
    Γ((sheafFunctor X n).obj M,U) :=
…

    Mentions: OAI.ActualExterior.sheafFunctor

  63. lemma OAI.ActualExterior.wedgeSection_map line 656
  64. lemma OAI.ActualExterior.map_wedgeSection line 669
  65. lemma OAI.ActualExterior.reindexIso_mk line 699
  66. lemma OAI.ActualExterior.sheafify_map_unit line 706
  67. lemma OAI.ActualExterior.openSheafifyMap_unit line 716
  68. lemma OAI.ActualExterior.openIso_wedgeSection line 727
  69. lemma OAI.ActualSections.iso_inv_hom_apply line 772
  70. lemma OAI.ActualSections.iso_hom_inv_apply line 775