ValuationSubring.lean

def absoluteValueUnitBallSubring
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) : Subring K where
  carrier := {x | v x ≤ 1}
  zero_mem' := by simp
  one_mem' := by simp
  add_mem' := by
    intro x y hx hy
    exact (LubinTate.Valuations.strong_triangle_of_nonarchimedean
      v hnonarch x y).trans (max_le hx hy)
  neg_mem' := by
    intro x hx
    simpa using hx
  mul_mem' := by
    intro x y hx hy
    change v (x * y) ≤ 1
    rw [v.map_mul]
    exact (mul_le_of_le_one_left (v.nonneg y) hx).trans hy

theorem mem_absoluteValueUnitBallSubring_iff
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) (x : K) :
    x ∈ absoluteValueUnitBallSubring v hnonarch ↔ v x ≤ 1

theorem absoluteValueUnitBallSubring_mem_or_inv_mem
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) (x : K) :
    x ∈ absoluteValueUnitBallSubring v hnonarch ∨
      x⁻¹ ∈ absoluteValueUnitBallSubring v hnonarch

def absoluteValueValuationSubring
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) :
    ValuationSubring K

theorem mem_absoluteValueValuationSubring_iff
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) (x : K) :
    x ∈ absoluteValueValuationSubring v hnonarch ↔
      v x ≤ 1

theorem isUnit_iff_abs_eq_one_of_mem_iff_le_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    {C : Type*} [SetLike C K] [SubmonoidClass C K]
    (S : C) (hS : ∀ x : K, x ∈ S ↔ v x ≤ 1) (x : S) :
    IsUnit x ↔ v (x : K) = 1

theorem not_isUnit_iff_abs_lt_one_of_mem_iff_le_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    {C : Type*} [SetLike C K] [SubmonoidClass C K]
    (S : C) (hS : ∀ x : K, x ∈ S ↔ v x ≤ 1) (x : S) :
    ¬ IsUnit x ↔ v (x : K) < 1

theorem absoluteValueUnitBallSubringAsValuationSubring_isUnit_iff_abs_eq_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (x : absoluteValueValuationSubring v hnonarch) :
    IsUnit x ↔ v (x : K) = 1

theorem absoluteValueValuationSubring_mem_maximalIdeal_iff_abs_lt_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (x : absoluteValueValuationSubring v hnonarch) :
    x ∈ IsLocalRing.maximalIdeal
        (absoluteValueValuationSubring v hnonarch) ↔
      v (x : K) < 1

theorem absoluteValueUnitBallSubringAsValuationSubring_residue_eq_zero_iff_abs_lt_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (x : absoluteValueValuationSubring v hnonarch) :
    IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch) x = 0 ↔
      v (x : K) < 1

theorem absoluteValueUnitBallSubringAsValuationSubring_residue_ne_zero_iff_abs_eq_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (x : absoluteValueValuationSubring v hnonarch) :
    IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch) x ≠ 0 ↔
      v (x : K) = 1

theorem absoluteValueUnitBallSubring_isIntegrallyClosedIn
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) :
    IsIntegrallyClosedIn (absoluteValueUnitBallSubring v hnonarch) K

theorem comap_absoluteValueUnitBallSubring_eq_of_extends
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ)
    (hvnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hwnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue w)
    (hw_ext : ∀ x : K, w (algebraMap K L x) = v x) :
    (absoluteValueUnitBallSubring w hwnonarch).comap
        (algebraMap K L) =
      absoluteValueUnitBallSubring v hvnonarch

theorem polynomial_lifts_absoluteValueUnitBallSubring_iff_coeff_mem
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) (f : K[X]) :
    f ∈ Polynomial.lifts
        (algebraMap (absoluteValueUnitBallSubring v hnonarch) K) ↔
      ∀ n : ℕ, f.coeff n ∈ absoluteValueUnitBallSubring v hnonarch

theorem exists_monic_polynomial_over_absoluteValueUnitBallSubring_of_coeff_mem
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) {f : K[X]}
    (hfmonic : f.Monic)
    (hfcoeff : ∀ n : ℕ, f.coeff n ∈ absoluteValueUnitBallSubring v hnonarch) :
    ∃ F : (absoluteValueUnitBallSubring v hnonarch)[X],
      F.Monic ∧
        F.map (algebraMap (absoluteValueUnitBallSubring v hnonarch) K) = f ∧
        F.natDegree = f.natDegree

theorem exists_polynomial_over_absoluteValueUnitBallSubringAsValuationSubring_of_coeff_abs_le_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) (f : K[X])
    (hfcoeff : ∀ n : ℕ, v (f.coeff n) ≤ 1) :
    ∃ F : (absoluteValueValuationSubring v hnonarch)[X],
      F.map (algebraMap
          (absoluteValueValuationSubring v hnonarch) K) = f ∧
        F.natDegree = f.natDegree ∧
          ∀ n : ℕ, v (F.coeff n : K) = v (f.coeff n)