Solid

Stream: maths

[Xavier Roblot]

I would like to generalise the results of the PR #18266 and #18477 on the theory of ℤ-lattices that are proved for ℝ to other fields (in particular ℚ). The right generalization appears to be docs#normed_linear_ordered_field with the additional property:
∀ a b, |a| ≤ |b| → ‖a‖ ≤ ‖b‖. This property already exists in mathlib as the property solid of docs#normed_lattice_add_comm_group.

My first idea is to add a class is_solid

class is_solid (α : Type*) [normed_linear_ordered_add_group α] : Prop :=
(solid: ∀ a b : α, |a| ≤ |b| → ‖a‖ ≤ ‖b‖)

and then an instance from normed_linear_ordered_field to normed_linear_ordered_add_group. It is then easy to prove that ℝ and ℚ (for which mathlib already knows that there are normed_linear_ordered_field) satisfy is_solid.

On the other hand, it would be nice to connect this to the property solid of docs#normed_lattice_add_comm_group so another option would be to create the class normed_lattice_field(?) that would extend both normed_linear_ordered_field and normed_lattice_add_comm_group. I am not sure if that is feasible easily though.

In any case, I'd like to get some advice on the best option and the best way to proceed.

[Kevin Buzzard]

Dare I ask whether there's any object in mathlib which has both a |b| and a ‖b‖, and they don't coincide?

[Xavier Roblot]

Well, I was quite surprised to find out that it is not part of the definition of docs#normed_linear_ordered_field... But it appears it is possible to have both exist and be different.

[Eric Wieser]

@Kevin Buzzard, I assume the point is that abs : K → K and norm : K → ℝ

[Eric Wieser]

So the question is really "when is ↑|b| ≠ ‖b‖", for which I suspect there is something Kevin can come up with about the p-adic norm on ℚ

[Eric Wieser]

Do you care about any types which don't satisfy algebra K ℝ?

[Xavier Roblot]

Eric Wieser said:

Do you care about any types which don't satisfy algebra K ℝ?

Probably not.

[Eric Wieser]

Is normed_algebra K ℝ acceptable?

[Eric Wieser]

That doesn't allow K=ℤ (though arguably we should refactor so that it does)

[Eric Wieser]

But that should give you ‖↑k‖ = ‖k • 1‖ = ‖k‖ * 1 = ‖k‖ = |k|

[Xavier Roblot]

That looks good to me. Let me try that

[Eric Wieser]

docs#norm_algebra_map' should be defeq to the left parts of that statement

[Kevin Buzzard]

Eric Wieser said:

So the question is really "when is ↑|b| ≠ ‖b‖", for which I suspect there is something Kevin can come up with about the p-adic norm on ℚ

Xavier is also well aware of the p-adic norm on the rationals :-)

[Eric Wieser]

Do we have a way to spell "ℚ but with the p-adic norm"? I think it would be worth PRing something minimal if so, just so that when this type of thing comes up it's possible to provide a counterexample in lean and not english

[Xavier Roblot]

Eric Wieser said:

Is normed_algebra K ℝ acceptable?

I cannot make it work, I am afraid. The problem is that I still need linear_ordered_field since I use docs#int.fract and then the absolute value coming from linear_ordered_field is disconnected to the norm unless I am missing something. Basically, this is what I need:

import analysis.normed.order.basic

variables {K : Type*} [normed_linear_ordered_field K] [normed_algebra K ℝ]

example (x : K) (h : |x| ≤ 1) : ‖x‖ ≤ 1 :=
begin
  sorry
end

[Eric Wieser]

docs#norm_eq_abs?

[Eric Wieser]

You can get the goal to |x • (1 : ℝ)| ≤ 1 without too much work

[Eric Wieser]

But then I guess you're stuck

[Eric Wieser]

We don't even seem to have the version of norm_eq_abs on rat!

[Xavier Roblot]

I am stuck

[Xavier Roblot]

Maybe the best way is to do

class normed_lattice_field (α : Type*)
extends normed_linear_ordered_field α :=
(solid: ∀ a b : α, |a| ≤ |b| → ‖a‖ ≤ ‖b‖)

instance normed_lattice_field.to_normed_lattice_add_comm_group  (α : Type*)
  [normed_lattice_field α] : normed_lattice_add_comm_group α :=
⟨λ _ _ h c, add_le_add_left h c, normed_lattice_field.solid⟩

and then normed_lattice_field (including ℚ and ℝ) inherits all the lemmas for normed_lattice_add_comm_group.

[Yaël Dillies]

Also dare I mention that solid is a poor name for this property?

[Xavier Roblot]

And it is suited that the right fields for dealing with ℤ-lattices are called normed_lattice_field :wink:

[Xavier Roblot]

Yaël Dillies said:

Also dare I mention that solid is a poor name for this property?

You will have to ask the author of the file analysis.normed.order.lattice: @Christopher Hoskin

[Kevin Buzzard]

There are solid modules in condensed mathematics which are unrelated to this concept

[Alex J. Best]

I was also thinking about this in relation to your PR @Xavier Roblot. I think one way of stating this issue is that currently one could take a totally real number field (like $\mathbf Q (\sqrt 2)$) and make an instance of Lt using one embedding and the norm using another embedding to R. I was wondering if the property x < y < z \implies || x - y ||< || x - z || was a good fix?

[Alex J. Best]

Maybe that is the same as yours?

[Kevin Buzzard]

x<y<z implies 0<y-x<z-x. Does abs satisfy x > 0 -> abs x = x?

[Alex J. Best]

I hope so! They should be the same after all (and Xavier's is simpler)

[Christopher Hoskin]

Yaël Dillies said:

Also dare I mention that solid is a poor name for this property?

In general mathematicians seem poor at coming up with imaginative names for properties.

I didn't invent this term, I picked it up from Wikipedia https://en.wikipedia.org/wiki/Normed_vector_lattice

I've seen the definition of a "solid subset" in several sources in the literature. @Yaël Dillies is your objection to the use of soild to describe "the unit ball is solid" or do you object to the use of "solid" in "solid subset" too?

[Yaël Dillies]

I would much expect "solid" to refer to (three dimensional) polyhedra.

[Kevin Buzzard]

Heh, so there's three distinct meanings in the literature already :-)

[Christopher Hoskin]

According to Zaanen, Lectures on Riesz space, the French use the term "épais" (which I think translates as "thick") and the Russians use (a term which translates as) "semi-normal".

[Xavier Roblot]

Alex J. Best said:

I hope so! They should be the same after all (and Xavier's is simpler)

Yes, I have decided to go ahead with this solution #18554

[Alex J. Best]

Great. I must say I'm not a huge fan of the name solid, I'm sure its standard in a part of the literature I don't know, but if we are now using this for the property of |a| \le |b| \implies ||a|| \le ||b|| on the rationals I think adding an alias norm_le_norm_of_abs_le_abs would be worthwhile.

[Eric Wieser]

Does has_isometric_smul α real have the same effect as what you need here?

[Eric Wieser]

Eric Wieser said:

But then I guess you're stuck

I think the missing piece is a typeclass that says algebra_map R A is monotone; which is true in lots of places around nat / int / rat

[Eric Wieser]

import analysis.normed.order.basic
import algebra.order.module

variables {K : Type*} [normed_linear_ordered_field K] [normed_algebra K ℝ]

example (x : K) (h : |x| ≤ 1) : ‖x‖ ≤ 1 :=
begin
  rw ←norm_algebra_map' ℝ (_ : K),
  rw real.norm_eq_abs,
  rw algebra.algebra_map_eq_smul_one,
  conv_rhs {rw ←one_smul K (1 : ℝ) },
  rw abs_le at ⊢ h,
  cases h, split,
  rw ←neg_smul,

end

is close

[Eric Wieser]

Any ideas, @Yaël Dillies?

[Yaël Dillies]

(Oh wow I was about to open a PR to add has_isometric_smul. No idea it existed)

[Yaël Dillies]

I have a hint that docs#has_ordered_smul could help here.

[Yaël Dillies]

I was about to say that we should define a normed_ordered_algebra mixin extending normed_algebra, but that would prevent us from being able to talk about non-unital stuff.

[Kevin Buzzard]

So what's an example of a normed ordered ring-without-a-unit? I mean, at some point you just have to be pragmatic, right?

[Johan Commelin]

Probably stuff like the ideal $2\mathbb{Z}$

[Yaël Dillies]

Yeah yeah, but also we might as well make do with existing pieces.

[Eric Wieser]

Johan Commelin said:

Probably stuff like the ideal $2\mathbb{Z}$

Does that have a non_unital_ring structure today?

[Johan Commelin]

Probably not.

[Johan Commelin]

I don't think we should add it before the alghier refactor in ml4.

[Johan Commelin]

Non-unital rings are causing enough problems in the current setup.