Module

AbsoluteConjugation.lean

Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteConjugation

8 declarations indexed from sourceView source ↗

Module documentation

Conjugation of absolute Galois automorphisms by a field automorphism

A chosen extension of a field automorphism to its algebraic closure conjugates base-linear automorphisms to base-linear automorphisms. Root quotients transform by the same extension; this is the concrete identity underlying Kummer naturality.

Imports4

Mathlib.FieldTheory.AbsoluteGaloisGroup
Nyll.GaloisCohomology.Kummer.Concrete.RootCharacters
Nyll.GaloisCohomology.Kummer.Concrete.SemilinearConjugation
Nyll.GaloisCohomology.Kummer.Concrete.SemilinearConjugationTopology

Imported by15

def

absoluteGaloisConjugate

L25 ↗

KummerTheory.absoluteGaloisConjugate

Documentation

Conjugate an absolute Galois automorphism by the chosen extension of τ.

Source context 2 commands

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

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

Lean source · statement

def absoluteGaloisConjugate (τ : K ≃+* K)
    (σ : Gal(AlgebraicClosure K/K)) : Gal(AlgebraicClosure K/K)

def

absoluteGaloisConjugateEquiv

L32 ↗

KummerTheory.absoluteGaloisConjugateEquiv

Documentation

The chosen conjugation is an automorphism of the absolute Galois group.

Source context 2 commands

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

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

Lean source · statement

def absoluteGaloisConjugateEquiv (τ : K ≃+* K) :
    Gal(AlgebraicClosure K/K) ≃* Gal(AlgebraicClosure K/K)

theorem

absoluteGaloisConjugateEquiv_apply

L39 ↗

KummerTheory.absoluteGaloisConjugateEquiv_apply

Documentation

Evaluation of the bundled chosen conjugation.

Source context 2 commands

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

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

Lean source · statement

theorem absoluteGaloisConjugateEquiv_apply (τ : K ≃+* K)
    (σ : Gal(AlgebraicClosure K/K)) :
    absoluteGaloisConjugateEquiv τ σ = absoluteGaloisConjugate τ σ

theorem

absoluteGaloisConjugateEquiv_continuous

L45 ↗

KummerTheory.absoluteGaloisConjugateEquiv_continuous

Documentation

The chosen conjugation is continuous in the Krull topology.

Source context 2 commands

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

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

Lean source · statement

theorem absoluteGaloisConjugateEquiv_continuous (τ : K ≃+* K) :
    Continuous (absoluteGaloisConjugateEquiv τ)

def

absoluteGaloisConjugateContinuousEquiv

L52 ↗

KummerTheory.absoluteGaloisConjugateContinuousEquiv

Documentation

The absolute Galois conjugation, with continuity in both directions.

Source context 2 commands

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

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

Lean source · statement

def absoluteGaloisConjugateContinuousEquiv (τ : K ≃+* K) :
    Gal(AlgebraicClosure K/K) ≃ₜ* Gal(AlgebraicClosure K/K)

theorem

absoluteGaloisConjugateContinuousEquiv_apply

L59 ↗

KummerTheory.absoluteGaloisConjugateContinuousEquiv_apply

Documentation

Evaluation of the continuous chosen conjugation.

Source context 2 commands

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

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

Lean source · statement

theorem absoluteGaloisConjugateContinuousEquiv_apply (τ : K ≃+* K)
    (σ : Gal(AlgebraicClosure K/K)) :
    absoluteGaloisConjugateContinuousEquiv τ σ = absoluteGaloisConjugate τ σ

theorem

absoluteGaloisConjugate_apply

L65 ↗

KummerTheory.absoluteGaloisConjugate_apply

Documentation

The conjugated automorphism is evaluated by conjugating in the closure.

Source context 2 commands

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

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

Lean source · statement

theorem absoluteGaloisConjugate_apply (τ : K ≃+* K)
    (σ : Gal(AlgebraicClosure K/K)) (x : AlgebraicClosure K) :
    absoluteGaloisConjugate τ σ x =
      IsAlgClosure.equivOfEquiv (AlgebraicClosure K) (AlgebraicClosure K) τ
        (σ ((IsAlgClosure.equivOfEquiv (AlgebraicClosure K) (AlgebraicClosure K) τ).symm x))

theorem

rootQuotient_absoluteGaloisConjugate

L73 ↗

KummerTheory.rootQuotient_absoluteGaloisConjugate

Documentation

Root quotients commute with semilinear conjugation in the algebraic closure.

Source context 2 commands

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

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

Lean source · statement

theorem rootQuotient_absoluteGaloisConjugate (τ : K ≃+* K)
    (β : (AlgebraicClosure K)ˣ) (σ : Gal(AlgebraicClosure K/K)) :
    rootQuotient (K := K)
      (Units.map (IsAlgClosure.equivOfEquiv (AlgebraicClosure K)
        (AlgebraicClosure K) τ).toMonoidHom β) (absoluteGaloisConjugate τ σ) =
      Units.map (IsAlgClosure.equivOfEquiv (AlgebraicClosure K)
        (AlgebraicClosure K) τ).toMonoidHom (rootQuotient (K := K) β σ)

Module documentation

Conjugation of absolute Galois automorphisms by a field automorphism

Declarations