localFullLevel isOpen

Stream: FLT

[Yakov Pechersky]

Is it the case that the supreme of two valuations is a valuation; relatedly, is it the case that the matrix ring over a valued ring is valued itself, with the supremum valuation over the elements? This holds for a rank one/MulArchimedean valuation, since those can be converted to a norm.

Given that, then the isOpen proof for localFullLevel can rely on the fact that matrices over the integers subring with det = 1 are a subset of the sphere at matrix valuation 1, since it must have at least one element at valuation 1.

[Kevin Buzzard]

If v(xy)=v(x)v(y) is the axiom then sup of two valuations isn't a valuation but if the axiom is <= then it is.

[Yakov Pechersky]

OK, just some scratch work if useful for anyone:

open scoped Valued NormedField

#synth Field (v.adicCompletion F)
#synth NormedField (v.adicCompletion F)
#synth IsUltrametricDist (v.adicCompletion F)
#synth IsUltrametricDist (v.adicCompletionIntegers F)
#synth NormedAddCommGroup (Fin 2 → (v.adicCompletion F))

section

variable {m' n' : Type*} [Fintype m'] [Fintype n']

instance foo {ι : Type*} {π : ι → Type*} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)]
    [(i : ι) → IsUltrametricDist (π i)] :
    IsUltrametricDist ((i : ι) → π i) := by
  refine IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm ?_
  intro f g
  simp only [Pi.norm_def, Pi.add_apply, le_sup_iff, NNReal.coe_le_coe, Finset.sup_le_iff,
    Finset.mem_univ, forall_const]
  by_cases H : ∃ i, ∀ j, ‖g j‖₊ ≤ ‖f i‖₊
  · obtain ⟨i, hi⟩ := H
    refine Or.inl ?_
    intro j
    refine (IsUltrametricDist.nnnorm_add_le_max _ _).trans (sup_le ?_ ((hi _).trans ?_)) <;>
    exact Finset.le_sup (f := fun i ↦ ‖f i‖₊) (Finset.mem_univ _)
  · push_neg at H
    refine Or.inr ?_
    intro i
    obtain ⟨j, hj⟩ := H i
    refine (IsUltrametricDist.nnnorm_add_le_max _ _).trans (sup_le (hj.le.trans ?_) ?_) <;>
    exact Finset.le_sup (f := fun i ↦ ‖g i‖₊) (Finset.mem_univ _)

noncomputable
local instance :
    NormedAddCommGroup (Matrix m' n' (v.adicCompletionIntegers F)) :=
  Matrix.normedAddCommGroup

instance : IsUltrametricDist ((Matrix m' n' (v.adicCompletionIntegers F))) := foo

variable {L : Type*} [Field L] {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
  [val : Valued L Γ₀] [hv : Valuation.RankOne val.v] in
lemma Valued.toNormedField_norm_eq (x : L) :
  letI _ : NormedField L := Valued.toNormedField L Γ₀
  ‖x‖₊ = hv.hom (Valued.v x) := rfl

lemma bar :
    IsOpen {x : Matrix m' n' (v.adicCompletionIntegers F) | ∃ i j, Valued.v (x i j).val = 1} := by
  convert IsUltrametricDist.isOpen_sphere (0 : Matrix m' n' (v.adicCompletionIntegers F))
    one_ne_zero
  ext f
  simp only [Set.mem_setOf_eq, mem_sphere_iff_norm, sub_zero, Matrix.norm_def, Pi.norm_def,
    Pi.nnnorm_def, ← NormedField.valuation_apply]
  constructor
  · rintro ⟨i, j, h⟩
    rw [le_antisymm_iff]
    simp only [NNReal.coe_le_one, Finset.sup_le_iff, Finset.mem_univ, forall_const,
      NNReal.one_le_coe, bot_eq_zero', zero_lt_one, Finset.le_sup_iff, true_and]
    refine ⟨?_, ?_⟩
    · intro x y
      simp [← NNReal.coe_le_coe, ← HeightOneSpectrum.mem_adicCompletionIntegers, (f _ _).prop]
    · refine ⟨i, j, ?_⟩
      simpa [← Valued.toNormedField.one_le_norm_iff] using h.ge
  · contrapose!
    intro H
    refine ne_of_lt ?_
    simp only [NNReal.coe_lt_one, bot_eq_zero', zero_lt_one, Finset.sup_lt_iff, Finset.mem_univ,
      forall_const]
    intro i j
    simp only [← NNReal.coe_lt_one, coe_nnnorm, AddSubgroupClass.coe_norm,
      Valued.toNormedField.norm_lt_one_iff]
    refine lt_of_le_of_ne ?_ (H _ _)
    simp [← HeightOneSpectrum.mem_adicCompletionIntegers, (f _ _).prop]

[Yakov Pechersky]

I'll PR the IsUltrametricDist pi result to mathlib

[Yakov Pechersky]

#22575

[Yakov Pechersky]

I've also started on the generalization of nonarchimedean normed spaces to nonarchimedean uniformities, which would also work for valued spaces that aren't necessarily rank one
#22580

[Kevin Buzzard]

(non-update: I have been temporarily distracted by various grant deadlines but will be back on FLT in a few days)