OAI/AlgebraicGeometry/SurfaceCones/AffineCanonicalCoordinates.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

A canonical frame on the ordinary-node affine normalization chart.

  1. def OAI.CanonicalCoordinates.subalgebraMonoid line 10
  2. lemma OAI.CanonicalCoordinates.coordinateJacobian_affine line 14
  3. abbrev OAI.KummerAffineZero.root line 29
  4. abbrev OAI.KummerAffineZero.C line 30
  5. abbrev OAI.KummerAffineZero.B line 31
  6. abbrev OAI.KummerAffineZero.S line 32
  7. abbrev OAI.KummerAffineZero.chartRootAlgebra line 33
  8. abbrev OAI.KummerAffineZero.planeEquiv line 35
  9. abbrev OAI.KummerAffineZero.bRoot line 36
  10. abbrev OAI.KummerAffineZero.coordinateRoot line 37
  11. abbrev OAI.KummerAffineZero.chartRootAlgebra_finiteFreeEtale line 38
  12. abbrev OAI.KummerAffineZero.remainingRoot line 40
  13. abbrev OAI.KummerAffineZero.remainingForm line 42
  14. abbrev OAI.KummerAffineZero.remainingRoot_mem_chartRootAlgebra line 43
  15. abbrev OAI.KummerAffineZero.remaining_unit line 45
  16. abbrev OAI.KummerAffineZero.exponent_unit line 46
  17. abbrev OAI.KummerAffineZero.root_ne_zero line 47
  18. lemma OAI.KummerAffineZero.remainingRoot_pow line 48
  19. def OAI.KummerAffineZero.cotangentBasis line 75

    Source documentation

    The smooth normalization has cotangent basis du,dv.

    def cotangentBasis : Basis (Fin 2) (chartRootAlgebra p) Ω[chartRootAlgebra p⁄ℂ] :=
…

    Mentions: OAI.KummerAffineZero.chartRootAlgebra

  20. def OAI.KummerAffineZero.chartCoordinate line 79
  21. lemma OAI.KummerAffineZero.cotangentBasis_apply line 82
  22. def OAI.KummerAffineZero.remainingElement line 89
  23. lemma OAI.KummerAffineZero.remainingElement_pow line 92
  24. lemma OAI.KummerAffineZero.remainingElement_isUnit line 101
  25. def OAI.KummerAffineZero.remainingUnit line 105
  26. lemma OAI.KummerAffineZero.remainingUnit_val line 108
  27. lemma OAI.KummerAffineZero.remainingUnit_to_field line 112
  28. lemma OAI.KummerAffineZero.chartCoordinate_to_field line 136
  29. def OAI.KummerAffineZero.canonicalUnit line 141
  30. lemma OAI.KummerAffineZero.canonicalUnit_to_field line 145
  31. lemma OAI.KummerAffineZero.canonical_density_identity line 158
  32. def OAI.KummerAffineZero.canonicalFrame line 182
  33. lemma OAI.KummerAffineZero.canonicalFrame_to_field line 186
  34. lemma OAI.KummerAffineZero.canonicalForm_eq line 198
  35. lemma OAI.KummerAffineZero.canonical_density_scalar line 214
  36. lemma OAI.KummerAffineZero.canonicalFrame_rational line 222
  37. lemma OAI.CanonicalCoordinates.scalar_nonzero line 239
  38. lemma OAI.CanonicalCoordinates.scalar_unique line 241
  39. lemma OAI.CanonicalCoordinates.basis_volume_ne_zero line 244
  40. lemma OAI.KummerTriple.canonicalForm_ne_zero line 261
  41. lemma OAI.SourceSymmetry.canonicalDensity_ne_zero line 282
  42. lemma OAI.SourceSymmetry.canonicalDensity_ratio line 286

    Source documentation

    Exact fifth-power transition, in the common fraction field.

    lemma canonicalDensity_ratio (s t : SectionIndex) :
    canonicalDensity s = (sectionCoefficient s / sectionCoefficient t)^5 • canonicalDensity t := by
…

    Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.canonicalDensity

  43. lemma OAI.SourceSymmetry.canonicalDensity_scalar_unique line 291
  44. def OAI.CanonicalCoordinates.rationalExteriorAlgebra line 304
  45. theorem OAI.CanonicalCoordinates.rationalExteriorTower line 306
  46. lemma OAI.CanonicalCoordinates.unitBasis_repr line 313
  47. lemma OAI.CanonicalCoordinates.rankOne_range line 317
  48. lemma OAI.CanonicalCoordinates.rankOne_injective line 331
  49. def OAI.CanonicalCoordinates.determinantMap line 349

    Source documentation

    The natural map from the determinant module to rational forms.

    def determinantMap : (⋀[A]^2 Ω[A⁄k]) →ₗ[A] ExteriorAlgebra F Ω[F⁄k] :=
…
  50. lemma OAI.CanonicalCoordinates.determinantMap_apply line 352
  51. lemma OAI.CanonicalCoordinates.determinantImage line 355
  52. lemma OAI.KummerTriple.canonicalImage line 402
  53. lemma OAI.KummerTriple.determinantMap_injective line 409
  54. lemma OAI.KummerTripleDiagonal.canonicalImage line 452
  55. lemma OAI.KummerTripleDiagonal.determinantMap_injective line 459
  56. lemma OAI.KummerShifted.canonicalImage line 502
  57. lemma OAI.KummerShifted.determinantMap_injective line 509
  58. lemma OAI.KummerShiftedDiagonal.canonicalImage line 552
  59. lemma OAI.KummerShiftedDiagonal.determinantMap_injective line 559
  60. lemma OAI.KummerAffineZero.canonicalImage line 602
  61. lemma OAI.KummerAffineZero.determinantMap_injective line 609
  62. def OAI.CanonicalCoordinates.rationalWedge line 628

    Source documentation

    A wedge of two rational differentials.

    def rationalWedge (a b : F) : ExteriorAlgebra F Ω[F⁄k] :=
…
  63. lemma OAI.CanonicalCoordinates.determinantMap_volume line 631
  64. lemma OAI.CanonicalCoordinates.determinantMap_generators line 639
  65. lemma OAI.CanonicalCoordinates.determinantMap_generators_of_derivations line 670
  66. lemma OAI.CanonicalCoordinates.determinantImage_localization line 694
  67. lemma OAI.CanonicalCoordinates.submodule_eq_of_local_spans line 719
  68. lemma OAI.FieldPrincipalOpen.determinantImage_away line 741
  69. lemma OAI.FieldPrincipalOpen.determinantImage_away_frame line 747
  70. lemma OAI.FieldPrincipalOpen.determinantImage_congr line 757
  71. lemma OAI.FieldPrincipalOpen.determinantImage_of_away line 766
  72. lemma OAI.ExplicitCone.tripleRegular_canonicalImage line 793
  73. lemma OAI.ExplicitCone.diagonalRegular_canonicalImage line 799
  74. lemma OAI.ExplicitCone.shiftedRegular_canonicalImage line 805
  75. lemma OAI.ExplicitCone.shiftedDiagonalRegular_canonicalImage line 811
  76. lemma OAI.ExplicitCone.affineRegular_canonicalImage line 817
  77. lemma OAI.ExplicitCone.affinePunctured_canonicalImage line 823
  78. def OAI.ExplicitCone.canonicalCoverDenominators line 829
  79. lemma OAI.ExplicitCone.canonicalCoverDenominators_ne_zero line 834
  80. lemma OAI.ExplicitCone.canonicalCoverDenominators_span line 843
  81. def OAI.ExplicitCone.canonicalCoverOpen line 858

    Source documentation

    The five principal-open coefficient algebras used to compute the determinant lattice.

    def canonicalCoverOpen (i : Fin 5) : Subalgebra ℂ L :=
…

    Mentions: OAI.ExplicitCone.L

  82. lemma OAI.ExplicitCone.canonicalCover_image line 862
  83. lemma OAI.ExplicitCone.sectionChart_canonicalImage line 883

    Source documentation

    The top-Kahler image.

    lemma sectionChart_canonicalImage :
    LinearMap.range (determinantMap ℂ sectionChart L) =
      Submodule.span sectionChart {SourceSymmetry.canonicalDensity (0,0)} := by
…

    Mentions: OAI.ExplicitCone.sectionChart, OAI.ExplicitCone.L, OAI.SourceSymmetry.canonicalDensity