OAI/AlgebraicGeometry/SurfaceCones/AffineExteriorSections.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

The affine exterior comparison on wedge sections.

  1. lemma OAI.AffineExterior.affineMap_unit line 27
  2. lemma OAI.AffineExterior.affineMap_basic_wedge line 33
  3. lemma OAI.AffineExterior.affineMap_top_wedge line 51
  4. lemma OAI.ActualExterior.openIso_inv_wedgeSection line 80
  5. lemma OAI.AffineExterior.affineIso_inv_top_wedge line 95
  6. def OAI.ActualExterior.openAffineIso line 115

    Source documentation

    The comparison of the top exterior sheaf on an affine open.

    def openAffineIso (e : M.restrict i ≅ tilde N) :
    ((sheafFunctor Y 2).obj M).restrict i ≅ tilde (N.exteriorPower 2) :=
…

    Mentions: OAI.ActualExterior.sheafFunctor

  7. lemma OAI.ActualExterior.openAffineIso_inv_wedge line 120
  8. lemma OAI.ActualExterior.openAffineInv_eval_wedge line 152
  9. def OAI.ActualSections.affineSection line 181
  10. lemma OAI.ActualSections.affineSection_zero line 184
  11. lemma OAI.ActualSections.affineSection_add line 188
  12. lemma OAI.ActualSections.affineSection_smul line 193
  13. def OAI.ActualCotangent.topSheaf line 223

    Source documentation

    The top exterior power of the cotangent sheaf.

    def topSheaf : Y.Modules := (ActualExterior.sheafFunctor Y 2).obj (sheaf g)

    Mentions: OAI.ActualExterior.sheafFunctor, OAI.ActualCotangent.sheaf

  14. def OAI.ActualCotangent.chartCoordinate line 226

    Source documentation

    The affine coordinate functions on their image in Y.

    def chartCoordinate : R →+* Γ(Y, i ''ᵁ ⊤) :=
…
  15. def OAI.ActualCotangent.topOpenAffineIso line 230

    Source documentation

    The intrinsic comparison on an affine open.

    def topOpenAffineIso : (topSheaf g).restrict i ≅
    tilde ((affineModule (k := k) R).exteriorPower 2) :=
…

    Mentions: OAI.ActualCotangent.topSheaf, OAI.ActualCotangent.affineModule

  16. def OAI.ActualCotangent.topChartSection line 236

    Source documentation

    Send a algebraic top differential to its intrinsic sheaf section.

    def topChartSection (m : (affineModule (k := k) R).exteriorPower 2) :
…

    Mentions: OAI.ActualCotangent.affineModule

  17. lemma OAI.ActualCotangent.topChartSection_volume line 241
  18. lemma OAI.ActualCotangent.topChartSection_zero line 251
  19. lemma OAI.ActualCotangent.topChartSection_add line 254
  20. lemma OAI.ActualCotangent.topChartSection_smul line 258
  21. lemma OAI.ActualSections.chart_coordinate_square line 277
  22. lemma OAI.ActualSections.chart_coordinate_restrict line 291
  23. lemma OAI.ActualSections.specMap_algebraMap line 313
  24. lemma OAI.ActualSections.affine_coordinate_restrict line 329
  25. lemma OAI.ActualCotangent.chartCoordinate_restrict line 362
  26. lemma OAI.ActualCotangent.topChartSection_volume_restrict line 369
  27. lemma OAI.ActualSections.eq_of_span_eq_top line 391
  28. lemma OAI.ActualCotangent.topChartSection_restrict line 428
  29. def OAI.ActualSections.scalarMul line 480
  30. lemma OAI.ActualSections.scalarMul_congr line 481
  31. lemma OAI.ActualCotangent.topChartSection_scalar line 496
  32. lemma OAI.SourceSymmetry.coefficientOverlapIota_toComplex line 514
  33. lemma OAI.SourceSymmetry.coefficientOverlap_le_left line 522
  34. lemma OAI.SourceSymmetry.coefficientOverlap_le_right line 529
  35. def OAI.SourceSymmetry.canonicalFrameSection line 537

    Source documentation

    The canonical generator, as a section of the intrinsic ∧² Ω.

    def canonicalFrameSection (s : SectionIndex) (hs : Good s) :
    Γ(canonicalSheaf, coefficientIota s hs ''ᵁ ⊤) :=
…

    Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.Good, OAI.SourceSymmetry.canonicalSheaf, OAI.SourceSymmetry.coefficientIota

  36. def OAI.SourceSymmetry.canonicalOverlapSection line 545

    Source documentation

    The intrinsic sheaf interpretation of an algebraic top form on the intersection.

    def canonicalOverlapSection (s t : SectionIndex) (hs : Good s)
    (m : ⋀[coefficientOverlap s t]^2 Ω[coefficientOverlap s t⁄ℂ]) :
    Γ(canonicalSheaf, coefficientOverlapIota s t hs ''ᵁ ⊤) :=
…

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

  37. lemma OAI.SourceSymmetry.canonicalFrameSection_restrict_left line 552
  38. lemma OAI.SourceSymmetry.canonicalFrameSection_restrict_right line 567
  39. lemma OAI.SourceSymmetry.intrinsic_canonical_transition line 582
  40. def OAI.ActualLineFrames.frame line 616
  41. lemma OAI.ActualLineFrames.frame_spans line 621
  42. lemma OAI.ActualLineFrames.frame_coordinate line 639
  43. lemma OAI.ActualLineFrames.exists_iso_of_matching_frames line 647
  44. def OAI.ActualLineFrames.overFromSection line 708
  45. lemma OAI.ActualLineFrames.overFromSection_app line 718
  46. lemma OAI.ActualLineFrames.overFromSection_top line 724
  47. lemma OAI.ActualLineFrames.overFromSection_frame line 731
  48. lemma OAI.ActualLineFrames.isIso_of_app_bijective line 747
  49. def OAI.ActualLineFrames.chartFrame line 770
  50. lemma OAI.ActualLineFrames.chartFrame_restrict line 773
  51. lemma OAI.ActualLineFrames.chartFrame_spans_bijective line 785
  52. lemma OAI.ActualLineFrames.chartFrame_on_open_bijective line 812
  53. lemma OAI.ActualLineFrames.chartFrame_isIso line 830