OAI/AlgebraicGeometry/SurfaceCones/KummerCanonical.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The triple-point chart has p^3 étale sheets over its ramified-coordinate algebra.

  1. lemma OAI.KummerTriple.coordinateRoot_mem_coordinateField line 13
  2. lemma OAI.KummerTriple.coordinateAlgebra_le_coordinateField line 21
  3. lemma OAI.KummerTriple.coordinateField_fractionRing line 38
  4. lemma OAI.KummerTriple.chartRootAlgebra_degree line 95
  5. def OAI.KummerTriple.cotangentBasis line 139

    Source documentation

    The smooth normalization has cotangent basis du,dv.

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

    Mentions: OAI.KummerTriple.chartRootAlgebra

  6. def OAI.KummerTriple.chartCoordinate line 143
  7. lemma OAI.KummerTriple.cotangentBasis_apply line 146
  8. lemma OAI.KummerTriple.cotangentJacobian_seven line 160

    Source documentation

    In particular the chart map to the affine plane has the Jacobian 49 u^13 v^6. The two coordinates are the source roots u = y₀ and v = y₁/y₀.

    lemma cotangentJacobian_seven :
    ExteriorAlgebra.ι (chartRootAlgebra p) (D ℂ _ ((chartCoordinate p 0) ^ 7)) *
      ExteriorAlgebra.ι (chartRootAlgebra p) (D ℂ _ ((chartCoordinate p 0 * chartCoordinate p 1) ^ 7)) =
    (49 * (chartCoordinate p 0) ^ 13 * (chartCoordinate p 1) ^ 6) •
      (ExteriorAlgebra.ι (chartRootAlgebra p) (D ℂ _ (chartCoordinate p 0)) *
        ExteriorAlgebra.ι (chartRootAlgebra p) (D ℂ _ (chartCoordinate p 1))) :=
…

    Mentions: OAI.KummerTriple.chartRootAlgebra, OAI.KummerTriple.chartCoordinate

  9. def OAI.KummerTriple.remainingElement line 181
  10. lemma OAI.KummerTriple.remainingElement_pow line 184
  11. lemma OAI.KummerTriple.remainingElement_isUnit line 193
  12. def OAI.KummerTriple.remainingUnit line 197
  13. lemma OAI.KummerTriple.remainingUnit_val line 200
  14. lemma OAI.KummerTriple.remainingUnit_to_field line 204
  15. def OAI.KummerTriple.canonicalUnit line 211

    Source documentation

    Unit multiplying du∧dv in the canonical frame c₀₀⁵ ω at n=7.

    def canonicalUnit : (chartRootAlgebra 7)ˣ :=
…

    Mentions: OAI.KummerTriple.chartRootAlgebra

  16. lemma OAI.KummerTriple.canonicalUnit_to_field line 215
  17. lemma OAI.KummerTriple.canonical_density_identity line 227

    Source documentation

    Exact Jacobian coefficient after multiplication by the fifth power of sectionCoefficient (0,0). All entries are roots in L.

    lemma canonical_density_identity :
    ExplicitCone.sectionCoefficient (0, 0) ^ 5 *
        (49 * (root 7 0) ^ 13 * (root 7 1 / root 7 0) ^ 6) /
      (∏ i : Fin 5, root 7 i) ^ 6 =
    algebraMap (chartRootAlgebra 7) (L 7) (canonicalUnit : chartRootAlgebra 7) := by
…

    Mentions: OAI.ExplicitCone.sectionCoefficient, OAI.KummerTriple.root, OAI.KummerTriple.chartRootAlgebra, OAI.KummerTriple.canonicalUnit

  18. def OAI.KummerTriple.canonicalFrame line 275

    Source documentation

    The regular frame expressed rationally as c₀₀⁵ dx∧dy/(∏yᵢ)^6. It is constructed in the determinant module.

    def canonicalFrame : Basis Unit (chartRootAlgebra 7)
    (⋀[chartRootAlgebra 7]^2 Ω[chartRootAlgebra 7⁄ℂ]) :=
…

    Mentions: OAI.KummerTriple.chartRootAlgebra

  19. lemma OAI.KummerTriple.canonicalFrame_apply line 279
  20. lemma OAI.KummerTriple.chartCoordinate_to_field line 330
  21. def OAI.KummerTriple.rationalCotangentBasis line 335
  22. lemma OAI.KummerTriple.rationalCotangentBasis_apply line 338
  23. def OAI.KummerTriple.canonicalForm line 344

    Source documentation

    The source's rational 2-form dx∧dy/(y₀y₁y₂y₃y₄)^6.

    def canonicalForm : ExteriorAlgebra (L 7) Ω[L 7⁄ℂ] :=
…
  24. lemma OAI.KummerTriple.canonicalFrame_to_field line 349
  25. lemma OAI.KummerTriple.canonicalForm_eq line 361
  26. lemma OAI.KummerTriple.canonical_density_scalar line 373
  27. lemma OAI.KummerTriple.canonicalFrame_rational line 384