Module

NormalRestrictionResidualAction.lean

Nyll.GaloisCohomology.Kummer.Concrete.NormalRestrictionResidualAction

3 declarations indexed from sourceView source ↗

Module documentation

The restriction kernel and the absolute residual action

The actual kernel of normal restriction identifies with the upper field's absolute Galois group. Transport through both actual quotient maps preserves conjugation by the same lift of the relative automorphism.

Imports8

Nyll.GaloisCohomology.Kummer.Concrete.NormalRestrictionKernel
Nyll.GaloisCohomology.Kummer.Concrete.NormalRestrictionKernelFinite
Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteResidualAbelianizationAction
Nyll.ProCGroups.ProC.MaximalQuotients.ResidualEquivalence
Nyll.ProCGroups.ProC.MaximalQuotients.ConjugationComparison
Nyll.ProCGroups.Abelian.TopologicalAbelianization
Mathlib.Algebra.CharP.Algebra
Mathlib.Topology.Algebra.OpenSubgroup

Imported by2

def

normalRestrictionResidualAbelianizationEquiv

L40 ↗

KummerTheory.normalRestrictionResidualAbelianizationEquiv

Documentation

The actual restriction kernel's abelianized residual quotient is the upper field's abelianized absolute residual quotient.

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 M : Type u} [Field K] [Field M] [Algebra K M]
  [FiniteDimensional K M] [Normal K M] [CharZero K]
  {C : FiniteGroupClass.{u}}
local notation "AC" => AlgebraicClosure M
local notation "N" => MonoidHom.ker (AlgEquiv.restrictNormalHom M : Gal(AC/K) →* Gal(M/K))
local notation "G" => Gal(AC/M)

Lean source · statement

def normalRestrictionResidualAbelianizationEquiv
    (hC : FiniteGroupClass.Hereditary C) :
    TopologicalAbelianization (N ⧸ proCResidualCore C N) ≃ₜ*
      TopologicalAbelianization (G ⧸ proCResidualCore C G)

theorem

normalRestrictionResidualAbelianizationEquiv_apply_mk

L53 ↗

KummerTheory.normalRestrictionResidualAbelianizationEquiv_apply_mk

Documentation

The restriction-kernel comparison evaluates through the actual 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 M : Type u} [Field K] [Field M] [Algebra K M]
  [FiniteDimensional K M] [Normal K M] [CharZero K]
  {C : FiniteGroupClass.{u}}
local notation "AC" => AlgebraicClosure M
local notation "N" => MonoidHom.ker (AlgEquiv.restrictNormalHom M : Gal(AC/K) →* Gal(M/K))
local notation "G" => Gal(AC/M)

Lean source · statement

theorem normalRestrictionResidualAbelianizationEquiv_apply_mk
    (hC : FiniteGroupClass.Hereditary C) (x : N) :
    normalRestrictionResidualAbelianizationEquiv (K := K) (M := M) hC
        (TopologicalAbelianization.mk (N ⧸ proCResidualCore C N)
          (QuotientGroup.mk' (proCResidualCore C N) x)) =
      TopologicalAbelianization.mk (G ⧸ proCResidualCore C G)
        (QuotientGroup.mk' (proCResidualCore C G)
          (normalRestrictionKernelContinuousEquiv (K := K) M AC x))

theorem

normalRestrictionResidualAbelianizationEquiv_conjugation

L65 ↗

KummerTheory.normalRestrictionResidualAbelianizationEquiv_conjugation

Documentation

Conjugation on the restriction kernel transports to the canonical absolute residual action of the actual restricted 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 M : Type u} [Field K] [Field M] [Algebra K M]
  [FiniteDimensional K M] [Normal K M] [CharZero K]
  {C : FiniteGroupClass.{u}}
local notation "AC" => AlgebraicClosure M
local notation "N" => MonoidHom.ker (AlgEquiv.restrictNormalHom M : Gal(AC/K) →* Gal(M/K))
local notation "G" => Gal(AC/M)

Lean source · statement

theorem normalRestrictionResidualAbelianizationEquiv_conjugation
    (hC : FiniteGroupClass.FullFormation C) (g : Gal(AC/K))
    (a : TopologicalAbelianization (N ⧸ proCResidualCore C N)) :
    normalRestrictionResidualAbelianizationEquiv (K := K) (M := M) hC.hereditary
        (TopologicalAbelianization.congr
          (residualQuotientConjugationContinuousMulEquiv hC N
            ((N).isClosed_of_isOpen
              (normalRestrictionKernel_isOpen (K := K) (M := M) (Ω := AC))) g) a) =
      absoluteGaloisResidualAbelianizationAction hC.hereditary
        (g.restrictNormal M).toRingEquiv
        (normalRestrictionResidualAbelianizationEquiv (K := K) (M := M) hC.hereditary a)

Module documentation

The restriction kernel and the absolute residual action

Declarations

normalRestrictionResidualAbelianizationEquiv

normalRestrictionResidualAbelianizationEquiv_apply_mk

normalRestrictionResidualAbelianizationEquiv_conjugation