## 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_ring.to_normed_group.{u_1} 𝕜 (@normed_field.to_normed_ring.{u_1} 𝕜 _inst_4)))
(@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_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, ...

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: May 08 2021 at 05:14 UTC