Module

AbsoluteKummerCharacterAction.lean

Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteKummerCharacterAction

3 declarations indexed from sourceView source ↗

Module documentation

Exact Kummer differences under the character action

When a field automorphism fixes the roots of unity, inverse-conjugation pullback sends a Kummer character to the character of the transformed unit. The fixed coordinate identification with cyclic coefficients preserves this formula and the nontrivial difference supplied by an eigenunit.

Imports7

Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteKummerNaturality
Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteKummerH1
Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteContinuousCharacterAction
Mathlib.Algebra.Group.Units.Hom
Mathlib.GroupTheory.QuotientGroup.Defs
Mathlib.Topology.Algebra.Group.Basic
Mathlib.Topology.Instances.ZMod

Imported by2

theorem

absoluteKummerContinuousNthRootsCharacterEquiv_action_of_fixes_roots

L32 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteKummerContinuousNthRootsCharacterEquiv_action_of_fixes_roots

Documentation

The actual left character action agrees with the action on Kummer classes when the coefficient roots are fixed.

Source context 3 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [CharZero K]

Lean source · statement

theorem absoluteKummerContinuousNthRootsCharacterEquiv_action_of_fixes_roots
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (τ : K ≃+* K) (hτ : ∀ ξ : K, ξ ^ (n : ℕ) = 1 → τ ξ = ξ) (u : Kˣ) :
    absoluteContinuousCharacterAction
        (K := K) (A := DiscreteNthRootsSubgroup (AlgebraicClosure K) (n : ℕ)) τ
        (absoluteKummerContinuousNthRootsCharacterEquiv K n hmu
          (u : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)) =
      absoluteKummerContinuousNthRootsCharacterEquiv K n hmu
        ((Units.map τ.toMonoidHom u : Kˣ) :
          Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)

theorem

absoluteKummerContinuousZModCharacterEquiv_action_of_fixes_roots

L64 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteKummerContinuousZModCharacterEquiv_action_of_fixes_roots

Documentation

The same fixed cyclic-coordinate identification preserves the exact Kummer action formula.

Source context 3 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [CharZero K]

Lean source · statement

theorem absoluteKummerContinuousZModCharacterEquiv_action_of_fixes_roots
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (τ : K ≃+* K) (hτ : ∀ ξ : K, ξ ^ (n : ℕ) = 1 → τ ξ = ξ) (u : Kˣ) :
    absoluteContinuousCharacterAction (K := K) (A := Multiplicative (ZMod (n : ℕ))) τ
        (absoluteKummerContinuousZModCharacterEquiv K n hmu
          (u : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) :
          Gal(AlgebraicClosure K/K) →ₜ* Multiplicative (ZMod (n : ℕ))) =
      absoluteKummerContinuousZModCharacterEquiv K n hmu
        ((Units.map τ.toMonoidHom u : Kˣ) :
          Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)

theorem

absoluteKummerContinuousZModCharacterEquiv_action_div_ne_one_of_eigenunit

L98 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteKummerContinuousZModCharacterEquiv_action_div_ne_one_of_eigenunit

Documentation

An eigenunit retains its exact nontrivial Kummer-character difference, in the cyclic coordinates used by continuous H¹.

Source context 3 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [CharZero K]

Lean source · full declaration

theorem absoluteKummerContinuousZModCharacterEquiv_action_div_ne_one_of_eigenunit
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (τ : K ≃+* K) (hτ : ∀ ξ : K, ξ ^ (n : ℕ) = 1 → τ ξ = ξ)
    (α ζ : Kˣ) (hα : Units.map τ.toMonoidHom α = ζ * α)
    (hζ : (ζ : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) ≠ 1) :
    let κ : (Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) ≃*
        (Gal(AlgebraicClosure K/K) →ₜ* Multiplicative (ZMod (n : ℕ))) :=
      absoluteKummerContinuousZModCharacterEquiv K n hmu
    absoluteContinuousCharacterAction (K := K) (A := Multiplicative (ZMod (n : ℕ))) τ
        (κ (α : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)) /
      κ (α : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) =
        κ (ζ : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) ∧
      κ (ζ : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) ≠ 1 := by
  intro κ
  have haction :
      absoluteContinuousCharacterAction (K := K) (A := Multiplicative (ZMod (n : ℕ))) τ
          (κ (α : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)) =
        κ ((Units.map τ.toMonoidHom α : Kˣ) :
          Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) :=
    absoluteKummerContinuousZModCharacterEquiv_action_of_fixes_roots K n hmu τ hτ α
  constructor
  · rw [haction, hα, QuotientGroup.mk_mul, κ.map_mul, mul_div_cancel_right]
  · intro h
    apply hζ
    apply κ.injective
    simpa only [_root_.map_one] using h

Module documentation

Exact Kummer differences under the character action

Declarations

absoluteKummerContinuousNthRootsCharacterEquiv_action_of_fixes_roots

absoluteKummerContinuousZModCharacterEquiv_action_of_fixes_roots

absoluteKummerContinuousZModCharacterEquiv_action_div_ne_one_of_eigenunit