The infinite place(s) of Q

Stream: Is there code for X?

[Kevin Buzzard]

I was going to prove a theorem about adeles of a number field by reducing to Q but I was unexpectedly thrown by a lack of API for infinite places for Q. I got this far:

import Mathlib

open NumberField

-- do we not have this?
def Rat.realAbsoluteValue : AbsoluteValue ℚ ℝ where
  toFun q := |q|
  map_mul' x y := by simp only [cast_mul, abs_mul]
  nonneg' x := by simp only [abs_nonneg]
  eq_zero' x := by simp only [abs_eq_zero, cast_eq_zero]
  add_le' x y := by simp only [cast_add, abs_add_le]

-- one possibility for def of unique infinite place
def Rat.infinitePlace : InfinitePlace ℚ := ⟨Rat.realAbsoluteValue, Rat.castHom ℂ, by
  ext; simp [Rat.realAbsoluteValue]⟩

-- another one
noncomputable def Rat.infinitePlace' : InfinitePlace ℚ := .mk (Rat.castHom _)

-- there's only one anyway
instance : Subsingleton (InfinitePlace ℚ) where
  allEq a b := Subtype.ext <| by
    obtain ⟨_, _, rfl⟩ := a
    obtain ⟨_, _, rfl⟩ := b
    ext
    simp

-- this is true for all of them
lemma Rat.infinitePlace_apply (v : InfinitePlace ℚ) (x : ℚ) : v x = |x| := by
  obtain ⟨_, _, rfl⟩ := v
  change place _ _ = _
  simp

-- stuck on this
lemma foo (v : InfinitePlace ℚ) (x : ℚ) : ‖(x : v.completion)‖ = |x| := by
  sorry

There are three possibilities for trying to prove foo -- either cases on v, or use Subsingleton.elim to reduce to either infinitePlace or infinitePlace', but I couldn't get any of them to work :-) I'm only just learning all the API for this stuff, I've not really thought about real-valued norms before.

[Riccardo Brasca]

Cc @Xavier Roblot

[Andrew Yang]

lemma foo (v : InfinitePlace ℚ) (x : ℚ) : ‖(x : v.completion)‖ = |x| := by
  convert UniformSpace.Completion.norm_coe (E := WithAbs v.1) x using 1
  · congr 1
    show _ = UniformSpace.Completion.coeRingHom (α := WithAbs v.1) x
    exact (eq_ratCast _ _).symm
  · show _ = v.1 x
    obtain ⟨_, v, rfl⟩ := v
    simp

[Adam Topaz]

That's a lot of borderline defeq abuse, which probably suggests some missing API

[Andrew Yang]

We definitely need the rewrite lemmas instead of the show.

[Kevin Buzzard]

After many hours of trying to understand @Andrew Yang 's proof, I've come up with this, which I propose PRing. Any comments before I do?

import Mathlib

-- uniform space completion API
lemma UniformSpace.Completion.coeRingHom_apply {α : Type*} [Ring α] [UniformSpace α]
    [TopologicalRing α] [UniformAddGroup α] (x : α) : coeRingHom x = ↑x := rfl

-- WithAbs.equiv API
lemma WithAbs.abv_equiv {R : Type*} [Ring R] (a : AbsoluteValue R ℝ)
    (x : WithAbs a) : a ((WithAbs.equiv a) x) = ‖x‖ := rfl

lemma WithAbs.norm_equiv_symm {R : Type*} [Ring R] (a : AbsoluteValue R ℝ) (x : R) :
    ‖(WithAbs.equiv a).symm x‖ = a x := rfl

def WithAbs.equivRingHom {R : Type*} [Semiring R] (a : AbsoluteValue R ℝ) :
    WithAbs a ≃+* R where
  toFun := WithAbs.equiv a
  invFun := (WithAbs.equiv a).symm
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl
  map_add' _ _ := rfl

-- Infinite place API
lemma NumberField.InfinitePlace.apply_def {K : Type*} [Field K] (v : InfinitePlace K) (x : K) :
  v x = v.1 x := rfl

-- Infinite place of ℚ API
open NumberField

noncomputable def Rat.infinitePlace : InfinitePlace ℚ := .mk (Rat.castHom _)

instance : Subsingleton (InfinitePlace ℚ) where
  allEq a b := Subtype.ext <| by
    obtain ⟨_, _, rfl⟩ := a
    obtain ⟨_, _, rfl⟩ := b
    ext
    simp

lemma Rat.infinitePlace_apply (v : InfinitePlace ℚ) (x : ℚ) : v x = |x| := by
  rw [NumberField.InfinitePlace.apply_def]
  obtain ⟨_, _, rfl⟩ := v
  simp

-- no defeq abuse
lemma Rat.norm_infinitePlace_completion (v : InfinitePlace ℚ) (x : ℚ) :
    ‖(x : v.completion)‖ = |x| := by
  rw [← eq_ratCast (UniformSpace.Completion.coeRingHom.comp (WithAbs.equivRingHom v.1).symm)]
  have := UniformSpace.Completion.norm_coe ((WithAbs.equiv v.1).symm x)
  rw [WithAbs.norm_equiv_symm] at this
  obtain ⟨a, φ, rfl⟩ := v
  simp [WithAbs.equivRingHom, this, UniformSpace.Completion.coeRingHom_apply]

[Andrew Yang]

I would suggest to also add the following two lemmas

lemma NumberField.InfinitePlace.completion.norm_coe {K : Type*} [Field K]
    (v : InfinitePlace K) (x : WithAbs v.1) :
    ‖(x : v.completion)‖ = v (WithAbs.equiv v.1 x) :=
  UniformSpace.Completion.norm_coe x

lemma WithAbs.ratCast_equiv (v : InfinitePlace ℚ) (x : WithAbs v.1) :
    Rat.cast (WithAbs.equiv _ x) = (x : v.completion) :=
  (eq_ratCast (UniformSpace.Completion.coeRingHom.comp (WithAbs.equivRingHom v.1).symm.toRingHom) x).symm

-- no defeq abuse
lemma Rat.norm_infinitePlace_completion (v : InfinitePlace ℚ) (x : ℚ) :
    ‖(x : v.completion)‖ = |x| := by
  rw [← (WithAbs.equiv v.1).apply_symm_apply x, WithAbs.ratCast_equiv,
    NumberField.InfinitePlace.completion.norm_coe, (WithAbs.equiv v.1).apply_symm_apply,
    Rat.infinitePlace_apply]

[Kevin Buzzard]

#19644

[Jz Pan]

Maybe you can write

def WithAbs.equivRingHom {R : Type*} [Semiring R] (a : AbsoluteValue R ℝ) :
    WithAbs a ≃+* R where
  __ := WithAbs.equiv a
  map_mul' _ _ := rfl
  map_add' _ _ := rfl

(untested)

[Kevin Buzzard]

During the PR process I discovered we already had it: docs#WithAbs.ringEquiv (and this is what I use in #19644)