HenselianSeparableClosure.lean

theorem exists_algebraMap_eq_of_normal_of_approximable
    {K L : Type*} [NormedField K] [NormedField L]
    [IsUltrametricDist K] [IsUltrametricDist L] [NormedAlgebra K L]
    [FiniteDimensional K L] [Normal K L]
    [HenselianRing (NormedField.valuation (K := K)).valuationSubring
      (IsLocalRing.maximalIdeal (NormedField.valuation (K := K)).valuationSubring)]
    (a : L) (ha : IsSeparable K a)
    (happrox : ∀ ε : ℝ, 0 < ε → ∃ k : K, ‖a - algebraMap K L k‖ < ε) :
    ∃ k : K, algebraMap K L k = a

theorem exists_algebraMap_eq_of_isAlgClosed_of_approximable
    {K Ω : Type*} [NormedField K] [NormedField Ω]
    [IsUltrametricDist K] [IsUltrametricDist Ω] [NormedAlgebra K Ω] [IsAlgClosed Ω]
    [HenselianRing (NormedField.valuation (K := K)).valuationSubring
      (IsLocalRing.maximalIdeal (NormedField.valuation (K := K)).valuationSubring)]
    (a : Ω) (ha : IsSeparable K a)
    (happrox : ∀ ε : ℝ, 0 < ε → ∃ k : K, ‖a - algebraMap K Ω k‖ < ε) :
    ∃ k : K, algebraMap K Ω k = a

theorem exists_algebraMap_eq_of_complete_of_approximable
    {K D : Type*} [NormedField K] [NontriviallyNormedField D]
    [IsUltrametricDist K] [IsUltrametricDist D] [NormedAlgebra K D] [CompleteSpace D]
    [HenselianRing (NormedField.valuation (K := K)).valuationSubring
      (IsLocalRing.maximalIdeal (NormedField.valuation (K := K)).valuationSubring)]
    (a : D) (ha : IsSeparable K a)
    (happrox : ∀ ε : ℝ, 0 < ε → ∃ k : K, ‖a - algebraMap K D k‖ < ε) :
    ∃ k : K, algebraMap K D k = a

theorem exists_completion_eq_of_isSeparable
    {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K]
    [HenselianRing (NormedField.valuation (K := K)).valuationSubring
      (IsLocalRing.maximalIdeal (NormedField.valuation (K := K)).valuationSubring)]
    (a : UniformSpace.Completion K) (ha : IsSeparable K a) :
    ∃ k : K, (k : UniformSpace.Completion K) = a