OAI/AlgebraicGeometry/SurfaceCones/AffineFrameSection.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

An affine module basis induces a line frame in its associated sheaf.

  1. lemma OAI.ActualLineFrames.tildeSelf_inv_one line 22
  2. lemma OAI.ActualLineFrames.affineUnit_chartFrame line 27
  3. lemma OAI.SourceSymmetry.coefficientCanonicalIso_eq_top line 46
  4. lemma OAI.SourceSymmetry.canonicalFrameSection_affine line 51
  5. lemma OAI.SourceSymmetry.canonicalFrameSection_chartFrame line 59
  6. instance OAI.SourceSymmetry.canonicalFrameSection_isIso line 66
  7. def OAI.SourceSymmetry.canonicalOpenUnitIso line 72
  8. lemma OAI.SourceSymmetry.canonicalOpenUnitIso_frame line 77
  9. lemma OAI.ActualSections.section_eq_of_appTop line 95
  10. lemma OAI.AlgebraicGeometry.Scheme.coordinateMap_precomp_apply line 120
  11. lemma OAI.AlgebraicGeometry.Scheme.coordinateMap_spec line 123
  12. lemma OAI.AlgebraicGeometry.Scheme.coordinateMap_ideal_of_cover line 129
  13. def OAI.SourcePullbackChart.degreeOneFunction line 153
  14. lemma OAI.SourcePullbackChart.degreeOneFunction_vanishes line 157
  15. def OAI.SourcePullbackChart.degreeOneIdealGenerator line 176

    Source documentation

    degree-one global section of the Cartier ideal.

    def degreeOneIdealGenerator (c : ExplicitCone.L) (hc : c ∈ ExplicitCone.pieces 1) :
    SheafOfModules.unit W.ringCatSheaf ⟶ ActualCartier.idealSheaf completedSourceZero :=
…

    Mentions: OAI.ExplicitCone.L, OAI.ExplicitCone.pieces, OAI.ActualCartier.idealSheaf

  16. def OAI.SourcePullbackChart.degreeOneConormalGenerator line 182

    Source documentation

    Degree-one section of the conormal line on the source X.

    def degreeOneConormalGenerator (c : ExplicitCone.L) (hc : c ∈ ExplicitCone.pieces 1) :
    SheafOfModules.unit ExplicitCone.projectiveSurface.ringCatSheaf ⟶
      (Scheme.Modules.pullback completedSourceZero).obj
        (ActualCartier.idealSheaf completedSourceZero) :=
…

    Mentions: OAI.ExplicitCone.L, OAI.ExplicitCone.pieces, OAI.ActualCartier.idealSheaf

  17. def OAI.SourcePullbackChart.degreeOneCoefficient line 207
  18. lemma OAI.SourcePullbackChart.degreeOneCoefficient_self line 213
  19. def OAI.SourcePullbackChart.completedDegreeOneCoefficient line 223
  20. lemma OAI.SourcePullbackChart.degreeOneFunction_chart line 227
  21. lemma OAI.SourcePullbackChart.degreeOneParameter_chart line 249
  22. lemma OAI.SourcePullbackChart.degreeOneFunction_chart_ratio line 258
  23. lemma OAI.SourcePullbackChart.degreeOneParameterIdeal_chart_isIso line 267
  24. lemma OAI.SourcePullbackChart.completedDegreeOneCoefficient_residue line 284
  25. lemma OAI.ActualSections.map_ratio_of_commute line 301
  26. lemma OAI.ActualSections.unit_scalar_comm line 315
  27. lemma OAI.ActualSections.ratio_across_natIso line 330
  28. lemma OAI.ActualChartPullback.section_ratio line 364
  29. lemma OAI.ActualSections.restrict_scalar_inv line 407
  30. lemma OAI.ActualSections.scalar_isIso line 420
  31. lemma OAI.ActualSections.scalar_comp_congr line 434
  32. lemma OAI.ActualChartPullback.section_ratio_eq line 445
  33. lemma OAI.ActualChartPullback.section_isIso line 457
  34. def OAI.SourcePullbackChart.degreeOneConormalChartSection line 482
  35. lemma OAI.SourcePullbackChart.degreeOneParameterConormal_chart_isIso line 490
  36. lemma OAI.SourcePullbackChart.zeroChart_degreeOneCoefficient line 499
  37. lemma OAI.SourcePullbackChart.degreeOneConormalChartSection_ratio line 525
  38. lemma OAI.ActualSections.isUnit_appTop_of_range line 551
  39. lemma OAI.ActualSections.restrict_scalar_isIso line 559
  40. lemma OAI.ActualSections.isIso_of_openImmersion_cover line 568
  41. lemma OAI.ActualSections.restrict_cover_range line 582
  42. lemma OAI.ActualSections.isIso_restrict_of_local_frames line 592
  43. lemma OAI.SourcePullbackChart.surfaceChart_degreeOne_open line 640
  44. lemma OAI.SourcePullbackChart.degreeOneConormal_isIso_on line 654

    Source documentation

    Original conormal generator on its exact Proj nonvanishing locus.

    lemma degreeOneConormal_isIso_on (c : L) (hc : c ∈ pieces 1) :
    IsIso ((restrictFunctor (Proj.basicOpen (homogeneous pieces) (linearSection pieces c hc)).ι).map
      (degreeOneConormalGenerator c hc)) := by
…

    Mentions: OAI.SourcePullbackChart.degreeOneConormalGenerator

  45. lemma OAI.ActualSections.scalar_mul line 677
  46. lemma OAI.ActualSections.restrict_ratio_comp line 684
  47. lemma OAI.ActualSections.restrict_ratio_of_comp line 703
  48. lemma OAI.ActualSections.ratio_of_common_frame line 724
  49. def OAI.AlgebraicGeometry.Proj.degreeOneLeft line 741
  50. def OAI.AlgebraicGeometry.Proj.degreeOneRight line 744
  51. instance OAI.AlgebraicGeometry.Proj.degreeOneLeft_open line 747
  52. instance OAI.AlgebraicGeometry.Proj.degreeOneRight_open line 749
  53. lemma OAI.AlgebraicGeometry.Proj.degreeOneLeft_eq line 751
  54. lemma OAI.AlgebraicGeometry.Proj.degreeOneRight_eq line 754
  55. lemma OAI.AlgebraicGeometry.Proj.degreeOne_overlap_square line 757
  56. lemma OAI.AlgebraicGeometry.Proj.degreeOneRight_range line 761
  57. lemma OAI.AlgebraicGeometry.Proj.degreeOne_intersection_right_cover line 766
  58. lemma OAI.HomogeneousLocalization.degreeOne_overlap_ratio line 782
  59. lemma OAI.ActualSections.specMap_inv line 801
  60. lemma OAI.ActualSections.ratio_along_eq line 805
  61. abbrev OAI.AlgebraicGeometry.Proj.degreeOneFraction line 821

    Source documentation

    A homogeneous degree-one quotient.

    abbrev degreeOneFraction {f c : A} (hf : f ∈ 𝒜 1) (hc : c ∈ 𝒜 1) : Away 𝒜 f :=
…
  62. lemma OAI.AlgebraicGeometry.Proj.degreeOne_coefficient_identity line 823
  63. lemma OAI.AlgebraicGeometry.Proj.degreeOne_section_ratio line 835