KummerTheory.absoluteGaloisClosureEquiv_character_conjugation
A continuous abelian character evaluates concrete semilinear conjugation through the closure comparison as the canonical absolute conjugation.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω A : Type*} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω]
[CommGroup A] [TopologicalSpace A] [T1Space A]Lean source · statement
theorem absoluteGaloisClosureEquiv_character_conjugation
(τ : K ≃+* K) (a : Ω ≃+* Ω)
(ha : ∀ k : K, a (algebraMap K Ω k) = algebraMap K Ω (τ k))
(f : Gal(AlgebraicClosure K/K) →ₜ* A) (σ : Gal(Ω/K)) :
f (absoluteGaloisClosureEquiv K Ω (semilinearGaloisConjugate τ a ha σ)) =
f (absoluteGaloisConjugate τ (absoluteGaloisClosureEquiv K Ω σ))