Zulip Chat Archive

Stream: new members

Topic: 'has_norm' has already been declared


Sebastien Gouezel (Sep 15 2022 at 07:28):

Note that this instance is bad, since there is no way Lean can guess which function f it should use to define the norm: if there are two functions around, it would give two different norms...

Notification Bot (Sep 15 2022 at 07:28):

Xavier Roblot has marked this topic as unresolved.

Damiano Testa (Sep 15 2022 at 07:31):

Continuing on Sebastien's remark: if this instance is not the consequence of minimizing, then also the linter is very unhappy with it.

Damiano Testa (Sep 15 2022 at 07:33):

From the linter message, it seems that Lean would not infer any instance, rather than produce one for each function K → ℝ. It also does not like that you did not use field K and thinks that the instance priorities are wrong!

Lean is very unhappy with this instance! :lol:

Xavier Roblot (Sep 15 2022 at 07:34):

Sebastien Gouezel said:

Note that this instance is bad, since there is no way Lean can guess which function f it should use to define the norm: if there are two functions around, it would give two different norms...

Yes, that is my next problem. What should I do in this case? Consider the following #mwe

import analysis.normed.field.basic

namespace mwe

variables {K A : Type*} [field K] [normed_division_ring A] (φ : K →+* A)

def place : K   := (norm : A  )  φ

instance : has_dist K := λ x y, place φ (x - y)⟩

As you said, that is not the right way to proceed since φ is implicit. So what is the right solution? I want to study embeddings of number field and I want to be able to say, for example, that an complex embedding defines a norm on K. I tried to do everything using def instead of instance but got into trouble (maybe I am supposed to try harder).

Johan Commelin (Sep 15 2022 at 07:36):

Do you want to study multiple embeddings at the same time? Or do you first want to fix an embedding, and study that on its own?

Johan Commelin (Sep 15 2022 at 07:37):

In my experience, most of the time we are happy to work with one embedding. And occasionally we have formulas that quantify over all embeddings.

Xavier Roblot (Sep 15 2022 at 07:38):

Johan Commelin said:

Do you want to study multiple embeddings at the same time? Or do you first want to fix an embedding, and study that on its own?

I'll probably need to consider several at same time at some point. For example, to see if they defined the same distance,

Johan Commelin (Sep 15 2022 at 07:39):

Right, but maybe you first want to build an API of x00 lines that focuses on 1 embedding.

Johan Commelin (Sep 15 2022 at 07:39):

In that case, I would assume that K is a normed field, and A is a normed K-algebra.

Johan Commelin (Sep 15 2022 at 07:40):

Then, once you start varying the embedding, you have to explain once and for all how you can get the norm on K and the normed K-algebra structure on A from the embedding and the norm on A.

Damiano Testa (Sep 15 2022 at 07:40):

Maybe you could make the instance on the function itself?

Damiano Testa (Sep 15 2022 at 07:41):

After all, a field embedding is... the embedding!

Johan Commelin (Sep 15 2022 at 07:41):

But that diverges from our mental model and the way it is written on paper.

Johan Commelin (Sep 15 2022 at 07:42):

I claim we switch back and forth between two points of view. And so we should have both points of view in Lean as well.

Johan Commelin (Sep 15 2022 at 07:42):

One where you have algebras and instances. And one where you have multiple explicit embeddings, and so you don't use instances.

Damiano Testa (Sep 15 2022 at 07:43):

Ok, I was going to argue that the paper version is way too sloppy, but I agree that both points of view should exist!

Xavier Roblot (Sep 15 2022 at 07:52):

Ok. Can you give me some pointers on how to do it for one embedding without using “bad” instances? Maybe some part of ‘’’mathlib’’’ where a similar construction is used.

Johan Commelin (Sep 15 2022 at 07:53):

My point is that in the "single embedding case" you should just assume everything you want.

Johan Commelin (Sep 15 2022 at 07:53):

So do not start with f : K \to+* A but with algebra K A. And assume that everything is compatible with the norms.

Johan Commelin (Sep 15 2022 at 07:53):

In particular, assume that the norm on K already exists.

Johan Commelin (Sep 15 2022 at 07:55):

variables (K A : Type*) [normed_field K] [normed_division_ring A] [normed_algebra K A]

Johan Commelin (Sep 15 2022 at 07:55):

Something like that, I guess.

Yaël Dillies (Sep 15 2022 at 07:58):

Another is to define a type synonym for each φ : K →+* A. Something like

def xavier_synonym (φ : K →+* A) := K

def place : K   := (norm : A  )  φ

instance : has_dist (xavier_synonym φ)  := λ x y, place φ (x - y)⟩

But indeed Johan's approach is most likely the better one.

Johan Commelin (Sep 15 2022 at 07:59):

Those type synonyms are probably needed for the other point of view.

Xavier Roblot (Sep 15 2022 at 08:04):

Ok. So I’ll do as Johann suggested and I guess then I add a theorem stating that an embedding gives the right properties on K and A.

Xavier Roblot (Sep 15 2022 at 10:23):

Well, I am sorry but I really do not see how to connect the dots. As Johann suggested I can do an API to work with normed_algebra indeed. But I still need to prove at some point that given an embedding φ : K →+* A, I get normed_field K and normed_algebra K A. Showing that we have normed_field K is straightforward, but then to show normed_algebra K A, I need to know that I already have normed_field K (that I can find a way to do although I am not sure it is correct) but more importantly I need to know what is the definition of the norm on K and I do not know how to pass that info without using instance

Xavier Roblot (Sep 15 2022 at 10:23):

import analysis.normed_space.basic

open function

variables {A : Type*} [normed_field A]

def normed_field_at (K : Type*) [field K] (φ : K →+* A) : normed_field K :=
{ to_metric_space := {
    dist := λ x y, (norm  φ) (x - y),
    dist_self := by simp only [dist, sub_self, comp_app, map_zero, norm_zero, forall_const],
    dist_comm := by simp only [dist, norm_sub_rev, comp_app, map_sub, eq_self_iff_true,
      forall_const],
    dist_triangle :=
    begin
      intros x y z,
      simpa [dist, comp_app, ring_hom.map_sub, sub_eq_add_neg, add_assoc]
        using norm_add_le (φ x - φ y) (φ y - φ z),
    end,
    eq_of_dist_eq_zero := by simpa [dist, comp_app, norm_eq_zero, ring_hom.map_sub, sub_eq_zero]
      using (ring_hom.injective φ), },
  norm := norm  φ,
  dist_eq := λ _ _, rfl,
  norm_mul' := λ _ _, by simp_rw [dist, comp_app, ring_hom.map_mul, norm_mul], }

def normed_algebra_at (K : Type*) [field K] (φ : K →+* A) :
@normed_algebra K A (normed_field_at K φ) _ :=
{ to_algebra := φ.to_algebra,
  norm_smul_le :=
  begin
    intros r x,
    sorry,
  end,
}

Yaël Dillies (Sep 15 2022 at 10:26):

Actually what Johan suggested is that the "one hom API" already exists: It is the normed_algebra API.

Eric Wieser (Sep 15 2022 at 13:36):

docs#norm_algebra_map' is the statement that the norm respects the embedding

Xavier Roblot (Sep 15 2022 at 13:44):

Well, I am still not quite sure I see how I am going to make thinks work. I'll have to think about it some more. Thanks for the help.


Last updated: Dec 20 2023 at 11:08 UTC