NYLL
Module

CyclotomicInvariantKummerTrace.lean

Nyll.GaloisCohomology.Kummer.Concrete.CyclotomicInvariantKummerTrace
2 declarations indexed from sourceView source ↗

Module documentation

An invariant Kummer trace retaining a nontrivial difference

The orbit product of an eigenunit's Kummer character is invariant under the upper cyclotomic group. The commuting automorphism changes it by the root's Kummer character to the cyclotomic degree. Coprimality prevents this nontrivial difference from disappearing.

Imports10
Imported by2

Declarations

theorem

invariant_moved_character_of_coprime

L33 ↗
ClassFieldTower.Martinet.Shafarevich.invariant_moved_character_of_coprime
Source context 2 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory GroupTheory

-- Keep the orbit calculation in its six-structure group/topology context;
-- it needs none of the four-field algebra towers of the Kummer construction.
Lean source · statement
theorem invariant_moved_character_of_coprime
    {G Γ A : Type*} [Group G] [Fintype G] [Monoid Γ] [TopologicalSpace Γ]
    [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A]
    (ρ : G →* MulAut (Γ →ₜ* A)) (a : MulAut (Γ →ₜ* A)) (C D : Γ →ₜ* A)
    (hcomm : ∀ g : G, Commute a (ρ g)) (hdiff : a C / C = D)
    (hD : ∀ g : G, ρ g D = D) (hDne : D ≠ 1)
    (hcop : (Nat.card A).Coprime (Fintype.card G)) :
    ∃ T : Γ →ₜ* A, (∀ g : G, ρ g T = T) ∧ a T ≠ T
theorem

exists_invariant_moved_cyclotomicKummerTrace

L66 ↗
ClassFieldTower.Martinet.Shafarevich.exists_invariant_moved_cyclotomicKummerTrace
Documentation

A root-valued eigenunit difference survives the actual cyclotomic orbit product. The root fixing and commutation are generated from the two fields.

Source context 3 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory GroupTheory

-- Keep the orbit calculation in its six-structure group/topology context;
-- it needs none of the four-field algebra towers of the Kummer construction.
variable {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]

-- Four fields, five algebras and two towers: eleven data structures.
-- The sole new local instance is the cyclotomic finite-dimensionality proposition.
Lean source · statement
theorem exists_invariant_moved_cyclotomicKummerTrace
    (p : ℕ) [Fact p.Prime]
    [IsCyclotomicExtension {p} F L] [IsCyclotomicExtension {p} K E]
    (s : ℕ) (hmu : (primitiveRoots (p ^ (s + 1)) E).Nonempty)
    (hdown : ∀ ξ : E, ξ ^ (p ^ (s + 1)) = 1 → ξ ∈ Set.range (algebraMap L E))
    (τ : E ≃ₐ[L] E) (α ζ : Eˣ)
    (hα : Units.map τ.toRingEquiv.toMonoidHom α = ζ * α)
    (hζroot : (ζ : E) ^ p = 1)
    (hζclass : (ζ : Eˣ ⧸ (powMonoidHom (p ^ (s + 1)) : Eˣ →* Eˣ).range) ≠ 1) :
    ∃ 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

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.