An automorphism over the common base preserves an embedded separably closed separable extension. Restricting both the automorphism and its inverse gives an automorphism of that extension, compatible with the original embedding.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ValuationTheory.Completion
variable {K S E : Type*} [Field K] [Field S] [Field E]
[Algebra K S] [Algebra K E] [IsSepClosed S] [Algebra.IsSeparable K S]def restrictionHom (i : S →ₐ[K] E) (σ : E ≃ₐ[K] E) : S →ₐ[K] SSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ValuationTheory.Completion
variable {K S E : Type*} [Field K] [Field S] [Field E]
[Algebra K S] [Algebra K E] [IsSepClosed S] [Algebra.IsSeparable K S]theorem restrictionHom_apply
(i : S →ₐ[K] E) (σ : E ≃ₐ[K] E) (s : S) :
i (restrictionHom i σ s) = σ (i s)Restrict an automorphism over the base to an embedded separably closed separable extension. No separability of the ambient field is required.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ValuationTheory.Completion
variable {K S E : Type*} [Field K] [Field S] [Field E]
[Algebra K S] [Algebra K E] [IsSepClosed S] [Algebra.IsSeparable K S]def separableClosedAutRestriction
(i : S →ₐ[K] E) (σ : E ≃ₐ[K] E) : S ≃ₐ[K] SThe restricted automorphism acts through the original embedding.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ValuationTheory.Completion
variable {K S E : Type*} [Field K] [Field S] [Field E]
[Algebra K S] [Algebra K E] [IsSepClosed S] [Algebra.IsSeparable K S]theorem separableClosedAutRestriction_apply
(i : S →ₐ[K] E) (σ : E ≃ₐ[K] E) (s : S) :
i (separableClosedAutRestriction i σ s) = σ (i s)