Zulip Chat Archive

Stream: new members

Topic: Dependency problem

Heather Macbeth (May 15 2020 at 19:26):

I made a new branch, modifying normed_space.basic (see discussions 1 2), which broke normed_space.operator_norm. I can't figure out why, and wondered if someone would mind diagnosing it for me.

Heather Macbeth (May 15 2020 at 19:26):

The first error is, "term f has type š•œ ā†’ā‚—[š•œ] E : Type (max u_1 u_2) but is expected to have type ?m_2 ā†’ā‚—[?m_1] ?m_3 : Type (max ? ?)".

Johan Commelin (May 15 2020 at 19:29):

That looks ugly )-; [The error, I mean]

Kevin Buzzard (May 15 2020 at 19:31):

  type mismatch at application
    @linear_map.mk_continuous.{?l_1 ?l_2 ?l_3} ?m_4 ?m_5 ?m_6 ?m_7 ?m_8 ?m_9 ?m_10 ?m_11 f
  term
    f
  has type
    @linear_map.{u_1 u_1 u_2} š•œ š•œ E
      (@normed_ring.to_ring.{u_1} š•œ (@normed_field.to_normed_ring.{u_1} š•œ _inst_4))
      (@normed_group.to_add_comm_group.{u_1} š•œ
         (@normed_ring.to_normed_group.{u_1} š•œ (@normed_field.to_normed_ring.{u_1} š•œ _inst_4)))
      (@normed_group.to_add_comm_group.{u_2} E _inst_1)
      (@field.to_vector_space.{u_1} š•œ (@normed_field.to_field.{u_1} š•œ _inst_4))
      (@normed_space.to_module.{u_1 u_2} š•œ E _inst_4 _inst_1 _inst_5) : Type (max u_1 u_2)
  but is expected to have type
    @linear_map.{?l_1 ?l_2 ?l_3} ?m_4 ?m_5 ?m_6
      (@normed_ring.to_ring.{?l_1} ?m_4 (@normed_field.to_normed_ring.{?l_1} ?m_4 ?m_7))
      (@normed_group.to_add_comm_group.{?l_2} ?m_5 ?m_8)
      (@normed_group.to_add_comm_group.{?l_3} ?m_6 ?m_9)
      (@normed_space.to_module.{?l_1 ?l_2} ?m_4 ?m_5 ?m_7 ?m_8 ?m_10)
      (@normed_space.to_module.{?l_1 ?l_3} ?m_4 ?m_6 ?m_7 ?m_9 ?m_11) : Type (max ?l_1 ?l_2)

Is it a diamond?

Johan Commelin (May 15 2020 at 19:31):

@Heather Macbeth (Btw, I think these questions could go in "general")
https://github.com/leanprover-community/mathlib/commit/0f96de153ffb79f9c3cb147f6c206e67cc09aa49#diff-fc5c89c1d4551a23597885d48b6ed4e5R705
this looks like an instance loop

Johan Commelin (May 15 2020 at 19:31):

It should probably be a def instead of an instance

Heather Macbeth (May 15 2020 at 19:33):

I'll try that! Of of_normed_module or to_normed_module, which should be the instance and which the def?

Johan Commelin (May 15 2020 at 19:34):

The one that makes your life easier when defining a new normed_space

Johan Commelin (May 15 2020 at 19:34):

So of_

Mario Carneiro (May 15 2020 at 19:35):

I think of_ should be the def

Mario Carneiro (May 15 2020 at 19:35):

I'm confused, are these two classes the same?

Johan Commelin (May 15 2020 at 19:36):

If at some point someone encounters a normed_module over a field, they will have to work a little bit to make it a normed_space. But the rest of the time, we want lemmas about normed_modules to automatically apply to normed_spaces.

Heather Macbeth (May 15 2020 at 19:36):

There is a typo in my documentation.

Mario Carneiro (May 15 2020 at 19:36):

or does this equivalence only hold under certain conditions

Heather Macbeth (May 15 2020 at 19:36):

It should read, "Over a normed field, āˆ„c ā€¢ xāˆ„ ā‰¤ āˆ„cāˆ„ āˆ„xāˆ„ automatically implies āˆ„c ā€¢ xāˆ„ = āˆ„cāˆ„ āˆ„xāˆ„"

Heather Macbeth (May 15 2020 at 19:36):

The equivalence holds when the ring is a field

Mario Carneiro (May 15 2020 at 19:37):

In general, if A -> B and C -> B -> A then B should be the parent and A -> B an instance

Johan Commelin (May 15 2020 at 19:37):

@Heather Macbeth We could also decide to do away with normed_module and just define normed_space over general rings, right?

Heather Macbeth (May 15 2020 at 19:37):

normed_module is brand new, I just made it.

Heather Macbeth (May 15 2020 at 19:38):

(Was going to open a discussion topic later.)

Johan Commelin (May 15 2020 at 19:38):

And then this:
Heather Macbeth said:

It should read, "Over a normed field, āˆ„c ā€¢ xāˆ„ ā‰¤ āˆ„cāˆ„ āˆ„xāˆ„ automatically implies āˆ„c ā€¢ xāˆ„ = āˆ„cāˆ„ āˆ„xāˆ„"

just becomes a lemma about normed spaces, if the base ring happens to be a field.

Johan Commelin (May 15 2020 at 19:38):

Heather Macbeth said:

normed_module is brand new, I just made it.

Sure, so I should have said: change the def or normed_space to work for general rings.

Heather Macbeth (May 15 2020 at 19:38):

I think normed_space means normed_vector_space

Johan Commelin (May 15 2020 at 19:39):

We decided to have both module and vector_space in mathlib, but it creates extra technical nuissance. The only reason we keep it is psychological/pedagogical.

Johan Commelin (May 15 2020 at 19:40):

You don't want a library without vector_space, but renaming module to vector_space also seems dishonest.

Heather Macbeth (May 15 2020 at 19:40):

I think consistency is good -- what is done in the general category should also be done in the normed category, etc.

Johan Commelin (May 15 2020 at 19:40):

But in the normed category, you won't have beginning users that don't know that modules and vector spaces are just the same thing.

Johan Commelin (May 15 2020 at 19:43):

Unifying the two concepts would allow you to get rid of this instance loops altogether. But keeping it for the sake of consistency isn't a big problem either. Upgrading a normed_module over a field to a normed_space is just a one-liner in a proof.

Heather Macbeth (May 15 2020 at 19:43):

I'm not sure it would be wise to go down the path of Banach modules, Hilbert modules, ...

Heather Macbeth (May 15 2020 at 19:43):

Sobolev modules

Heather Macbeth (May 15 2020 at 19:43):

The module of measures of bounded variation

Sebastien Gouezel (May 15 2020 at 19:59):

I think vector_space is just an abbreviation for module. We could have normed_module, and then normed_space as an abbreviation of normed_module.

Johan Commelin (May 15 2020 at 20:00):

But "just an abbreviation" is not good enough for type class inference.

Johan Commelin (May 15 2020 at 20:00):

I wish the pretty printer could do type class inference :oops: :head_bandage:

Heather Macbeth (May 15 2020 at 20:01):

Let me add that I made up these "normed modules" this morning because I had some instances in mind

Johan Commelin (May 15 2020 at 20:01):

Then everything would be a module, but print as vector_space if the pretty printer can infer that the base ring is a field.

Heather Macbeth (May 15 2020 at 20:01):

(I was going to start a thread discussing it, but here will do.)

Heather Macbeth (May 15 2020 at 20:02):

Notably: if E is a normed k-space then C(a, E) is a C(a, k)-module

Heather Macbeth (May 15 2020 at 20:04):

In that case, one has norm_smul_le rather than norm_smul, i.e., āˆ„c ā€¢ xāˆ„ ā‰¤ āˆ„cāˆ„ āˆ„xāˆ„ without equality

Heather Macbeth (May 15 2020 at 20:05):

So if normed_module becomes the basic object, it should still be with the norm_smul_le axiom rather than the norm_smul axiom, which is only equivalent over fields.

Johan Commelin (May 15 2020 at 20:07):

Sure. And norm_smul would be a lemma with the assumption [normed_field k]

Heather Macbeth (May 15 2020 at 20:32):

Hmm. Won't this break all the existing instances of normed spaces in the library? They are all constructed by checking the axiom norm_smul.

Johan Commelin (May 16 2020 at 04:15):

Yup, that's right. So all their constructions should be prepended with normed_space.mk' or some other name that provided a second constructor.
@Heather Macbeth You might be shocked if you read the defn of metric_space in mathlib. It hardcodes a metric + a topology + proof that they are compatible.
But of course nobody creates metric spaces like that, so there is a 2nd constructor that only asks for a metric.

Johan Commelin (May 16 2020 at 04:17):

The reason for this design is: in the case of the product metric/topology, you don't use the 2nd constructor, but fill in all fields by hand. And now the product metric induces a topology that is definitionally the product topology! :tada:

Yury G. Kudryashov (May 16 2020 at 08:44):

so there is a 2nd constructor that only asks for a metric.

AFAIR, metric_space is done by using := and . types, not by a second constructor.

Last updated: Dec 20 2023 at 11:08 UTC