An actual base-linear equivalence transports a semilinear automorphism and intertwines its conjugation on the two relative Galois groups.
Transport a field automorphism along a base-linear field equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
variable {K Ω Ω' : Type*} [Field K] [Field Ω] [Field Ω']
[Algebra K Ω] [Algebra K Ω']def transportSemilinearEquiv (e : Ω ≃ₐ[K] Ω') (a : Ω ≃+* Ω) : Ω' ≃+* Ω'Evaluation of the transported field automorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
variable {K Ω Ω' : Type*} [Field K] [Field Ω] [Field Ω']
[Algebra K Ω] [Algebra K Ω']theorem transportSemilinearEquiv_apply (e : Ω ≃ₐ[K] Ω') (a : Ω ≃+* Ω) (x : Ω') :
transportSemilinearEquiv e a x = e (a (e.symm x))Evaluation of its inverse.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
variable {K Ω Ω' : Type*} [Field K] [Field Ω] [Field Ω']
[Algebra K Ω] [Algebra K Ω']theorem transportSemilinearEquiv_symm_apply (e : Ω ≃ₐ[K] Ω') (a : Ω ≃+* Ω)
(x : Ω') :
(transportSemilinearEquiv e a).symm x = e (a.symm (e.symm x))Transport preserves the base automorphism of a semilinear map.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
variable {K Ω Ω' : Type*} [Field K] [Field Ω] [Field Ω']
[Algebra K Ω] [Algebra K Ω']theorem transportSemilinearEquiv_algebraMap (τ : K ≃+* K)
(e : Ω ≃ₐ[K] Ω') (a : Ω ≃+* Ω)
(ha : ∀ k : K, a (algebraMap K Ω k) = algebraMap K Ω (τ k)) (k : K) :
transportSemilinearEquiv e a (algebraMap K Ω' k) = algebraMap K Ω' (τ k)The Galois-group transport intertwines the two concrete semilinear conjugations, before passing to any quotient or character.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
variable {K Ω Ω' : Type*} [Field K] [Field Ω] [Field Ω']
[Algebra K Ω] [Algebra K Ω']theorem autCongr_semilinearGaloisConjugate (τ : K ≃+* K)
(e : Ω ≃ₐ[K] Ω') (a : Ω ≃+* Ω)
(ha : ∀ k : K, a (algebraMap K Ω k) = algebraMap K Ω (τ k))
(σ : Gal(Ω/K)) :
AlgEquiv.autCongr e (semilinearGaloisConjugate τ a ha σ) =
semilinearGaloisConjugate τ (transportSemilinearEquiv e a)
(transportSemilinearEquiv_algebraMap τ e a ha) (AlgEquiv.autCongr e σ)