OAI/AlgebraicGeometry/SurfaceCones/KummerGalois.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

The five line ratios are independent modulo p-th powers, by their line valuations.

  1. lemma OAI.KummerLines.lineForm_not_dvd line 10
  2. lemma OAI.KummerLines.emultiplicity_lineProduct line 17
  3. lemma OAI.KummerLines.radicand_ne_zero line 27
  4. lemma OAI.KummerLines.radicand_pow_independent line 33

    Source documentation

    affine-line valuation independence, with bounded exponents. If two radical monomials differ by a p-th power in the rational function field, their vectors of exponents modulo p agree.

    lemma radicand_pow_independent (p : ℕ) (hp : 0 < p)
    (e f : Fin 5 → Fin p) (z : K)
    (hz : ∏ i, radicand i ^ (e i).val = z ^ p * ∏ i, radicand i ^ (f i).val) :
    e = f := by
…

    Mentions: OAI.KummerLines.K, OAI.KummerLines.radicand

  5. abbrev OAI.KummerLines.actualRoot line 89
  6. lemma OAI.KummerLines.actualRoot_pow line 91
  7. lemma OAI.KummerLines.actualRoot_ne_zero line 94
  8. abbrev OAI.KummerLines.primitiveScalar line 100
  9. lemma OAI.KummerLines.primitiveScalar_root line 101
  10. lemma OAI.KummerLines.primitiveScalar_map_root line 104
  11. lemma OAI.KummerLines.rootPolynomial_splits line 108
  12. instance OAI.KummerLines.actual_rootField_normal line 113
  13. instance OAI.KummerLines.actual_rootField_galois line 132
  14. lemma OAI.KummerLines.aut_fixes_rootUnity line 136

    Source documentation

    Every p-th root of unity in the extension is a complex scalar, hence fixed by every base-field automorphism.

    lemma aut_fixes_rootUnity (σ : L p ≃ₐ[K] L p) (x : L p) (hx : x ^ p = 1) :
    σ x = x := by
…

    Mentions: OAI.KummerLines.L, OAI.KummerLines.K

  15. lemma OAI.KummerLines.aut_quotient_pow line 143
  16. def OAI.KummerLines.radicalCharacter line 150

    Source documentation

    The action character of a radical monomial.

    def radicalCharacter (x : L p) (hx : x ≠ 0) (a : K)
    (ha : x ^ p = algebraMap K (L p) a) : (L p ≃ₐ[K] L p) →* L p where
…

    Mentions: OAI.KummerLines.L, OAI.KummerLines.K

  17. abbrev OAI.KummerLines.radicalMonomial line 164
  18. abbrev OAI.KummerLines.radicandMonomial line 165
  19. lemma OAI.KummerLines.radicalMonomial_ne_zero line 166
  20. lemma OAI.KummerLines.radicalMonomial_pow line 168
  21. def OAI.KummerLines.monomialCharacter line 176
  22. lemma OAI.KummerLines.monomialCharacter_injective line 180
  23. lemma OAI.KummerLines.radicalMonomial_linearIndependent line 212
  24. lemma OAI.KummerLines.radicalMonomial_degree_lower line 238
  25. def OAI.KummerLines.rootAction line 242

    Source documentation

    action on the five chosen radicals, with values in the roots of unity.

    def rootAction (σ : L p ≃ₐ[K] L p) (i : Fin 5) : rootsOfUnity p (L p) :=
…

    Mentions: OAI.KummerLines.L, OAI.KummerLines.K

  26. lemma OAI.KummerLines.rootAction_injective line 250
  27. lemma OAI.KummerLines.actual_rootField_degree line 261
  28. lemma OAI.KummerLines.rootAction_bijective line 278
  29. def OAI.KummerLines.radicalBasis line 285

    Source documentation

    Basis of the source field by its radical monomials.

    def radicalBasis : Module.Basis (Fin 5 → Fin p) K (L p) :=
…

    Mentions: OAI.KummerLines.K, OAI.KummerLines.L

  30. lemma OAI.KummerLines.offBranchCover_degree line 301
  31. abbrev OAI.KummerLines.coordinateField line 322
  32. lemma OAI.KummerLines.rootAction_eq_one_iff line 325
  33. lemma OAI.KummerLines.mem_coordinateFix_iff line 338
  34. def OAI.KummerLines.coordinateAction line 357

    Source documentation

    The fixing subgroup, with precisely the three remaining scalars.

    def coordinateAction (σ : (coordinateField p).fixingSubgroup)
    (i : Fin 3) : rootsOfUnity p (L p) := rootAction p σ.val (Fin.natAdd 2 i)

    Mentions: OAI.KummerLines.coordinateField, OAI.KummerLines.L, OAI.KummerLines.rootAction

  35. lemma OAI.KummerLines.coordinateAction_injective line 360
  36. lemma OAI.KummerLines.coordinateAction_surjective line 372
  37. lemma OAI.KummerLines.coordinateField_degree line 386