Module

RelativeAbelianModPowerAction.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.RelativeAbelianModPowerAction

4 declarations indexed from sourceView source ↗

Module documentation

Relative Galois conjugation on the abelianization modulo powers

The conjugation map on the absolute Galois group is a continuous automorphism. Passing to its topological abelianization and then modulo q-th powers gives the actual map used in Section 3.

Imports4

Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteConjugation
Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteH1Action
Nyll.ProCGroups.Abelian.AbelianModPower
Mathlib.Topology.Instances.ZMod

Imported by13

theorem

exists_changed_character_of_inverse_relativeH1Action_ne_one

L26 ↗

ClassFieldTower.Martinet.Shafarevich.exists_changed_character_of_inverse_relativeH1Action_ne_one

Documentation

A nontrivial inverse pullback action on degree-one classes gives a character moved by forward conjugation.

Source context 2 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ClassFieldTower.ProP

Lean source · statement

theorem exists_changed_character_of_inverse_relativeH1Action_ne_one
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (q : ℕ) (τ : Gal(L/K))
    (hτ : relativeGaloisH1Action (n := q) K L τ⁻¹ ≠ 1) :
    ∃ χ : Gal(AlgebraicClosure L/L) →ₜ* Multiplicative (ZMod q),
      ∃ σ : Gal(AlgebraicClosure L/L),
        χ (absoluteGaloisConjugate τ.toRingEquiv σ) ≠ χ σ

def

relativeGaloisAbelianModPowerTransform

L69 ↗

Yamaguchi26AbfaithfulGalois.relativeGaloisAbelianModPowerTransform

Documentation

The map on G_Lᵃᵇ/q induced by a relative Galois automorphism. It is constructed from the chosen continuous conjugation of G_L; the choice disappears on abelianization.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups.Abelian
universe u

Lean source · statement

def relativeGaloisAbelianModPowerTransform
    (K L : Type u) [Field K] [Field L] [Algebra K L]
    (q : ℕ) (τ : Gal(L/K)) :
    abelianModPower Gal(AlgebraicClosure L/L) q →*
      abelianModPower Gal(AlgebraicClosure L/L) q

theorem

relativeGaloisAbelianModPowerTransform_apply_mk

L79 ↗

Yamaguchi26AbfaithfulGalois.relativeGaloisAbelianModPowerTransform_apply_mk

Documentation

Conjugation on G_Lᵃᵇ/q evaluates on the canonical quotient image.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups.Abelian
universe u

Lean source · statement

theorem relativeGaloisAbelianModPowerTransform_apply_mk
    (K L : Type u) [Field K] [Field L] [Algebra K L]
    (q : ℕ) (τ : Gal(L/K)) (σ : Gal(AlgebraicClosure L/L)) :
    relativeGaloisAbelianModPowerTransform K L q τ
        ((TopologicalAbelianization.mk Gal(AlgebraicClosure L/L) σ :
          TopologicalAbelianization Gal(AlgebraicClosure L/L)) :
          abelianModPower Gal(AlgebraicClosure L/L) q) =
      ((TopologicalAbelianization.mk Gal(AlgebraicClosure L/L)
          (absoluteGaloisConjugate τ.toRingEquiv σ) :
        TopologicalAbelianization Gal(AlgebraicClosure L/L)) :
        abelianModPower Gal(AlgebraicClosure L/L) q)

theorem

exists_moved_abelianModPower_of_inverse_relativeH1Action_ne_one

L94 ↗

Yamaguchi26AbfaithfulGalois.exists_moved_abelianModPower_of_inverse_relativeH1Action_ne_one

Documentation

A nontrivial inverse action on continuous H¹ moves an element of the actual quotient G_Lᵃᵇ/q under forward relative Galois conjugation.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups.Abelian
universe u

Lean source · statement

theorem exists_moved_abelianModPower_of_inverse_relativeH1Action_ne_one
    (K L : Type u) [Field K] [Field L] [Algebra K L]
    (q : ℕ) (τ : Gal(L/K))
    (hτ : relativeGaloisH1Action (n := q) K L τ⁻¹ ≠ 1) :
    ∃ z : abelianModPower Gal(AlgebraicClosure L/L) q,
      relativeGaloisAbelianModPowerTransform K L q τ z ≠ z

Module documentation

Relative Galois conjugation on the abelianization modulo powers

Declarations

exists_changed_character_of_inverse_relativeH1Action_ne_one

relativeGaloisAbelianModPowerTransform

relativeGaloisAbelianModPowerTransform_apply_mk

exists_moved_abelianModPower_of_inverse_relativeH1Action_ne_one