Transformation of PART 18 COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)

[avekens]

The definitions and theorems in Part 18 COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED) should be transferred to be based on extensible stuctures (if not already available) and integrated into PART 12 BASIC TOPOLOGY. Afterwards, this deprecated part can/should be removed, including the deprecated definitions/theorems of the former Part 18 ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS (DEPRECATED), which were only kept because they are used in the current PART 18 (see issue #1432).

Tasks:

• [x] Transformation of section 18.2 Complex vector spaces
• [x] Transformation of section 18.3 Normed complex vector spaces I (subsections 18.3.1 and 18.3.2)
• [x] Transformation of section 18.3 Normed complex vector spaces II (subsections 18.3.3 to 18.3.5)
• [ ] Transformation of section 18.4 Operators on complex vector spaces
• [ ] Transformation of section 18.5 Inner product (pre-Hilbert) spaces
• [ ] Transformation of section 18.6 Complex Banach spaces
• [ ] Transformation of section 18.7 Complex Hilbert spaces
• [ ] Deletion of PART 18 (maybe some definitions/theorems will still be used in mathhboxes - these definitions/theorems must be moved into the corresponding mathboxes)

[avekens]

With PR #2226, the first task is done. A summary of the results is provided in the attached PDF document: Deprecated_Part_18_Complex_Topological_Vector_Spaces_2.pdf Many theorems had already a corresponding version in main set.mm (first column), the missing theorems were added by me (second column). There are several deprecated theorems which are currently not used (third column): @nmegill @digama0 can these theorems (and the not used theorems in the remaining sections of PART 18) be deleted immediately?

I started already to work on the second task (Transformation of section 18.3 Normed complex vector spaces). It will be finished soon (there is only a little number of theorems about the norm, most of the deprecated theorems are about arbitrary groups and vector spaces...)

[benjub]

@avekens : Can you confirm that Section 18 is only about vector spaces with scalar field CC ? Or is a subfield of CC allowed ? In particular, are complex Banach and Hilbert spaces necessarily over CC, or is RR allowed ?

I'm asking in order to see whether the changes mentioned in #2230:

complex vector space --> subcomplex vector space complex left module --> subcomplex module

may interfer with your work on Section 18.

[avekens]

@benjub Although part 18 is about vector spaces with scalar field CC, my revisions will be about vector spaces (or modules) over subfields of CC. If you only plan to modify the comments, I think there will be no (or only little) problems. I can adapt the comments of my revised theorems accordingly. If you plan to change labels (e.g. clm -> scm for complex (left) modules), then we have to be more careful. I think I will wait with my changes until you finished your work.

[benjub]

Thanks @avekens. I was thinking only comments, but it's true that some labels may have to be changed too... Don't wait for me: when I'm ready to do the change, I'll give you a heads up so that we don't overlap.

[avekens]

With PR #2235, the second task is done. A summary of the results is provided in the attached PDF document: Deprecated_Part_18_Complex_Topological_Vector_Spaces_3.pdf

Again, many theorems had already a corresponding version in main set.mm (first column), the missing theorems were added by me (second column). There are several deprecated theorems which are currently not used (third column).

@benjub I stop working for this issue for now, so you can perform your revisions about renaming.

[benjub]

@avekens Reading at the changes, I ran into df-phl. Is it possible to write in plain English, in the comment of df-phl, what a "generalized pre-Hilbert (inner product) space" is ? In particular, in what sense is it "generalized" ? If I'm not mistaken, this could be:

Define the class of all pre-Hilbert spaces (inner product spaces) over arbitrary fields with involution.

[avekens]

@benjub Yes, I think the definition you propose is more adequate. Maybe you can add how a pre-Hilber space is usually defined, namely over the real or complex numbers, e.g. in [Roman] p. 205: "A real (or complex) vector space V, together with an inner product, is called a real (or complex) inner product space".

[benjub]

@avekens : will do

[avekens]

With PR #2255, the task 3 is done, completing the revision of section 18.3. A summary of the results of tasks 2 and 3 is provided in the attached PDF document: Deprecated_Part_18_Complex_Topological_Vector_Spaces_3.pdf

Again, many theorems had already a corresponding version in main set.mm (first column), the missing theorems were added by me (second column). There are several deprecated theorems which are currently not used (third column).

In a next step, I will remove the theorems of Part 18 which are not used in any proof.

[avekens]

I continued to analyse part 18 with the goal to replace/remove some of its theorems (because they are covered already by not deprecated parts), but I found out that many of the theorems of part 18 are used in part 19, which is a topic by itself (Complex Hilbert Space explorer, having an own web page https://us.metamath.org/mpeuni/mmhil.html).

From my point of view, part 18 cannot be removed/reduced unless part 19 is completely revised (not to depend on part 18 anymore). This will be a lot of work I assume! I will open a separate issue for that, and the transformation of part 18 should be paused until the revision of part 19 is finished.

[david-a-wheeler]

@avekens - makes sense, in fact, I'm 0% surprised :-).