OAI/AlgebraicGeometry/SurfaceCones/CanonicalConormal.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Conormal ratios on homogeneous degree-one charts.

  1. lemma OAI.SourcePullbackChart.source_degreeOne_ratio line 42

    Source documentation

    Degree-one section ratios in the normalized section algebra.

    lemma source_degreeOne_ratio {g c : polynomials pieces}
    (hg : g ∈ homogeneous pieces 1) (hc : c ∈ homogeneous pieces 1)
    {M : (Proj (homogeneous pieces)).Modules}
    (s t : SheafOfModules.unit (Proj (homogeneous pieces)).ringCatSheaf ⟶ M)
    (u : Fin 3 → (SheafOfModules.unit (Proj (homogeneous pieces)).ringCatSheaf ⟶ M))
    (hs : ∀ i, (restrictUnitIso (Proj.awayι (homogeneous pieces)
          (linearSection pieces (projectiveParameter i) (projectiveParameter_mem i))
          (linearSection_homogeneous pieces (projectiveParameter i) (projectiveParameter_mem i))
          (by decide : 0 < 1))).inv ≫
        (restrictFunctor (Proj.awayι (homogeneous pieces)
          (linearSection pieces (projectiveParameter i) (projectiveParameter_mem i))
          (linearSection_homogeneous pieces (projectiveParameter i) (projectiveParameter_mem i))
…
  2. lemma OAI.SourcePullbackChart.degreeOneCoefficient_fraction line 114
  3. lemma OAI.SourcePullbackChart.degreeOneConormalFraction_ratio line 121
  4. lemma OAI.SourcePullbackChart.degreeOne_projective_ratio_template line 133
  5. lemma OAI.SourcePullbackChart.degreeOneConormal_projective_ratio line 163
  6. lemma OAI.ActualSections.restrict_isIso_comp line 186
  7. abbrev OAI.SourceSymmetry.originalConormal line 195
  8. def OAI.SourceSymmetry.conormalSection line 198
  9. def OAI.SourceSymmetry.conormalChartSection line 202
  10. lemma OAI.SourceSymmetry.conormalChartSection_isIso line 208
  11. lemma OAI.SourceSymmetry.projChartEquiv_degreeOneFraction line 221
  12. lemma OAI.SourceSymmetry.conormalChartSection_ratio line 227
  13. def OAI.ActualLineFrames.globalFrame line 262
  14. lemma OAI.ActualLineFrames.globalFrame_restrict line 265
  15. lemma OAI.ActualLineFrames.restricted_globalFrame line 274
  16. lemma OAI.ActualLineFrames.globalFrame_isIso line 281
  17. lemma OAI.ActualLineFrames.globalFrame_ratio line 289
  18. def OAI.ActualLineFrames.globalOpenUnitIso line 321
  19. lemma OAI.ActualLineFrames.globalOpenUnitIso_frame line 327
  20. lemma OAI.ActualLineFrames.globalFrame_ratio_restrict line 335
  21. def OAI.SourceSymmetry.conormalOpenUnitIso line 356
  22. lemma OAI.SourceSymmetry.conormalOpenUnitIso_frame line 364
  23. lemma OAI.SourceSymmetry.conormalFrame_ratio line 372
  24. def OAI.SourceSymmetry.conormalOverlapRatio line 381

    Source documentation

    The linear transition, in the common-open ring.

    def conormalOverlapRatio (s t : SectionIndex) : coefficientOverlap s t :=
…

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

  25. lemma OAI.SourceSymmetry.canonicalOverlapRatio_is_power line 384
  26. lemma OAI.SourceSymmetry.intrinsic_conormal_transition line 388
  27. def OAI.ActualSheafTensor.tensorPower line 416
  28. def OAI.ActualSheafTensor.powerSection line 420
  29. lemma OAI.ActualSheafTensor.pure_smul_left line 425
  30. lemma OAI.ActualSheafTensor.pure_smul_right line 433
  31. lemma OAI.ActualSheafTensor.powerSection_smul line 441
  32. lemma OAI.ActualSheafTensor.powerSection_restrict line 454
  33. def OAI.ActualSheafTensor.powerUnitIso line 476
  34. lemma OAI.ActualSheafTensor.powerUnitIso_hom_section line 482
  35. lemma OAI.ActualSheafTensor.powerUnitIso_inv_one line 499
  36. def OAI.ActualSheafTensor.tensorRightIso line 513
  37. lemma OAI.ActualSheafTensor.tensorRightIso_inv_pure line 517
  38. def OAI.ActualSheafTensor.powerOverIso line 527
  39. lemma OAI.ActualSheafTensor.tensorOverIso_inv_pure line 533
  40. lemma OAI.ActualSheafTensor.powerOverIso_step line 542
  41. lemma OAI.ActualSheafTensor.powerOverIso_inv_section line 571
  42. def OAI.ActualLineFrames.overPowerFrameIso line 591
  43. lemma OAI.ActualLineFrames.overPowerFrameIso_frame line 596
  44. lemma OAI.ActualLineFrames.powerFrame_matching line 606
  45. lemma OAI.ActualLineFrames.section_transition_restrict line 623
  46. lemma OAI.ActualLineFrames.section_transition_power_restrict line 633
  47. lemma OAI.ActualLineFrames.section_power_frame_restrict line 653
  48. lemma OAI.ActualLineFrames.section_scalar_power_frame_restrict line 664
  49. lemma OAI.SourceSymmetry.coefficientOverlap_image line 692
  50. def OAI.SourceSymmetry.overlapScalar line 699
  51. lemma OAI.SourceSymmetry.canonical_frame_power_transition line 704
  52. lemma OAI.SourceSymmetry.conormal_frame_linear_transition line 717
  53. lemma OAI.SourceSymmetry.canonical_conormal_matching_frames line 732
  54. lemma OAI.SourceSymmetry.canonical_originalConormal_pow5 line 749

    Source documentation

    The canonical/polarization identification on the surface.

    lemma canonical_originalConormal_pow5 :
    Nonempty (canonicalSheaf ≅ tensorPower projectiveSurface.sheaf originalConormal 5) := by
…

    Mentions: OAI.SourceSymmetry.canonicalSheaf, OAI.SourceSymmetry.originalConormal

  55. lemma OAI.SourceSymmetry.coefficientChart_regular line 765
  56. lemma OAI.SourceSymmetry.projChart_regular line 770
  57. lemma OAI.SourceSymmetry.regularStalk_spec line 775
  58. lemma OAI.SourceSymmetry.regularStalk_open line 780
  59. theorem OAI.SourceSymmetry.projectiveSurface_regular line 786

    Source documentation

    Regularity at EVERY point of the normalized source surface.

    theorem projectiveSurface_regular (x : projectiveSurface) :
    IsRegularLocalRing (projectiveSurface.presheaf.stalk x) := by
…
  60. lemma OAI.SourceSymmetry.dimension_le_of_open_cover line 810
  61. lemma OAI.SourceSymmetry.projChart_dimension line 830
  62. lemma OAI.SourceSymmetry.smoothOpen_dimension line 838
  63. theorem OAI.SourceSymmetry.projectiveSurface_dimension line 849

    Source documentation

    The source Proj is a surface.

    theorem projectiveSurface_dimension : topologicalKrullDim projectiveSurface = 2 := by
…