Module

AbsoluteRestrictionConjugation.lean

Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteRestrictionConjugation

1 declaration indexed from sourceView source ↗

Module documentation

Comparing restriction and semilinear absolute Galois conjugation

Restriction along the inverse field automorphism and conjugation by a chosen extension of the field automorphism agree on all commutative characters.

Imports2

Imported by5

theorem

character_map_symm_eq_absoluteGaloisConjugate

L23 ↗

KummerTheory.character_map_symm_eq_absoluteGaloisConjugate

Documentation

Character pullback along the inverse field automorphism is the existing semilinear conjugation action, independently of closure-lift choices.

Source context 2 commands

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

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

Lean source · statement

theorem character_map_symm_eq_absoluteGaloisConjugate
    (τ : K ≃+* K) (χ : Gal(AlgebraicClosure K/K) →ₜ* A)
    (σ : Gal(AlgebraicClosure K/K)) :
    χ (Field.absoluteGaloisGroup.map τ.symm.toRingHom σ) =
      χ (absoluteGaloisConjugate τ σ)

Module documentation

Comparing restriction and semilinear absolute Galois conjugation

Declarations

character_map_symm_eq_absoluteGaloisConjugate