Documentation

MazurTorsion.NumberTheory.CyclotomicKummerFrobeniusCoordinate

Kummer coordinates for finite-prime Frobenius products #

This file changes the cyclic coordinate of an inverse-cyclotomic extension to the root-of-unity coordinate supplied by a Kummer presentation. It then extends the local Frobenius values to a finite product on nonzero fractional ideals. No principal product formula or reciprocity principle is asserted here.

source
noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.coordinateEquiv {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) :
Multiplicative (ZMod p) ≃* ↥(rootsOfUnity p (PrimeCyclotomicField p))

Change from the cyclic coordinate packaged in an inverse extension to the root-of-unity coordinate supplied by a Kummer presentation.

Equations
Instances For
    source
    noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.localKummerFrobeniusSymbol {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) (v : FinitePrime (PrimeCyclotomicField p)) :
    ↥(rootsOfUnity p (PrimeCyclotomicField p))

    The local arithmetic Frobenius symbol in the Kummer root-of-unity coordinate.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.localKummerFrobeniusSymbol_eq_pairing {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) (v : FinitePrime (PrimeCyclotomicField p)) :
      localKummerFrobeniusSymbol E P v = (pairing E P) (E.frobeniusAt v)

      The local Kummer symbol is the Kummer pairing evaluated on the selected arithmetic Frobenius automorphism.

      source
      noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.fractionalKummerSymbol {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) :
      (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (PrimeCyclotomicField p))ˣ →* ↥(rootsOfUnity p (PrimeCyclotomicField p))

      Extend the local Kummer/Frobenius symbols to nonzero fractional ideals. By construction this is the finite product over the prime divisor of the fractional ideal.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.fractionalKummerSymbol_prime {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) (v : FinitePrime (PrimeCyclotomicField p)) :
        (fractionalKummerSymbol E P) (UnramifiedArtin.primeFractionalIdealUnit v) = localKummerFrobeniusSymbol E P v

        On a prime fractional ideal, the finite product is the corresponding local Kummer/Frobenius symbol.

        source
        theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.fractionalKummerSymbol_apply {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (PrimeCyclotomicField p))ˣ) :
        (fractionalKummerSymbol E P) I = ((UnramifiedArtin.fractionalIdealDivisor (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Additive.ofMul I)).prod fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (n : ℤ) => localKummerFrobeniusSymbol E P v ^ n

        Explicit finite-product formula for a fractional Kummer symbol.

        source
        theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.fractionalKummerSymbol_eq_coordinate_comp {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) :
        fractionalKummerSymbol E P = (coordinateEquiv E P).toMonoidHom.comp E.fractionalArtin

        The fractional Kummer symbol is exactly the original fractional Artin map followed by the change to Kummer coordinates.