Module

AbsoluteCharacterAction.lean

Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteCharacterAction

8 declarations indexed from sourceView source ↗

Module documentation

The canonical action on abelian absolute Galois characters

Precomposition with inverse conjugation gives a left action. Its group law uses independence from the chosen extensions to the algebraic closure.

Imports4

Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteConjugation
Nyll.GaloisCohomology.Kummer.Concrete.SemilinearConjugation
Mathlib.Algebra.Ring.Aut
Mathlib.Algebra.Group.Hom.Instances

Imported by2

def

absoluteGaloisCharacterTransform

L24 ↗

KummerTheory.absoluteGaloisCharacterTransform

Documentation

Pull a character back along the conjugation attached to the inverse base map.

Source context 2 commands

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

namespace KummerTheory
variable {K A : Type*} [Field K] [CommGroup A]

Lean source · statement

def absoluteGaloisCharacterTransform (τ : RingAut K)
    (f : Gal(AlgebraicClosure K/K) →* A) : Gal(AlgebraicClosure K/K) →* A

theorem

absoluteGaloisCharacterTransform_apply

L29 ↗

KummerTheory.absoluteGaloisCharacterTransform_apply

Documentation

Evaluation of the character transform.

Source context 2 commands

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

namespace KummerTheory
variable {K A : Type*} [Field K] [CommGroup A]

Lean source · statement

theorem absoluteGaloisCharacterTransform_apply (τ : RingAut K)
    (f : Gal(AlgebraicClosure K/K) →* A) (σ : Gal(AlgebraicClosure K/K)) :
    absoluteGaloisCharacterTransform τ f σ =
      f (absoluteGaloisConjugate τ.symm σ)

theorem

absoluteGaloisCharacterTransform_one

L36 ↗

KummerTheory.absoluteGaloisCharacterTransform_one

Documentation

The transform by the identity is independent of its possibly nonidentity lift.

Source context 2 commands

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

namespace KummerTheory
variable {K A : Type*} [Field K] [CommGroup A]

Lean source · statement

theorem absoluteGaloisCharacterTransform_one (f : Gal(AlgebraicClosure K/K) →* A) :
    absoluteGaloisCharacterTransform 1 f = f

theorem

absoluteGaloisCharacterTransform_mul

L50 ↗

KummerTheory.absoluteGaloisCharacterTransform_mul

Documentation

The transforms compose in the order required for a left action.

Source context 2 commands

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

namespace KummerTheory
variable {K A : Type*} [Field K] [CommGroup A]

Lean source · statement

theorem absoluteGaloisCharacterTransform_mul (τ υ : RingAut K)
    (f : Gal(AlgebraicClosure K/K) →* A) :
    absoluteGaloisCharacterTransform (τ * υ) f =
      absoluteGaloisCharacterTransform τ (absoluteGaloisCharacterTransform υ f)

def

absoluteGaloisCharacterTransformEquiv

L75 ↗

KummerTheory.absoluteGaloisCharacterTransformEquiv

Documentation

Each base automorphism acts by an automorphism of the abelian character group.

Source context 2 commands

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

namespace KummerTheory
variable {K A : Type*} [Field K] [CommGroup A]

Lean source · full declaration

def absoluteGaloisCharacterTransformEquiv (τ : RingAut K) :
    MulAut (Gal(AlgebraicClosure K/K) →* A) where
  toFun := absoluteGaloisCharacterTransform τ
  invFun := absoluteGaloisCharacterTransform τ⁻¹
  left_inv f := by
    rw [← absoluteGaloisCharacterTransform_mul, inv_mul_cancel,
      absoluteGaloisCharacterTransform_one]
  right_inv f := by
    rw [← absoluteGaloisCharacterTransform_mul, mul_inv_cancel,
      absoluteGaloisCharacterTransform_one]
  map_mul' f g := by
    apply MonoidHom.ext
    intro σ
    simp only [absoluteGaloisCharacterTransform_apply, MonoidHom.mul_apply]

theorem

absoluteGaloisCharacterTransformEquiv_apply

L91 ↗

KummerTheory.absoluteGaloisCharacterTransformEquiv_apply

Documentation

Evaluation of the automorphism of the abelian character group.

Source context 2 commands

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

namespace KummerTheory
variable {K A : Type*} [Field K] [CommGroup A]

Lean source · statement

theorem absoluteGaloisCharacterTransformEquiv_apply (τ : RingAut K)
    (f : Gal(AlgebraicClosure K/K) →* A) :
    absoluteGaloisCharacterTransformEquiv τ f = absoluteGaloisCharacterTransform τ f

def

absoluteGaloisCharacterAction

L97 ↗

KummerTheory.absoluteGaloisCharacterAction

Documentation

The canonical action of base-field automorphisms on abelian Galois characters.

Source context 2 commands

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

namespace KummerTheory
variable {K A : Type*} [Field K] [CommGroup A]

Lean source · full declaration

def absoluteGaloisCharacterAction :
    RingAut K →* MulAut (Gal(AlgebraicClosure K/K) →* A) where
  toFun := absoluteGaloisCharacterTransformEquiv
  map_one' := by
    apply MulEquiv.ext
    intro f
    rw [absoluteGaloisCharacterTransformEquiv_apply, MulAut.one_apply,
      absoluteGaloisCharacterTransform_one]
  map_mul' τ υ := by
    apply MulEquiv.ext
    intro f
    rw [MulAut.mul_apply, absoluteGaloisCharacterTransformEquiv_apply,
      absoluteGaloisCharacterTransformEquiv_apply, absoluteGaloisCharacterTransformEquiv_apply,
      absoluteGaloisCharacterTransform_mul]

theorem

absoluteGaloisCharacterAction_apply

L113 ↗

KummerTheory.absoluteGaloisCharacterAction_apply

Documentation

Evaluation of the canonical action.

Source context 2 commands

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

namespace KummerTheory
variable {K A : Type*} [Field K] [CommGroup A]

Lean source · statement

theorem absoluteGaloisCharacterAction_apply (τ : RingAut K)
    (f : Gal(AlgebraicClosure K/K) →* A) :
    absoluteGaloisCharacterAction τ f = absoluteGaloisCharacterTransform τ f

Module documentation

The canonical action on abelian absolute Galois characters

Declarations