Module

AbsoluteAbelianizationAction.lean

Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteAbelianizationAction

10 declarations indexed from sourceView source ↗

Module documentation

The canonical action on the abelianized absolute Galois group

Semilinear conjugation descends through the closed commutator subgroup. The result is independent of the chosen lift to the algebraic closure and gives a covariant action of base-field automorphisms. A changed continuous abelian character detects a nontrivial element of this action.

Imports5

Imported by11

theorem

topologicalAbelianization_congr_ne_one_of_character_ne

L33 ↗

KummerTheory.topologicalAbelianization_congr_ne_one_of_character_ne

Documentation

A continuous abelian character changed by an automorphism detects its nontrivial action on topological abelianization.

Source context 4 commands

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

namespace KummerTheory
open ProCGroups.Abelian
section GeneralDetection
variable {G A : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CommGroup A] [TopologicalSpace A] [T1Space A]

Lean source · statement

theorem topologicalAbelianization_congr_ne_one_of_character_ne
    (e : G ≃ₜ* G) (χ : G →ₜ* A) {x : G} (hχ : χ (e x) ≠ χ x) :
    (TopologicalAbelianization.congr e).toMulEquiv ≠ 1

theorem

semilinearGaloisAbelianizationEquiv_eq

L61 ↗

KummerTheory.semilinearGaloisAbelianizationEquiv_eq

Documentation

The continuous automorphism of topological abelianization depends only on the base automorphism, not on its semilinear lift.

Source context 4 commands

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

namespace KummerTheory
open ProCGroups.Abelian
section SemilinearIndependence
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
  [Algebra.IsAlgebraic K Ω]

Lean source · statement

theorem semilinearGaloisAbelianizationEquiv_eq (τ : K ≃+* K) (e e' : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (he' : ∀ k : K, e' (algebraMap K Ω k) = algebraMap K Ω (τ k)) :
    TopologicalAbelianization.congr (semilinearGaloisConjugateContinuousEquiv τ e' he') =
      TopologicalAbelianization.congr (semilinearGaloisConjugateContinuousEquiv τ e he)

def

absoluteGaloisAbelianizationEquiv

L83 ↗

KummerTheory.absoluteGaloisAbelianizationEquiv

Documentation

A base automorphism induces a continuous automorphism of the topological abelianization of its absolute Galois group.

Source context 4 commands

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

namespace KummerTheory
open ProCGroups.Abelian
section AbsoluteAction
variable {K : Type*} [Field K]

Lean source · statement

def absoluteGaloisAbelianizationEquiv (τ : RingAut K) :
    _root_.TopologicalAbelianization Gal(AlgebraicClosure K/K) ≃ₜ*
      _root_.TopologicalAbelianization Gal(AlgebraicClosure K/K)

theorem

absoluteGaloisAbelianizationEquiv_apply_mk

L89 ↗

KummerTheory.absoluteGaloisAbelianizationEquiv_apply_mk

Documentation

The descended automorphism acts on representatives by Galois conjugation.

Source context 4 commands

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

namespace KummerTheory
open ProCGroups.Abelian
section AbsoluteAction
variable {K : Type*} [Field K]

Lean source · statement

theorem absoluteGaloisAbelianizationEquiv_apply_mk (τ : RingAut K)
    (σ : Gal(AlgebraicClosure K/K)) :
    absoluteGaloisAbelianizationEquiv τ
        (TopologicalAbelianization.mk Gal(AlgebraicClosure K/K) σ) =
      TopologicalAbelianization.mk Gal(AlgebraicClosure K/K)
        (absoluteGaloisConjugate τ σ)

theorem

absoluteGaloisAbelianizationEquiv_eq_of_lift

L99 ↗

KummerTheory.absoluteGaloisAbelianizationEquiv_eq_of_lift

Documentation

The descended automorphism agrees with the descent of any actual lift.

Source context 4 commands

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

namespace KummerTheory
open ProCGroups.Abelian
section AbsoluteAction
variable {K : Type*} [Field K]

Lean source · statement

theorem absoluteGaloisAbelianizationEquiv_eq_of_lift (τ : RingAut K)
    (e : AlgebraicClosure K ≃+* AlgebraicClosure K)
    (he : ∀ k : K, e (algebraMap K (AlgebraicClosure K) k) =
      algebraMap K (AlgebraicClosure K) (τ k)) :
    absoluteGaloisAbelianizationEquiv τ =
      TopologicalAbelianization.congr (semilinearGaloisConjugateContinuousEquiv τ e he)

theorem

absoluteGaloisAbelianizationEquiv_one

L110 ↗

KummerTheory.absoluteGaloisAbelianizationEquiv_one

Documentation

The identity base automorphism induces the identity on abelianization.

Source context 4 commands

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

namespace KummerTheory
open ProCGroups.Abelian
section AbsoluteAction
variable {K : Type*} [Field K]

Lean source · statement

theorem absoluteGaloisAbelianizationEquiv_one :
    (absoluteGaloisAbelianizationEquiv (1 : RingAut K)).toMulEquiv = 1

theorem

absoluteGaloisAbelianizationEquiv_mul

L130 ↗

KummerTheory.absoluteGaloisAbelianizationEquiv_mul

Documentation

Composition of base automorphisms acts covariantly on abelianization.

Source context 4 commands

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

namespace KummerTheory
open ProCGroups.Abelian
section AbsoluteAction
variable {K : Type*} [Field K]

Lean source · statement

theorem absoluteGaloisAbelianizationEquiv_mul (τ υ : RingAut K) :
    (absoluteGaloisAbelianizationEquiv (τ * υ)).toMulEquiv =
      (absoluteGaloisAbelianizationEquiv τ).toMulEquiv *
        (absoluteGaloisAbelianizationEquiv υ).toMulEquiv

def

absoluteGaloisAbelianizationAction

L163 ↗

KummerTheory.absoluteGaloisAbelianizationAction

Documentation

The canonical covariant action of base automorphisms on the abelianized absolute Galois group.

Source context 4 commands

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

namespace KummerTheory
open ProCGroups.Abelian
section AbsoluteAction
variable {K : Type*} [Field K]

Lean source · full declaration

def absoluteGaloisAbelianizationAction :
    RingAut K →* MulAut (_root_.TopologicalAbelianization Gal(AlgebraicClosure K/K)) where
  toFun τ := (absoluteGaloisAbelianizationEquiv τ).toMulEquiv
  map_one' := absoluteGaloisAbelianizationEquiv_one
  map_mul' := absoluteGaloisAbelianizationEquiv_mul

theorem

absoluteGaloisAbelianizationAction_apply_mk

L170 ↗

KummerTheory.absoluteGaloisAbelianizationAction_apply_mk

Documentation

Evaluation of the canonical action on quotient representatives.

Source context 4 commands

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

namespace KummerTheory
open ProCGroups.Abelian
section AbsoluteAction
variable {K : Type*} [Field K]

Lean source · statement

theorem absoluteGaloisAbelianizationAction_apply_mk (τ : RingAut K)
    (σ : Gal(AlgebraicClosure K/K)) :
    absoluteGaloisAbelianizationAction τ
        (TopologicalAbelianization.mk Gal(AlgebraicClosure K/K) σ) =
      TopologicalAbelianization.mk Gal(AlgebraicClosure K/K)
        (absoluteGaloisConjugate τ σ)

theorem

absoluteGaloisAbelianizationAction_ne_one_of_character_ne

L180 ↗

KummerTheory.absoluteGaloisAbelianizationAction_ne_one_of_character_ne

Documentation

A continuous character changed by base conjugation detects a nontrivial element of the canonical abelianization action.

Source context 4 commands

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

namespace KummerTheory
open ProCGroups.Abelian
section AbsoluteAction
variable {K : Type*} [Field K]

Lean source · statement

theorem absoluteGaloisAbelianizationAction_ne_one_of_character_ne
    {A : Type*} [CommGroup A] [TopologicalSpace A] [T1Space A]
    (τ : RingAut K) (χ : Gal(AlgebraicClosure K/K) →ₜ* A)
    {σ : Gal(AlgebraicClosure K/K)}
    (hχ : χ (absoluteGaloisConjugate τ σ) ≠ χ σ) :
    absoluteGaloisAbelianizationAction τ ≠ 1

Module documentation

The canonical action on the abelianized absolute Galois group

Declarations