Nyll.Yamaguchi26AbfaithfulGalois.Kummer.Concrete.MixedCharInvariantKummerTrace

Module documentation

Constructing an invariant moved Kummer trace at the last root level

The original prime degree and the two cyclotomic extensions supply the upper prime-degree Galois extension. A nonidentity automorphism, an eigenunit with primitive eigenvalue, and the last positive root level are chosen internally. If the roots at that level descend, their actual Kummer trace is invariant under the cyclotomic group and moved by the chosen automorphism.

theorem

exists_lastLevel_invariant_moved_cyclotomicKummerTrace

L38 ↗

ClassFieldTower.Martinet.Shafarevich.exists_lastLevel_invariant_moved_cyclotomicKummerTrace

Documentation

A mixed-characteristic discrete valuation and the original prime-degree extension produce a last root level and, in the roots-downstairs branch, an actual invariant character moved by an internally selected automorphism.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ValuationTheory.DiscreteValuationField

-- Four fields, five algebras and two towers give eleven supplied data structures.
-- The valuation is an ordinary bundle. Only finite-dimensionality, normality,
-- characteristic, Galoisness and nontriviality propositions are added locally.

Lean source · statement

theorem exists_lastLevel_invariant_moved_cyclotomicKummerTrace
    (F K L E : Type*) [Field F] [Field K] [Field L] [Field E]
    [Algebra F K] [Algebra F L] [Algebra F E] [Algebra K E] [Algebra L E]
    [IsScalarTower F K E] [IsScalarTower F L E] [Normal F K] [CharZero E]
    (p : ℕ) [Fact p.Prime]
    [IsCyclotomicExtension {p} F L] [IsCyclotomicExtension {p} K E]
    (hdegree : Module.finrank F K = p)
    (V : DVF E) [hres : CharP V.residueField p] :
    ∃ s : ℕ, (primitiveRoots (p ^ (s + 1)) E).Nonempty ∧
      (∀ m : ℕ, (primitiveRoots (p ^ m) E).Nonempty → m ≤ s + 1) ∧
      ¬ (primitiveRoots (p ^ (s + 2)) E).Nonempty ∧
      ((∀ ξ : E, ξ ^ (p ^ (s + 1)) = 1 → ξ ∈ Set.range (algebraMap L E)) →
        ∃ (τ : E ≃ₐ[L] E)
          (T : Gal(AlgebraicClosure E/E) →ₜ* Multiplicative (ZMod (p ^ (s + 1)))),
          (∀ δ : E ≃ₐ[K] E,
            absoluteContinuousCharacterAction (K := E)
              (A := Multiplicative (ZMod (p ^ (s + 1)))) δ.toRingEquiv T = T) ∧
          absoluteContinuousCharacterAction (K := E)
            (A := Multiplicative (ZMod (p ^ (s + 1)))) τ.toRingEquiv T ≠ T)

Module documentation

Constructing an invariant moved Kummer trace at the last root level

Declarations

exists_lastLevel_invariant_moved_cyclotomicKummerTrace