Yamaguchi26AbfaithfulGalois.relativeGaloisAbelianModPowerTransform_naturality
Intertwined relative field automorphisms induce intertwined maps on the absolute Galois abelianizations modulo any power.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups.Abelian
open Field.absoluteGaloisGroup
universe u
variable {K L F E : Type u} [Field K] [Field L] [Field F] [Field E]
[Algebra K L] [Algebra F E]Lean source · statement
theorem relativeGaloisAbelianModPowerTransform_naturality
(q : ℕ) (f : L →+* E) (τ : Gal(L/K)) (σ : Gal(E/F))
(hcompat : ∀ x : L, σ (f x) = f (τ x))
(z : abelianModPower Gal(AlgebraicClosure E/E) q) :
abelianModPowerMap q (map f)
(relativeGaloisAbelianModPowerTransform F E q σ z) =
relativeGaloisAbelianModPowerTransform K L q τ
(abelianModPowerMap q (map f) z)