OAI/AlgebraicGeometry/SurfaceCones/KummerCanonicalCharts.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CanonicalCoordinates.volume_complement line 13
2. lemma OAI.CanonicalCoordinates.coordinateJacobian_diagonal line 18
3. lemma OAI.CanonicalCoordinates.coordinateJacobian_shifted line 28
4. lemma OAI.CanonicalCoordinates.coordinateJacobian_shiftedDiagonal line 38
5. def OAI.KummerTripleDiagonal.cotangentBasis line 78

   Source documentation

   The smooth normalization has cotangent basis du,dv.

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

   Mentions: OAI.KummerTripleDiagonal.chartRootAlgebra

6. def OAI.KummerTripleDiagonal.chartCoordinate line 82
7. lemma OAI.KummerTripleDiagonal.cotangentBasis_apply line 85
8. def OAI.KummerTripleDiagonal.remainingElement line 92
9. lemma OAI.KummerTripleDiagonal.remainingElement_pow line 95
10. lemma OAI.KummerTripleDiagonal.remainingElement_isUnit line 104
11. def OAI.KummerTripleDiagonal.remainingUnit line 108
12. lemma OAI.KummerTripleDiagonal.remainingUnit_val line 111
13. lemma OAI.KummerTripleDiagonal.remainingUnit_to_field line 115
14. lemma OAI.KummerTripleDiagonal.chartCoordinate_to_field line 139
15. def OAI.KummerTripleDiagonal.canonicalUnit line 144
16. lemma OAI.KummerTripleDiagonal.canonicalUnit_to_field line 148
17. lemma OAI.KummerTripleDiagonal.canonical_density_identity line 161
18. def OAI.KummerTripleDiagonal.canonicalFrame line 185
19. lemma OAI.KummerTripleDiagonal.canonicalFrame_to_field line 189
20. lemma OAI.KummerTripleDiagonal.canonicalForm_eq line 201
21. lemma OAI.KummerTripleDiagonal.canonical_density_scalar line 215
22. lemma OAI.KummerTripleDiagonal.canonicalFrame_rational line 223
23. def OAI.KummerShifted.cotangentBasis line 262

    Source documentation

    The smooth normalization has cotangent basis du,dv.

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

    Mentions: OAI.KummerShifted.chartRootAlgebra

24. def OAI.KummerShifted.chartCoordinate line 266
25. lemma OAI.KummerShifted.cotangentBasis_apply line 269
26. def OAI.KummerShifted.remainingElement line 276
27. lemma OAI.KummerShifted.remainingElement_pow line 279
28. lemma OAI.KummerShifted.remainingElement_isUnit line 288
29. def OAI.KummerShifted.remainingUnit line 292
30. lemma OAI.KummerShifted.remainingUnit_val line 295
31. lemma OAI.KummerShifted.remainingUnit_to_field line 299
32. lemma OAI.KummerShifted.chartCoordinate_to_field line 323
33. def OAI.KummerShifted.canonicalUnit line 328
34. lemma OAI.KummerShifted.canonicalUnit_to_field line 332
35. lemma OAI.KummerShifted.canonical_density_identity line 345
36. def OAI.KummerShifted.canonicalFrame line 369
37. lemma OAI.KummerShifted.canonicalFrame_to_field line 373
38. lemma OAI.KummerShifted.canonicalForm_eq line 385
39. lemma OAI.KummerShifted.canonical_density_scalar line 393
40. lemma OAI.KummerShifted.canonicalFrame_rational line 401
41. def OAI.KummerShiftedDiagonal.cotangentBasis line 440

    Source documentation

    The smooth normalization has cotangent basis du,dv.

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

    Mentions: OAI.KummerShiftedDiagonal.chartRootAlgebra

42. def OAI.KummerShiftedDiagonal.chartCoordinate line 444
43. lemma OAI.KummerShiftedDiagonal.cotangentBasis_apply line 447
44. def OAI.KummerShiftedDiagonal.remainingElement line 454
45. lemma OAI.KummerShiftedDiagonal.remainingElement_pow line 457
46. lemma OAI.KummerShiftedDiagonal.remainingElement_isUnit line 466
47. def OAI.KummerShiftedDiagonal.remainingUnit line 470
48. lemma OAI.KummerShiftedDiagonal.remainingUnit_val line 473
49. lemma OAI.KummerShiftedDiagonal.remainingUnit_to_field line 477
50. lemma OAI.KummerShiftedDiagonal.chartCoordinate_to_field line 501
51. def OAI.KummerShiftedDiagonal.canonicalUnit line 506
52. lemma OAI.KummerShiftedDiagonal.canonicalUnit_to_field line 510
53. lemma OAI.KummerShiftedDiagonal.canonical_density_identity line 523
54. def OAI.KummerShiftedDiagonal.canonicalFrame line 547
55. lemma OAI.KummerShiftedDiagonal.canonicalFrame_to_field line 551
56. lemma OAI.KummerShiftedDiagonal.canonicalForm_eq line 563
57. lemma OAI.KummerShiftedDiagonal.canonical_density_scalar line 571
58. lemma OAI.KummerShiftedDiagonal.canonicalFrame_rational line 579