OAI/AlgebraicGeometry/SurfaceCones/CotangentCoordinates.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CanonicalCoordinates.kaehlerModule line 10
2. def OAI.CanonicalCoordinates.exteriorSMul line 13
3. def OAI.CanonicalCoordinates.etaleBasis line 22

   Source documentation

   differentials of polynomial coordinates remain a basis after an étale map. This is used below on the Kummer normalization chart.

   def etaleBasis (e : MvPolynomial (Fin 2) k ≃ₐ[k] B) :
       Basis (Fin 2) A Ω[A⁄k] := by
   …

4. lemma OAI.CanonicalCoordinates.etaleBasis_apply line 40
5. lemma OAI.CanonicalCoordinates.coordinateJacobian_seven line 51

   Source documentation

   Jacobian of the local ramification coordinates in exterior algebra.

   lemma coordinateJacobian_seven {M : Type*} [AddCommGroup M] [Module A M] [Module k M]
       (d : Derivation k A M) (u v : A) :
       ExteriorAlgebra.ι A (d (u ^ 7)) *
         ExteriorAlgebra.ι A (d ((u * v) ^ 7)) =
       (49 * u ^ 13 * v ^ 6) •
         (ExteriorAlgebra.ι A (d u) * ExteriorAlgebra.ι A (d v)) := by
   …

6. def OAI.CanonicalCoordinates.topIndex line 73
7. lemma OAI.CanonicalCoordinates.topIndex_unique line 76
8. def OAI.CanonicalCoordinates.topIndexEquiv line 83
9. def OAI.CanonicalCoordinates.topModule line 89
10. def OAI.CanonicalCoordinates.topBasis line 94
11. lemma OAI.CanonicalCoordinates.topBasis_apply line 97
12. lemma OAI.CanonicalCoordinates.topBasis_coe line 107
13. def OAI.CanonicalCoordinates.unitTopBasis line 117

    Source documentation

    Multiplying the wedge of a cotangent basis by an ring unit still is a basis of the determinant line.

    def unitTopBasis (b : Basis (Fin 2) A M) (u : Aˣ) : Basis Unit A (⋀[A]^2 M) :=
    …

14. lemma OAI.CanonicalCoordinates.unitTopBasis_apply line 120
15. def OAI.CanonicalCoordinates.exteriorMulAction line 133
16. def OAI.CanonicalCoordinates.exteriorMap line 139
17. lemma OAI.CanonicalCoordinates.exteriorMap_D line 143
18. def OAI.CanonicalCoordinates.rationalBasis line 152

    Source documentation

    The rational cotangent basis induced from an affine étale coordinate chart agrees with the differentials of those very same coordinates.

    def rationalBasis [Algebra.FormallyEtale A F] (b : Basis (Fin 2) A Ω[A⁄k]) :
        Basis (Fin 2) F Ω[F⁄k] :=
    …

19. lemma OAI.CanonicalCoordinates.rationalBasis_apply line 156
20. lemma OAI.CanonicalCoordinates.towerViaMiddle line 163
21. lemma OAI.CanonicalCoordinates.unitTopBasis_coe line 172
22. lemma OAI.CanonicalCoordinates.exteriorMap_frame line 180