AbsoluteValue.lean

def realAbsoluteValueValuation
    {F : Type*} [Field F]
    (vF : AbsoluteValue F ℝ)
    (hvF : IsNonarchimedean (vF : F → ℝ)) :
    Valuation F NNReal where
  toFun x := ⟨vF x, vF.nonneg x⟩
  map_one' := by
    ext
    exact vF.map_one
  map_zero' := by
    ext
    exact vF.map_zero
  map_mul' x y := by
    ext
    exact vF.map_mul x y
  map_add_le_max' x y := by
    change vF (x + y) ≤ max (vF x) (vF y)
    exact hvF x y

theorem realAbsoluteValueValuation_apply
    {F : Type*} [Field F]
    (vF : AbsoluteValue F ℝ)
    (hvF : IsNonarchimedean (vF : F → ℝ))
    (x : F) :
    ((realAbsoluteValueValuation vF hvF x : NNReal) : ℝ) =
      vF x

theorem absoluteValueExtension_isNonarchimedean
    {F E : Type*} [Field F] [Field E] [Algebra F E]
    (vF : AbsoluteValue F ℝ)
    (hvF : IsNonarchimedean (vF : F → ℝ))
    (w : AbsoluteValueExtension vF E) :
    IsNonarchimedean (w.1 : E → ℝ)

theorem absoluteValue_le_one_of_isIntegral
    {F : Type*} [Field F]
    (vF : AbsoluteValue F ℝ)
    (hvF : IsNonarchimedean (vF : F → ℝ))
    {x : F} (hx : IsIntegral ℤ x) :
    vF x ≤ 1

def absoluteValueCompletionIntegers
    {F : Type*} [Field F]
    (vF : AbsoluteValue F ℝ)
    (hvF : IsNonarchimedean (vF : F → ℝ)) :
    ValuationSubring vF.Completion

theorem mem_absoluteValueCompletionIntegers_iff
    {F : Type*} [Field F]
    (vF : AbsoluteValue F ℝ)
    (hvF : IsNonarchimedean (vF : F → ℝ))
    (x : vF.Completion) :
    x ∈ absoluteValueCompletionIntegers vF hvF ↔
      ‖x‖ ≤ 1

theorem isIntegral_over_baseCompletionIntegers_of_mem
    [Algebra.IsSeparable K L]
    (vK : AbsoluteValue K ℝ)
    (hvK : IsNonarchimedean (vK : K → ℝ))
    (hvK0 : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
    {x : w.1.Completion}
    (hx : x ∈ absoluteValueCompletionIntegers w.1
      (absoluteValueExtension_isNonarchimedean vK hvK w)) :
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    IsIntegral (absoluteValueCompletionIntegers vK hvK) x := by
  let hw : IsNonarchimedean (w.1 : L → ℝ) :=
    absoluteValueExtension_isNonarchimedean vK hvK w
  let aC := AbsoluteValue.completionAbsoluteValue vK
  let bC := AbsoluteValue.completionAbsoluteValue w.1
  let haC : LubinTate.Valuations.NonarchimedeanAbsoluteValue aC :=
    (AbsoluteValue.isNonarchimedean_iff_bounded_nat aC).1
      (AbsoluteValue.completionAbsoluteValue_isNonarchimedean vK hvK)
  let hbC : LubinTate.Valuations.NonarchimedeanAbsoluteValue bC :=
    (AbsoluteValue.isNonarchimedean_iff_bounded_nat bC).1
      (AbsoluteValue.completionAbsoluteValue_isNonarchimedean w.1 hw)
  let va :=
    absoluteValueExponentialValuation aC haC
  let vb :=
    absoluteValueExponentialValuation bC hbC
  let : Algebra vK.Completion w.1.Completion :=
    AbsoluteValue.completionAlgebra vK w.1 w.2
  let : Module.Finite vK.Completion w.1.Completion :=
    completionModuleFinite vK hvK0 w
  let : Algebra.IsAlgebraic vK.Completion w.1.Completion :=
    Algebra.IsAlgebraic.of_finite vK.Completion w.1.Completion
  have hVaAbs :
      LubinTate.Valuations.exponentialValuationSubringAsValuationSubring va =
        absoluteValueValuationSubring aC haC :=
    associatedAbsoluteValue_valuationSubring_eq
      va (Real.exp 1) aC haC
        (absoluteValueExponentialValuation_associated aC haC)
  have hVbAbs :
      LubinTate.Valuations.exponentialValuationSubringAsValuationSubring vb =
        absoluteValueValuationSubring bC hbC :=
    associatedAbsoluteValue_valuationSubring_eq
      vb (Real.exp 1) bC hbC
        (absoluteValueExponentialValuation_associated bC hbC)
  have hVa :
      LubinTate.Valuations.exponentialValuationSubringAsValuationSubring va =
        absoluteValueCompletionIntegers vK hvK := by
    rw [hVaAbs]
    ext y
    rw [mem_absoluteValueValuationSubring_iff,
      mem_absoluteValueCompletionIntegers_iff]
    rfl
  have hVb :
      LubinTate.Valuations.exponentialValuationSubringAsValuationSubring vb =
        absoluteValueCompletionIntegers w.1 hw := by
    rw [hVbAbs]
    ext y
    rw [mem_absoluteValueValuationSubring_iff,
      mem_absoluteValueCompletionIntegers_iff]
    rfl
  have hhensAbs :
      ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
        (absoluteValueValuationSubring aC haC).valuation :=
    henselianValuation_of_complete aC
      ((absoluteValueCompleteness_completeSpace_withAbs_iff_complete aC).1
        (AbsoluteValue.completionAbsoluteValue_complete vK))
      haC
  have hhens :
      ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
        (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring
          va).valuation := by
    rw [hVaAbs]
    exact hhensAbs
  have hExt :
      ∀ y : vK.Completion,
        bC (algebraMap vK.Completion w.1.Completion y) = aC y :=
    AbsoluteValue.completionAbsoluteValue_extends vK w.1 w.2
  have hclosure :=
    exponentialValuationSubring_eq_integralClosure_of_henselian
      va vb
      (absoluteValueExponentialValuation_extends
        aC bC haC hbC hExt)
      hhens
  rw [hVa, hVb] at hclosure
  rw [← mem_integralClosure_iff]
  change x ∈
    (integralClosure
      (absoluteValueCompletionIntegers vK hvK) w.1.Completion).toSubring
  rw [← hclosure]
  exact hx