The chosen algebraic-closure embeddings behind absoluteGaloisGroup.map need not compose. Their discrepancy is an inner automorphism, so restriction of a continuous homomorphism with commutative target does compose exactly.
The algebraic-closure embedding used to define the absolute Galois restriction.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Field.absoluteGaloisGroup
variable {K L M : Type*} [Field K] [Field L] [Field M]def closureLift (f : K →+* L) :
AlgebraicClosure K →+* AlgebraicClosure LThe chosen closure embedding extends the original field embedding.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Field.absoluteGaloisGroup
variable {K L M : Type*} [Field K] [Field L] [Field M]theorem closureLift_algebraMap (f : K →+* L) (x : K) :
closureLift f (algebraMap K (AlgebraicClosure K) x) =
algebraMap L (AlgebraicClosure L) (f x)Absolute Galois restriction commutes with its chosen closure embedding.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Field.absoluteGaloisGroup
variable {K L M : Type*} [Field K] [Field L] [Field M]theorem map_closureLift (f : K →+* L)
(σ : Gal(AlgebraicClosure L/L)) (x : AlgebraicClosure K) :
closureLift f ((map f σ : Gal(AlgebraicClosure K/K)).toAlgHom x) = σ (closureLift f x)Surrounding namespaces, section variables, and local commands at this declaration.
namespace Field.absoluteGaloisGroup
variable {K L M : Type*} [Field K] [Field L] [Field M]theorem exists_precomposition_aut
{Ω : Type*} [Field Ω] [Algebra K Ω]
(j₁ j₂ : AlgebraicClosure K →ₐ[K] Ω) :
∃ τ : Gal(AlgebraicClosure K/K), ∀ x, j₁ (τ x) = j₂ xRestriction to a commutative target is independent of the discrepancy between chosen closure embeddings, and hence respects composition of field embeddings.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Field.absoluteGaloisGroup
variable {K L M : Type*} [Field K] [Field L] [Field M]theorem character_map_comp
{A : Type*} [CommGroup A] [TopologicalSpace A]
(f : K →+* L) (g : L →+* M)
(χ : Gal(AlgebraicClosure K/K) →ₜ* A) :
χ.comp (map (g.comp f)) = (χ.comp (map f)).comp (map g)