Field.absoluteGaloisGroup.character_map_apply_of_lift
Any compatible closure embedding computes the same commutative character restriction as the chosen absolute Galois map.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Field.absoluteGaloisGroup
variable {K L : Type*} [Field K] [Field L]Lean source · statement
theorem character_map_apply_of_lift
{A : Type*} [CommGroup A] [TopologicalSpace A]
(f : K →+* L) (j : AlgebraicClosure K →+* AlgebraicClosure L)
(hj : ∀ x : K, j (algebraMap K (AlgebraicClosure K) x) =
algebraMap L (AlgebraicClosure L) (f x))
(σ : Gal(AlgebraicClosure L/L)) (θ : Gal(AlgebraicClosure K/K))
(hθ : ∀ x, j (θ x) = σ (j x))
(χ : Gal(AlgebraicClosure K/K) →ₜ* A) :
χ (map f σ) = χ θ