search

metamath / set.mm

Metamath source file for logic and set theory
Other
246 stars 88 forks source link

Unicode symbols for CHil and friends #947

Closed benjub closed 2 years ago

benjub commented 5 years ago
nmegill commented 5 years ago
  • May I change unicode symbols (i.e. althtmldef) to make the "C" blackboard bold in CMod, CVec, CPreHil, toCHil, CHil, CPreHilOLD, CBan, CHilOLD, and others that I may have forgotten?

I'm not sure if I like that - I think it would look weird and might even be confusing (e.g. the CC and Mod in CMod might look like two juxtaposed symbols that someone forgot to put space between). If anything, making the CC a subscript might be better. Maybe someone else has an opinion.

However, the whole section containing these is deprecated and will be deleted someday. So it will be wasted effort. This was all done before the extensible structure builder and some definitions ended up awkward and inflexible. We are keeping primarily to use as a possible reference for the structured and possibly more general versions. Maybe that time has even passed or will soon.

  • May I change the tokens pi to _pi om to _om tau to _tau iota to iota iota to iota (without the spaces: it is to avoid markdown) in order to avoid confusion with wff metavariables (and in the case of pi and om, to make the non-underscored versions usable as wff metavariables), and others that I may have forgotten?

OK except iota, see below. Also, we have been using non-italic for Roman constants e.g. _e and _i, and probably should use non-italic (non-slanted) for Greek constants. I have seen non-italic letters for constants used more often in recent literature, and I think I've even seen a non-italic pi used for 3.14.

I don't think we should add them as wff variables until there's an actual need. Perhaps that is what you meant.

However, the iota and iota are actually upside-down iota. I'm not sure what to do about those. LaTeX calls it \riota for "rotated iota", but we use riota in labels to mean "restricted iota" i.e. iota We've been using a dot suffix for rotated letters like A. and E. I wanted to use F. for F/ (not free) but F. was already taken by "false". And "false" is really a rotated T, not an F. :) Maybe leave the iotas alone until we figure out what's best. I don't think we'll be using it as a wff variable any time soon. BTW some of the historical changes are in a little table in the 3-Oct-2010 entry on the mmrecent.html page.

digama0 commented 5 years ago
  • May I change unicode symbols (i.e. althtmldef) to make the "C" blackboard bold in CMod, CVec, CPreHil, toCHil, CHil, CPreHilOLD, CBan, CHilOLD, and others that I may have forgotten?

I'm not sure if I like that - I think it would look weird and might even be confusing (e.g. the CC and Mod in CMod might look like two juxtaposed symbols that someone forgot to put space between). If anything, making the CC a subscript might be better. Maybe someone else has an opinion.

How about {\Bbb C}-Mod? It's pretty common to denote complex vector spaces like this, but possibly the meaning is too specific to this case (i.e. CMod is about modules over a subset of CC, not necessarily CC itself.)

However, the whole section containing these is deprecated and will be deleted someday. So it will be wasted effort. This was all done before the extensible structure builder and some definitions ended up awkward and inflexible. We are keeping primarily to use as a possible reference for the structured and possibly more general versions. Maybe that time has even passed or will soon.

I don't think df-clm (CMod) is deprecated, unless I missed something. It uses extensible structures. Possibly you are thinking of the Hilbert space explorer stuff? I think all the definitions for replacing the HSE with a set.mm version are in place, but most of the theorems haven't been redone.

nmegill commented 5 years ago

How about {\Bbb C}-Mod? It's pretty common to denote complex vector spaces like this, but possibly the meaning is too specific to this case (i.e. CMod is about modules over a subset of CC, not necessarily CC itself.)

I don't have an objection, but I'm not familiar with the literature convention on this.

I don't think df-clm (CMod) is deprecated, unless I missed something. It uses extensible structures. Possibly you are thinking of the Hilbert space explorer stuff? I think all the definitions for replacing the HSE with a set.mm version are in place, but most of the theorems haven't been redone.

My mistake, What I meant is everything in Parts 18, 19, and 20 of the Theorem List contents, which includes some renamed to OLD like CHilOLD and others not renamed like CBan, is deprecated. The ones outside those Parts are (probably) not deprecated.

benjub commented 5 years ago
benjub commented 5 years ago

@digama0 Calling the elements of CMod complex modules is at best dangerous, since a complex module is by definition of module over \C. What do you think of calling them "subcomplex modules" instead ?

benjub commented 5 years ago

Done in #972 .

@nmegill, @digama0 It turns out that CMod, CVec, CPreHil, CHil actually define vector spaces whose scalar ring is a subring/subfield of \C . Can I make the change "complex module" ----> "subcomplex module" and similarly for the others?

benjub commented 5 years ago

@nmegill or @digama0, may I change the wording to the less confusing "subcomplex module" etc., and then close this issue?

nmegill commented 5 years ago

@nmegill or @digama0, may I change the wording to the less confusing "subcomplex module" etc., and then close this issue?

It is OK with me.