EEhil

[fl]

After spending some time trying to understand EEhil's definition, I think it's nice

(except for NN0 instead of NN) but if you hope that a non-mathematically-inclined brain

deciphers that comfortably, you are dreaming.

--

FL

[Thierry Arnoux]

Hi Frédéric,

We could do two things to make the definition easier to understand:

One thing would be to provide more explanations in the comment for df-ehl, like, explaining that this defines the Euclidean spaces as direct sums of identical copies the field of the real numbers, and pointing to other definitions (where more explanations can also be provided if needed), or pointing to an appropriate reference in the littérature.

Another thing would be to expand the different components of the structure, showing what is the “base”, the group addition operation, etc. are what one would expect.

Maybe we could also note that the matrix ring is defined in a similar way.

About the starting index, I understand your concern. I started with index 0 because but I believe the dimension 0 is an interesting case. This is not Scott Fenton’s convention (he starts at 1 in df-ee), but I think maybe Scott’s definition can be extended without causing too much “damage” (i.e. proofs to be rewritten). I’ll give it a try if I find time to.
BR,
_
Thierry

[fl]

Hi Thierry,

I actually think we should reference the names of the variables, give their real type when V has been used (for example for i in the case of df-rrx, 

or for r and i in the case of df-frlm, or for s and r in the case of df-dsmm), and finally delete the definitions that are useless (this is the case of df-rrx I think). 

Using a direct sum when the number of dimensions is finite seems to me to add unnecessary complexity (or it should be said in the commentary 

that in this case the finite support is useless and that df-dsmm is only used for the sake of not having an additional definition). 

It is also necessary to explain in what order this is done. I think that adding the sequence of actions is very enlightening: 

1) building the RR field 

2) building the module from the field 

3) building a function  indexed by naturals (𝑖 × { {(ringLMod'𝑟)}) 

4) making the tuples of the base set of the product and making the pointwise operations,the distance, topology and Hermitian form.

5) and finally making and adding the norm.

It's also not bad to add at *which level* of definition the elements are built and add to the structure, for example 

Hermitian form at the df-prds level but the norm at the tiCHil level.

By the way, I wondered if all your metric and topological structures are correctly connected.

And we have to comment on df-prds. In particular, explain that this operator only looks so strange because his real purpose is to overload a symbol.

-- 

FL

[fl]

In the commentary of

"11.1.1  Direct sum of left modules"

the definition of wikipedia and that of Lang amount to the same. We can settle for Lang's.

Let's favor the book. It looks better.

--
FL

[Thierry Arnoux]

Hi Frédéric,

I agree more explanations would help, I also needed time myself to get
familiar with those definitions.

Would you mind proposing the additional text for the comments to those
definitions?

I can then help doing the actual changes in set.mm if needed.

BR,
_
Thierry

[fl]

 

Would you mind proposing the additional text for the comments to those
definitions?

I wouldn't mind.

Will you keep on with the direct sum or will you use the product Xs directly? The direct product would
remove one layer. It woulld be less complex.

I cite wilipedia:

"In the case of two summands, or any finite number of summands, the direct sum is the same as the direct product."

https://en.wikipedia.org/wiki/Direct_sum

I can then help doing the actual changes in set.mm if needed.

I will send them to you.

--
FL

[Benoit]

Of course, you can define a (finite-dimensional) Euclidean space as a direct sum or a direct product since, they are equal for a finite number of summands/factors.  I think the present definition is better, since in the infinite case, you can define an inner product on a direct sum, but not on a direct product.

As for the unicode symbol for the direct sum of copies of \R, I would use Mario's suggestion from a previous thread, i.e. R^() instead of R^.  This would free up the symbol R^ to be used for the direct product.

Benoit

[fl]

Of course, you can define a (finite-dimensional) Euclidean space as a direct sum or a direct product since, they are equal for a finite number of summands/factors.  I think the present definition is better, since in the infinite case, you can define an inner product on a direct sum, but not on a direct product.

OK.I hadn't seen that that way.RR^ is for a finite or non-finite  number of dimensions. And EEhil is for the finite case. OK.
 
--
FL

[fl]

My dear Thierry,

I think you should adapt your EE (and RR^) definition so that the topology and uniform structure are generated from the distance. Currently and unless I'm mistaken (the definitions are sometimes a little confusing) I think they are independent. It will allow to speak of RRhil as a Hilbert space with a standard norm defined from the inner product, a standard distance defined from the norm, a uniform structure defined from the distance, and a standard topology defined from the uniform structure.

(The promised comments are coming in. The weather has been a little hot so far.)

-- 

FL

[fl]

The former message must be read this way. (Modifications marked by two stars.)

I think you should adapt your *EEhil* (and RR^) definition so that the topology and uniform structure are generated from the distance. Currently and unless I'm mistaken (the definitions are sometimes a little confusing) I think they are independent. It will allow to speak of EEhil as a Hilbert space with a standard norm defined from the inner product, a standard distance defined from the norm, a uniform structure defined from the distance, and a standard topology defined from the uniform structure.

[Thierry Arnoux]

Hi Frédéric,

The definitions of RR^ (and by extension EEhil) use toCHil, which itself uses toNrmGrp (~ df-tng).

The toNrmGrp operation ensures that the topology and metric components are set according to the distance. 

The norm is always defined according to the distance (see ~ df-nm)，so it will be compatible with the topology and metric.

As far as the uniform structure is concerned, toNrmGrp does not set it. If we want it to be set correctly (so that the resulting space is a uniform space), we would need to modify toNrmGrp to also set the uniform structure to the uniform structure generated by the structure’s metric. This is provided by the “ metUnif “ function (see ~ df-metu).

So... here is the whole process again:

* df-cnfld defines the complex addition and multiplication operation.

* df-refld restricts it to the field of the real numbers 

* df-rgmod / df-sra assigns the field of reals as its own scalar field, and the inner product as the real multiplication, so we obtain the real numbers as a left module,

* df-frlm / df-dsmm (df-prds) defines an inner product on the direct sum (product) structure, so that we get the inner product as the sum of (inner) products of each components, pairwise. This is the scalar product.

* df-tch then defines a norm function as the square root of the inner (scalar) product of a vector with itself,

* df-tng uses that norm to populate the distance (which is a metric) and topology. It may be enhanced to also populate the uniform structure defined from the same distance. Is there any interesting application for that?

* finally, df-ehl restricts the whole to index sets of the form ( 1 ... N )

It’s indeed a complicated construct, but it is following the path you describe. I believe all bits and pieces are there for a Hilbert space. I’ll try to continue on that path!

_

Thierry

Le 2 juil. 2019 à 02:07, 'fl' via Metamath <meta...@googlegroups.com> a écrit :

The former message must be read this way. (Modifications marked by two stars.)

I think you should adapt your *EEhil* (and RR^) definition so that the topology and uniform structure are generated from the distance. Currently and unless I'm mistaken (the definitions are sometimes a little confusing) I think they are independent. It will allow to speak of EEhil as a Hilbert space with a standard norm defined from the inner product, a standard distance defined from the norm, a uniform structure defined from the distance, and a standard topology defined from the uniform structure.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/0eed8f5b-a63f-421d-a1d2-9e19e85eb2a6%40googlegroups.com.

[fl]

Hi Thierry,

I missed the fact that the topology is defined from the distance by toNrmGrp.

I still think that the order of definitions should be:

(1) The distance is defined from the norm. (2) The uniform structure is defined from the distance.

(3) The topology is defined from the uniform structure.

We should adopt this order for all spaces where there are combined norms metrics, uniform structures, topologies, regardless of the level of generality of the spaces  for the sake of homogeneity.

It bothers me that the norm is defined by distance. (Even if in this case, this is possible. But only because there is a zero.)

There may be a shortcut for topologies defined in terms of distances by bypassing uniform structures.

Because there is still a problem of generality.  The least general, the most particular space

here is the normed space, then the metric space then the space with a uniform structure then the

space with a topology.

There are spaces where there are distances and no norms.

There are spaces where the natural concept is the norm. The distance is derived.

Hoping to have been able to convey what I wanted to say and I  havn't made any mistakes.

(I also notice, in df-nm, that putting dist in the middle of the expression (x(dist`w)(0g` w)) can be difficult to understand when you are not a distinguished expert in metamath. But it's not your definition.)

--

FL

[fl]

Some fixes.

Hi Thierry,

I missed the fact that the topology is defined from the distance by toNrmGrp.

I still think that the order of definitions should be:

(1) The distance is defined from the norm. (2) The uniform structure is defined from the distance.

(3) The topology is defined from the uniform structure.

We should adopt this order for all spaces where there are combined norms, metrics, uniform structures, topologies, regardless of the level of generality of the spaces,  for the sake of homogeneity.

*(a) It bothers me that the norm is defined by distance. (Even if in this case, this is possible. But only because there is a zero.) *

*(b) There may be a shortcut for topologies defined in terms of distances by bypassing uniform structures. But it bothers me too. *

*The reason  is that there is a problem of generality in (a) and (b).*

*We should adopt a homogeneous way of treating all spaces and not rely on properties specific to a type of space. This does not mean that we cannot then prove the derivations specific to a specific space. If we adopt a homogeneous and standard way of defining all these spaces, it will be easier to memorize and manage. We will not have to check the details of the definitions for each structure.*

--

FL