ValuationTheory.DiscreteValuationField.HenselianDVF.separableClosedAutEquiv
The chosen embedding identifies the automorphism groups by actual extension and restriction, with multiplication given by composition.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K : Type*} [Field K] (base : HenselianDVF K)
{S E : Type*} [Field S] [Field E] [Algebra K S]
[Algebra base.valuation.Completion E] [Algebra K E]
[IsScalarTower K base.valuation.Completion E] [Algebra.IsSeparable K S]
[IsSepClosed S] [Algebra.IsSeparable base.valuation.Completion E]Lean source · full declaration
def separableClosedAutEquiv (i : S →ₐ[K] E) :
(S ≃ₐ[K] S) ≃* (E ≃ₐ[base.valuation.Completion] E) where
toFun := base.extendSeparableClosedAut i
invFun σ := Completion.separableClosedAutRestriction i (σ.restrictScalars K)
left_inv σ := by
apply AlgEquiv.ext
intro s
apply i.injective
change i (Completion.separableClosedAutRestriction i
((base.extendSeparableClosedAut i σ).restrictScalars K) s) = i (σ s)
rw [Completion.separableClosedAutRestriction_apply]
exact base.extendSeparableClosedAut_apply i σ s
right_inv σ := by
apply AlgEquiv.coe_toAlgHom_injective
apply AlgHom.ext_of_adjoin_eq_top (base.toDVF.adjoin_range_eq_top_of_isSepClosed i)
rintro x ⟨s, rfl⟩
change base.extendSeparableClosedAut i
(Completion.separableClosedAutRestriction i (σ.restrictScalars K)) (i s) = σ (i s)
rw [extendSeparableClosedAut_apply, Completion.separableClosedAutRestriction_apply]
rfl
map_mul' := base.extendSeparableClosedAut_mul i