'has_norm' has already been declared

Stream: new members

[Sebastien Gouezel]

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]

Xavier Roblot has marked this topic as unresolved.

[Damiano Testa]

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]

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]

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]

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]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

Maybe you could make the instance on the function itself?

[Damiano Testa]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Damiano Testa]

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]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

Something like that, I guess.

[Yaël Dillies]

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]

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

[Xavier Roblot]

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]

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]

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]

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

[Eric Wieser]

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

[Xavier Roblot]

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.