OAI/AlgebraicGeometry/SurfaceCones/KummerSymmetry.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

Projective symmetries of the complete quadrangle lift to its Kummer extension.

  1. abbrev OAI.SourceSymmetry.A line 9
  2. def OAI.SourceSymmetry.closureLift line 12

    Source documentation

    Lift a complex-linear automorphism of the rational function field to its algebraic closure.

    def closureLift (σ : K ≃ₐ[ℂ] K) : A ≃ₐ[ℂ] A :=
…

    Mentions: OAI.SourceSymmetry.A

  3. lemma OAI.SourceSymmetry.closureLift_base line 21
  4. lemma OAI.SourceSymmetry.scalar_of_power line 27

    Source documentation

    Over the algebraically closed ground field every element with a scalar positive power is itself a scalar.

    lemma scalar_of_power {E : Type*} [Field E] [Algebra ℂ E]
    {n : ℕ} (hn : 0 < n) {x : E} {a : ℂ}
    (hx : x ^ n = algebraMap ℂ E a) : ∃ c : ℂ, algebraMap ℂ E c = x := by
…
  5. def OAI.SourceSymmetry.lineValue line 36

    Source documentation

    Six homogeneous forms in the affine rational trivialization.

    def lineValue : Fin 6 → K := Fin.cases 1 KummerLines.radicand

    Mentions: OAI.KummerLines.radicand

  6. lemma OAI.SourceSymmetry.z_pow line 38
  7. lemma OAI.SourceSymmetry.ambient_z_pow line 43
  8. lemma OAI.SourceSymmetry.ambient_z_ne_zero line 46
  9. lemma OAI.SourceSymmetry.transformed_roots line 52

    Source documentation

    Projectively permuting the six line forms in the base field really permutes the six Kummer roots up to nonzero complex scalar and the same projective denominator in the chosen algebraic closure.

    lemma transformed_roots (σ : K ≃ₐ[ℂ] K) (π : Equiv.Perm (Fin 6))
    (a : Fin 6 → ℂ)
    (hσ : ∀ i, σ (lineValue i) =
      algebraMap ℂ K (a i) * (lineValue (π i) / lineValue (π 0))) :
    ∀ i, ∃ c : ℂ, c ≠ 0 ∧ closureLift σ (z i : A) =
      algebraMap ℂ A c * ((z (π i) : A) / (z (π 0) : A)) := by
…

    Mentions: OAI.SourceSymmetry.lineValue, OAI.SourceSymmetry.closureLift, OAI.SourceSymmetry.A

  10. lemma OAI.SourceSymmetry.closureLift_mem line 77

    Source documentation

    The lifted automorphism maps the five-root subfield to itself.

    lemma closureLift_mem (σ : K ≃ₐ[ℂ] K) (π : Equiv.Perm (Fin 6))
    (a : Fin 6 → ℂ)
    (hσ : ∀ i, σ (lineValue i) =
      algebraMap ℂ K (a i) * (lineValue (π i) / lineValue (π 0)))
    (x : L) : closureLift σ (x : A) ∈ L := by
…

    Mentions: OAI.SourceSymmetry.lineValue, OAI.SourceSymmetry.closureLift, OAI.SourceSymmetry.A

  11. def OAI.SourceSymmetry.rootMap line 105

    Source documentation

    Restriction of a lifted projective line-arrangement symmetry to the Kummer field.

    def rootMap (σ : K ≃ₐ[ℂ] K) (π : Equiv.Perm (Fin 6))
    (a : Fin 6 → ℂ)
    (hσ : ∀ i, σ (lineValue i) =
      algebraMap ℂ K (a i) * (lineValue (π i) / lineValue (π 0))) : L →ₐ[ℂ] L :=
…

    Mentions: OAI.SourceSymmetry.lineValue

  12. lemma OAI.SourceSymmetry.rootMap_z line 116
  13. lemma OAI.SourceSymmetry.rootMap_surjective line 125
  14. def OAI.SourceSymmetry.rootEquiv line 153

    Source documentation

    The Kummer field carries every projective symmetry of the six line arrangement that is supplied by an rational-function automorphism.

    def rootEquiv (σ : K ≃ₐ[ℂ] K) (π : Equiv.Perm (Fin 6))
    (a : Fin 6 → ℂ) (hσ : ∀ i, σ (lineValue i) =
      algebraMap ℂ K (a i) * (lineValue (π i) / lineValue (π 0))) : L ≃ₐ[ℂ] L :=
…

    Mentions: OAI.SourceSymmetry.lineValue

  15. abbrev OAI.SourceSymmetry.coord line 167

    Source documentation

    The affine coordinate x in the exact source rational function field.

    abbrev coord (i : Fin 2) : K := algebraMap R K (X i)
  16. lemma OAI.SourceSymmetry.coord_ne_zero line 169
  17. lemma OAI.SourceSymmetry.xPowers_le line 172
  18. def OAI.SourceSymmetry.xOpen line 176
  19. instance OAI.SourceSymmetry.(instance at line 179) line 179
  20. instance OAI.SourceSymmetry.(instance at line 182) line 182
  21. abbrev OAI.SourceSymmetry.ax line 185
  22. def OAI.SourceSymmetry.ix line 187
  23. lemma OAI.SourceSymmetry.ax_ix line 189
  24. lemma OAI.SourceSymmetry.ix_unit line 190
  25. def OAI.SourceSymmetry.invertEval line 192
  26. lemma OAI.SourceSymmetry.invertEval_x line 194
  27. lemma OAI.SourceSymmetry.invertEval_y line 195
  28. def OAI.SourceSymmetry.invertHom line 198

    Source documentation

    The projective involution (x,y) ↦ (1/x,y/x), constructed on its principal open before extending to the function field.

    def invertHom : xOpen →ₐ[ℂ] xOpen :=
…

    Mentions: OAI.SourceSymmetry.xOpen

  29. lemma OAI.SourceSymmetry.invertHom_base line 202
  30. lemma OAI.SourceSymmetry.invertHom_x line 206
  31. lemma OAI.SourceSymmetry.invertHom_y line 207
  32. lemma OAI.SourceSymmetry.invertHom_ix line 209
  33. lemma OAI.SourceSymmetry.invertHom_involutive line 217
  34. def OAI.SourceSymmetry.invertOpenEquiv line 230
  35. def OAI.SourceSymmetry.invertBase line 233
  36. lemma OAI.SourceSymmetry.ix_coe line 236
  37. lemma OAI.SourceSymmetry.invertBase_x line 243
  38. lemma OAI.SourceSymmetry.invertBase_y line 249
  39. def OAI.SourceSymmetry.swapPolynomial line 258
  40. def OAI.SourceSymmetry.reflectPolynomial line 263
  41. def OAI.SourceSymmetry.swapBase line 268
  42. def OAI.SourceSymmetry.reflectBase line 270
  43. lemma OAI.SourceSymmetry.swapBase_coord line 272
  44. lemma OAI.SourceSymmetry.reflectBase_coord line 277
  45. def OAI.SourceSymmetry.swapLines line 282
  46. def OAI.SourceSymmetry.reflectLines line 288
  47. def OAI.SourceSymmetry.invertLines line 294
  48. lemma OAI.SourceSymmetry.lineValue_eq line 300
  49. def OAI.SourceSymmetry.swapScalars line 308
  50. def OAI.SourceSymmetry.reflectScalars line 309
  51. def OAI.SourceSymmetry.invertScalars line 310
  52. lemma OAI.SourceSymmetry.swapBase_lines line 312
  53. lemma OAI.SourceSymmetry.reflectBase_lines line 317
  54. lemma OAI.SourceSymmetry.invertBase_lines line 322
  55. def OAI.SourceSymmetry.rootSwap line 330

    Source documentation

    Three symmetries, generating the projective S₄ of the quadrangle.

    def rootSwap : L ≃ₐ[ℂ] L := rootEquiv swapBase swapLines swapScalars swapBase_lines

    Mentions: OAI.SourceSymmetry.rootEquiv, OAI.SourceSymmetry.swapBase, OAI.SourceSymmetry.swapLines, OAI.SourceSymmetry.swapScalars, OAI.SourceSymmetry.swapBase_lines

  56. def OAI.SourceSymmetry.rootReflect line 331
  57. def OAI.SourceSymmetry.rootInvert line 333
  58. def OAI.SourceSymmetry.ratioChart line 344
  59. lemma OAI.SourceSymmetry.ratioChart_generator line 347
  60. lemma OAI.SourceSymmetry.ratioChart_map_eq line 351
  61. def OAI.SourceSymmetry.ratioChartEquiv line 384
  62. abbrev OAI.SourceSymmetry.SectionIndex line 399
  63. def OAI.SourceSymmetry.coefficientChart line 401
  64. lemma OAI.SourceSymmetry.coefficient_ne_zero line 404
  65. lemma OAI.SourceSymmetry.coefficientChart_base line 407
  66. def OAI.SourceSymmetry.sectionPerm line 409
  67. def OAI.SourceSymmetry.swapPairs line 412
  68. def OAI.SourceSymmetry.invertPairs line 417
  69. lemma OAI.SourceSymmetry.swap_pair_products line 423
  70. lemma OAI.SourceSymmetry.reflect_pair_products line 428
  71. lemma OAI.SourceSymmetry.invert_pair_products line 433
  72. lemma OAI.SourceSymmetry.transformed_sections line 438
  73. def OAI.SourceSymmetry.sectionChartEquiv line 460
  74. def OAI.SourceSymmetry.swapSections line 476
  75. def OAI.SourceSymmetry.reflectSections line 477
  76. def OAI.SourceSymmetry.invertSections line 478
  77. def OAI.SourceSymmetry.swapChart line 480
  78. def OAI.SourceSymmetry.reflectChart line 484
  79. def OAI.SourceSymmetry.invertChart line 489
  80. def OAI.SourceSymmetry.stepPermutation line 500
  81. def OAI.SourceSymmetry.stepChart line 503
  82. def OAI.SourceSymmetry.applyWord line 509
  83. def OAI.SourceSymmetry.wordChart line 513
  84. def OAI.SourceSymmetry.Good line 518
  85. def OAI.SourceSymmetry.wordFor line 521
  86. lemma OAI.SourceSymmetry.wordFor_image line 529
  87. def OAI.SourceSymmetry.goodChartEquiv line 535
  88. lemma OAI.SourceSymmetry.coefficientChart_field line 547
  89. instance OAI.SourceSymmetry.coefficientChart_fractionRing line 567
  90. lemma OAI.SourceSymmetry.section_pow_10 line 576
  91. lemma OAI.SourceSymmetry.section_pow_40 line 582
  92. lemma OAI.SourceSymmetry.section_pow_21 line 588
  93. lemma OAI.SourceSymmetry.section_pow_31 line 594
  94. lemma OAI.SourceSymmetry.section_pow_52 line 600
  95. lemma OAI.SourceSymmetry.section_pow_02 line 606