NYLL
Module

AbsoluteResidualAbelianizationAction.lean

Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteResidualAbelianizationAction
7 declarations indexed from sourceView source ↗

Module documentation

The absolute action on an abelianized residual quotient

Base automorphisms act on the actual residual quotient of the absolute Galois group. After topological abelianization the action is independent of the selected semilinear lift, and composition agrees with composition on the base field. No restriction on the characteristic is needed: compactness of the absolute Galois group is supplied by its actual comparison with the separable-closure Galois group.

Imports12
Imported by3

Declarations

def

residualAbelianizationEquiv

L44 ↗
KummerTheory.residualAbelianizationEquiv
Source context 7 commands

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

namespace KummerTheory
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u
variable {K : Type u} [Field K]
  {C : FiniteGroupClass.{u}} (hC : FiniteGroupClass.Hereditary C)
local notation "G" => Gal(AlgebraicClosure K/K)
local notation "R" => proCResidualCore C G
local notation "Q" => G ⧸ R
Lean source · statement
def residualAbelianizationEquiv (τ : RingAut K) :
    TopologicalAbelianization Q ≃ₜ* TopologicalAbelianization Q
theorem

residualAbelianizationEquiv_apply_mk

L51 ↗
KummerTheory.residualAbelianizationEquiv_apply_mk
Source context 7 commands

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

namespace KummerTheory
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u
variable {K : Type u} [Field K]
  {C : FiniteGroupClass.{u}} (hC : FiniteGroupClass.Hereditary C)
local notation "G" => Gal(AlgebraicClosure K/K)
local notation "R" => proCResidualCore C G
local notation "Q" => G ⧸ R
Lean source · statement
theorem residualAbelianizationEquiv_apply_mk
    (τ : RingAut K) (σ : G) :
    residualAbelianizationEquiv hC τ
        (TopologicalAbelianization.mk Q (QuotientGroup.mk' R σ)) =
      TopologicalAbelianization.mk Q
        (QuotientGroup.mk' R (absoluteGaloisConjugate τ σ))
theorem

residualAbelianizationEquiv_one

L61 ↗
KummerTheory.residualAbelianizationEquiv_one
Source context 7 commands

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

namespace KummerTheory
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u
variable {K : Type u} [Field K]
  {C : FiniteGroupClass.{u}} (hC : FiniteGroupClass.Hereditary C)
local notation "G" => Gal(AlgebraicClosure K/K)
local notation "R" => proCResidualCore C G
local notation "Q" => G ⧸ R
Lean source · statement
theorem residualAbelianizationEquiv_one :
    (residualAbelianizationEquiv hC (1 : RingAut K)).toMulEquiv = 1
theorem

residualAbelianizationEquiv_mul

L84 ↗
KummerTheory.residualAbelianizationEquiv_mul
Source context 7 commands

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

namespace KummerTheory
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u
variable {K : Type u} [Field K]
  {C : FiniteGroupClass.{u}} (hC : FiniteGroupClass.Hereditary C)
local notation "G" => Gal(AlgebraicClosure K/K)
local notation "R" => proCResidualCore C G
local notation "Q" => G ⧸ R
Lean source · statement
theorem residualAbelianizationEquiv_mul (τ υ : RingAut K) :
    (residualAbelianizationEquiv hC (τ * υ)).toMulEquiv =
      (residualAbelianizationEquiv hC τ).toMulEquiv *
        (residualAbelianizationEquiv hC υ).toMulEquiv
def

absoluteGaloisResidualAbelianizationAction

L120 ↗
KummerTheory.absoluteGaloisResidualAbelianizationAction
Documentation

Base automorphisms act on the abelianization of the actual residual quotient of the absolute Galois group.

Source context 7 commands

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

namespace KummerTheory
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u
variable {K : Type u} [Field K]
  {C : FiniteGroupClass.{u}} (hC : FiniteGroupClass.Hereditary C)
local notation "G" => Gal(AlgebraicClosure K/K)
local notation "R" => proCResidualCore C G
local notation "Q" => G ⧸ R
Lean source · full declaration
def absoluteGaloisResidualAbelianizationAction :
    RingAut K →* MulAut (TopologicalAbelianization Q) where
  toFun τ := (residualAbelianizationEquiv hC τ).toMulEquiv
  map_one' := residualAbelianizationEquiv_one hC
  map_mul' := residualAbelianizationEquiv_mul hC
theorem

absoluteGaloisResidualAbelianizationAction_apply_mk

L128 ↗
KummerTheory.absoluteGaloisResidualAbelianizationAction_apply_mk
Documentation

On representatives the residual action is the actual absolute Galois conjugation, followed by the two quotient maps.

Source context 7 commands

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

namespace KummerTheory
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u
variable {K : Type u} [Field K]
  {C : FiniteGroupClass.{u}} (hC : FiniteGroupClass.Hereditary C)
local notation "G" => Gal(AlgebraicClosure K/K)
local notation "R" => proCResidualCore C G
local notation "Q" => G ⧸ R
Lean source · statement
theorem absoluteGaloisResidualAbelianizationAction_apply_mk
    (τ : RingAut K) (σ : G) :
    absoluteGaloisResidualAbelianizationAction hC τ
        (TopologicalAbelianization.mk Q (QuotientGroup.mk' R σ)) =
      TopologicalAbelianization.mk Q
        (QuotientGroup.mk' R (absoluteGaloisConjugate τ σ))
theorem

absoluteGaloisResidualAbelianizationAction_apply_mk_of_lift

L138 ↗
KummerTheory.absoluteGaloisResidualAbelianizationAction_apply_mk_of_lift
Documentation

The representative formula holds for any actual semilinear lift of the same field automorphism.

Source context 7 commands

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

namespace KummerTheory
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u
variable {K : Type u} [Field K]
  {C : FiniteGroupClass.{u}} (hC : FiniteGroupClass.Hereditary C)
local notation "G" => Gal(AlgebraicClosure K/K)
local notation "R" => proCResidualCore C G
local notation "Q" => G ⧸ R
Lean source · statement
theorem absoluteGaloisResidualAbelianizationAction_apply_mk_of_lift
    (τ : RingAut K) (e : AlgebraicClosure K ≃+* AlgebraicClosure K)
    (he : ∀ k : K, e (algebraMap K (AlgebraicClosure K) k) =
      algebraMap K (AlgebraicClosure K) (τ k))
    (σ : G) :
    absoluteGaloisResidualAbelianizationAction hC τ
        (TopologicalAbelianization.mk Q (QuotientGroup.mk' R σ)) =
      TopologicalAbelianization.mk Q
        (QuotientGroup.mk' R (semilinearGaloisConjugate τ e he σ))

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