Completion.lean

def completionAbsoluteValue
    {K : Type u} [Field K] (vK : AbsoluteValue K ℝ) :
    AbsoluteValue vK.Completion ℝ

theorem completionAbsoluteValue_coe
    {K : Type u} [Field K] (vK : AbsoluteValue K ℝ) (x : K) :
    completionAbsoluteValue vK (x : vK.Completion) = vK x

theorem completionAbsoluteValue_uniformSpace_eq
    {K : Type u} [Field K] (vK : AbsoluteValue K ℝ) :
    (completionAbsoluteValue vK).uniformSpace =
      (@UniformSpace.Completion.uniformSpace (WithAbs vK) inferInstance)

theorem completionAbsoluteValue_complete
    {K : Type u} [Field K] (vK : AbsoluteValue K ℝ) :
    CompleteSpace (WithAbs (completionAbsoluteValue vK))

theorem completionAbsoluteValue_isNontrivial
    {K : Type u} [Field K] (vK : AbsoluteValue K ℝ)
    (hvK : vK.IsNontrivial) :
    (completionAbsoluteValue vK).IsNontrivial

def toCompletion
    {K : Type u} [Field K] (vK : AbsoluteValue K ℝ) :
    K →+* vK.Completion

theorem toCompletion_apply
    {K : Type u} [Field K] (vK : AbsoluteValue K ℝ) (x : K) :
    toCompletion vK x = ((WithAbs.equiv vK).symm x : vK.Completion)

theorem toCompletion_eq_algebraMap
    {K : Type u} [Field K] (vK : AbsoluteValue K ℝ) (x : K) :
    toCompletion vK x = algebraMap K vK.Completion x

theorem denseRange_toCompletion
    {K : Type u} [Field K] (vK : AbsoluteValue K ℝ) :
    DenseRange (toCompletion vK)

def baseToExtensionCompletion
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (wL : AbsoluteValue L ℝ) :
    WithAbs vK →+* wL.Completion

theorem baseToExtensionCompletion_norm
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (wL : AbsoluteValue L ℝ)
    (hw : Extends vK wL) (x : WithAbs vK) :
    ‖baseToExtensionCompletion vK wL x‖ = ‖x‖

theorem baseToExtensionCompletion_isometry
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (wL : AbsoluteValue L ℝ)
    (hw : Extends vK wL) :
    Isometry (baseToExtensionCompletion vK wL)

def completionMap
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (wL : AbsoluteValue L ℝ)
    (hw : Extends vK wL) :
    vK.Completion →+* wL.Completion

theorem completionMap_withAbs_coe
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (wL : AbsoluteValue L ℝ)
    (hw : Extends vK wL) (x : WithAbs vK) :
    completionMap vK wL hw (x : vK.Completion) =
      baseToExtensionCompletion vK wL x

theorem completionMap_coe
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (wL : AbsoluteValue L ℝ)
    (hw : Extends vK wL) (x : K) :
    completionMap vK wL hw (algebraMap K vK.Completion x) =
      toCompletion wL (algebraMap K L x)

theorem completionMap_isometry
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (wL : AbsoluteValue L ℝ)
    (hw : Extends vK wL) :
    Isometry (completionMap vK wL hw)

def completionAlgebra
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (wL : AbsoluteValue L ℝ)
    (hw : Extends vK wL) :
    Algebra vK.Completion wL.Completion

theorem completionAlgebra_algebraMap
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (wL : AbsoluteValue L ℝ)
    (hw : Extends vK wL) (x : vK.Completion) :
    @algebraMap vK.Completion wL.Completion _ _
        (completionAlgebra vK wL hw) x = completionMap vK wL hw x

def extensionCompletionAlgebra
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (wL : AbsoluteValue L ℝ) :
    Algebra K wL.Completion

def toCompletionAlgHom
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (wL : AbsoluteValue L ℝ) :
    letI := extensionCompletionAlgebra (K := K) wL
    L →ₐ[K] wL.Completion := by
  letI := extensionCompletionAlgebra (K := K) wL
  exact
    { __ := toCompletion wL
      commutes' _ := rfl }

theorem completion_isScalarTower
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (wL : AbsoluteValue L ℝ)
    (hw : Extends vK wL) :
    letI hK := extensionCompletionAlgebra (K := K) wL
    letI : SMul K wL.Completion := hK.toSMul
    letI := completionAlgebra vK wL hw
    IsScalarTower K vK.Completion wL.Completion := by
  let hK := extensionCompletionAlgebra (K := K) wL
  let : SMul K wL.Completion := hK.toSMul
  let := completionAlgebra vK wL hw
  exact IsScalarTower.of_algebraMap_eq fun x ↦
    (completionMap_coe vK wL hw x).symm

theorem completionAbsoluteValue_extends
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (wL : AbsoluteValue L ℝ)
    (hw : Extends vK wL) :
    letI := completionAlgebra vK wL hw
    Extends (completionAbsoluteValue vK) (completionAbsoluteValue wL) := by
  let := completionAlgebra vK wL hw
  intro x
  change ‖algebraMap vK.Completion wL.Completion x‖ = ‖x‖
  exact (completionMap_isometry vK wL hw).norm_map_of_map_zero
    (map_zero _) x

theorem completionAbsoluteValue_isNonarchimedean
    {K : Type u} [Field K] (vK : AbsoluteValue K ℝ)
    (hvK : IsNonarchimedean (vK : K → ℝ)) :
    IsNonarchimedean
      (completionAbsoluteValue vK : vK.Completion → ℝ)

theorem completionAbsoluteValue_range_eq
    {K : Type u} [Field K] (vK : AbsoluteValue K ℝ)
    (hvK : IsNonarchimedean (vK : K → ℝ)) :
    Set.range (completionAbsoluteValue vK) = Set.range vK

def toCompleteTargetRingHom
    (vK : AbsoluteValue K ℝ) (vD : AbsoluteValue D ℝ)
    (i : K →+* D) :
    WithAbs vK →+* WithAbs vD

theorem toCompleteTargetRingHom_norm
    (vK : AbsoluteValue K ℝ) (vD : AbsoluteValue D ℝ)
    (i : K →+* D) (hi : ∀ x : K, vD (i x) = vK x)
    (x : WithAbs vK) :
    ‖toCompleteTargetRingHom vK vD i x‖ = ‖x‖

theorem toCompleteTargetRingHom_isometry
    (vK : AbsoluteValue K ℝ) (vD : AbsoluteValue D ℝ)
    (i : K →+* D) (hi : ∀ x : K, vD (i x) = vK x) :
    Isometry (toCompleteTargetRingHom vK vD i)

def completionMapToCompleteTarget
    (vK : AbsoluteValue K ℝ) (vD : AbsoluteValue D ℝ)
    [CompleteSpace (WithAbs vD)]
    (i : K →+* D) (hi : ∀ x : K, vD (i x) = vK x) :
    vK.Completion →+* WithAbs vD

theorem completionMapToCompleteTarget_withAbs_coe
    (vK : AbsoluteValue K ℝ) (vD : AbsoluteValue D ℝ)
    [CompleteSpace (WithAbs vD)]
    (i : K →+* D) (hi : ∀ x : K, vD (i x) = vK x)
    (x : WithAbs vK) :
    completionMapToCompleteTarget vK vD i hi
        (x : vK.Completion) =
      toCompleteTargetRingHom vK vD i x

theorem completionMapToCompleteTarget_coe
    (vK : AbsoluteValue K ℝ) (vD : AbsoluteValue D ℝ)
    [CompleteSpace (WithAbs vD)]
    (i : K →+* D) (hi : ∀ x : K, vD (i x) = vK x)
    (x : K) :
    completionMapToCompleteTarget vK vD i hi
        (algebraMap K vK.Completion x) =
      (WithAbs.equiv vD).symm (i x)

theorem completionMapToCompleteTarget_isometry
    (vK : AbsoluteValue K ℝ) (vD : AbsoluteValue D ℝ)
    [CompleteSpace (WithAbs vD)]
    (i : K →+* D) (hi : ∀ x : K, vD (i x) = vK x) :
    Isometry (completionMapToCompleteTarget vK vD i hi)

theorem completionMapToCompleteTarget_eq_of_coe_eq
    (vK : AbsoluteValue K ℝ) (vD : AbsoluteValue D ℝ)
    [CompleteSpace (WithAbs vD)]
    (i : K →+* D) (hi : ∀ x : K, vD (i x) = vK x)
    (g : vK.Completion →+* WithAbs vD) (hg : Continuous g)
    (hcoe : ∀ x : K,
      completionMapToCompleteTarget vK vD i hi
          (algebraMap K vK.Completion x) =
        g (algebraMap K vK.Completion x)) :
    completionMapToCompleteTarget vK vD i hi = g

theorem completionMapToCompleteTarget_comp_completionMap_coe
    (vK : AbsoluteValue K ℝ) (wL : AbsoluteValue L ℝ)
    (hw : Extends vK wL) (vD : AbsoluteValue D ℝ)
    [CompleteSpace (WithAbs vD)]
    (i : L →+* D) (hi : ∀ x : L, vD (i x) = wL x)
    (x : K) :
    completionMapToCompleteTarget wL vD i hi
        (completionMap vK wL hw (algebraMap K vK.Completion x)) =
      (WithAbs.equiv vD).symm (i (algebraMap K L x))

theorem completionMapToCompleteTarget_comp_completionMap_eq_of_coe_eq
    (vK : AbsoluteValue K ℝ) (wL : AbsoluteValue L ℝ)
    (hw : Extends vK wL) (vD : AbsoluteValue D ℝ)
    [CompleteSpace (WithAbs vD)]
    (i : L →+* D) (hi : ∀ x : L, vD (i x) = wL x)
    (g : vK.Completion →+* WithAbs vD) (hg : Continuous g)
    (hcoe : ∀ x : K,
      (WithAbs.equiv vD).symm (i (algebraMap K L x)) =
        g (algebraMap K vK.Completion x)) :
    (completionMapToCompleteTarget wL vD i hi).comp
        (completionMap vK wL hw) = g