SeparableClosureConjugation.lean

def separableClosureEquivOfEquiv (τ : K ≃+* K) :
    SeparableClosure K ≃+* SeparableClosure K

theorem separableClosureEquivOfEquiv_apply_coe
    (τ : K ≃+* K) (x : SeparableClosure K) :
    (separableClosureEquivOfEquiv τ x : AlgebraicClosure K) =
      IsAlgClosure.equivOfEquiv (AlgebraicClosure K) (AlgebraicClosure K) τ
        (x : AlgebraicClosure K)

theorem separableClosureEquivOfEquiv_symm_apply_coe
    (τ : K ≃+* K) (x : SeparableClosure K) :
    ((separableClosureEquivOfEquiv τ).symm x : AlgebraicClosure K) =
      (IsAlgClosure.equivOfEquiv (AlgebraicClosure K) (AlgebraicClosure K) τ).symm
        (x : AlgebraicClosure K)

theorem separableClosureEquivOfEquiv_algebraMap (τ : K ≃+* K) (x : K) :
    separableClosureEquivOfEquiv τ (algebraMap K (SeparableClosure K) x) =
      algebraMap K (SeparableClosure K) (τ x)

theorem separableClosureAutEquiv_absoluteGaloisConjugate
    (τ : K ≃+* K) (σ : Gal(AlgebraicClosure K/K)) :
    ValuationTheory.Completion.separableClosureAutEquiv K
        (absoluteGaloisConjugate τ σ) =
      semilinearGaloisConjugate τ (separableClosureEquivOfEquiv τ)
        (separableClosureEquivOfEquiv_algebraMap τ)
        (ValuationTheory.Completion.separableClosureAutEquiv K σ)