Discussion about substructures of extensible structures

[avekens]

This issue is about substructures of extensible structures in general, see discussion starting with the comment of @benjub on 17-Dec-2019.

The original open point is tracked in issue #1333 now. The original first comment of this issue was:

I almost finished the revisions of the sections with theorems in the context of the Cayley Hamilton theorem in my mathbox. The next step would be to move these sections (and after the definition of diagonal/scalar matrices is clarified, see the discussion in the Google group https://groups.google.com/d/msg/metamath/4_ZOT4Gddwo/k-lxGMxGBgAJ , also subsection "The subalgebras of diagonal and scalar matrices " ) into the main part, Part "11. BASIC LINEAR ALGEBRA").

I would propose to place subsection "The subalgebras of diagonal and scalar matrices" after subsection "11.2.1 The matrix algebra", and sections "Polynomial matrices" and "The characteristic polynomial " after "11.3 The determinant".

Would this be OK? Of course there will be a lot of auxiliary theorems currently in my mathbox, which are used in the proofs of these sections, to be moved to the main part, too.

[avekens]

According to David's Google group post https://groups.google.com/d/msg/metamath/jINlwEjvwOc/IINkUI1sBAAJ, I want to move the Cayley Hamilton theorem and all the theorems required to prove it from my mathbox into the main part of set.mm, as indicated in this issue. Before I can do this, the question how to define diagonal and scalar matrices must be answered, see my Google group post https://groups.google.com/d/msg/metamath/4_ZOT4Gddwo/k-lxGMxGBgAJ . Unfortunately, there is no response to this post until now. So I want to ask (some of) you directly:

@nmegill @benjub @tirix @david-a-wheeler @digama0 : do you have any hint/opinion/preference which of the alternatives to define diagonal and scalar matrices described in the Google group post https://groups.google.com/d/msg/metamath/4_ZOT4Gddwo/k-lxGMxGBgAJ should be used?

As soon as we have a decision, I'll start to revise section "The subalgebras of diagonal and scalar matrices" in my mathbox. Afterwards, I can move this and other subsections concerning the Cayley Hamilton theorem into the main part as proposed in this issue.

[tirix]

Hi Alexander,

Both solutions described in your post seem to have their advantages and drawbacks.

I think my vote may go to your current ‘ DMatALT ‘, since its definition is simpler, the operations are identical, and I would assume that later developments would use more often statements like “M is a diagonal matrix” rather than “the set of diagonal matrices forms a ring”.

However, I have no strong opinion and would agree with any solution. BR, _ Thierry

[benjub]

I do not have enough experience in long proofs and extensible structures to give an authorized advice. From a theoretical point of view, I would prefer the first version. Would it be possible to define substructures generally ? I mean:

df-substruct $a |- SubStruct = ( x e. _V |-> { y | ( ( Base ` y ) C_ ( Base ` x ) /\ ... ) } ) $.

It would be a huge incomprehensible definition, like df-prds or df-imas, and it would not be able to handle all the cases. For the "slots" I'm thinking of, like the algebraic operations, the topology, etc., it looks doable. But this might be dangerous if the forgetful functors stay implicit... Worth doing ?

[tirix]

Not sure I get what you mean: we do have the |'s operation for substructures, which you are already using. If you want to talk about the subring of scalar matrices, you can use ( ( N Mat R ) |'s A ) where A is the subset of interest. That's how you'd get the "substructure".

My point (maybe weak) was that I guess we are likely to make more statements about the scalar matrices themselves (elements of the set A) than on the structure of scalar matrices, and even the statement that this structure is a subring can be expressed without the |'s operation, just with A e. ( SubRing ' ( N Mat R ) ) .

[benjub]

@tirix By defining df-substruct, I want to define substructures in general, that is, A e. ( SubStruct ` CCfield ) will mean that A is a subfield of CCfield (provided CCfield is defined as a field, I don't remember, maybe it is defined as a topological field); A e. ( SubStruct ` ( N Mat R ) ) will mean that A is a subring of ( N Mat R ), etc. It's like the definition df-prds I mentionned above: you don't define "group product", "field product", "topological space product"; you just define "extensible structure product".

A possible problem is that often, a structure is defined in set.mm "as rich as possible", e.g. RRfield, IIRC, is defined as an ordered topological field (or even ordered topological measured \R-algebra ?), and one might want to say "A is a subring of RRfield", or "A is a subspace", or "A is an ordered subgroup", etc. That's what I was referring to when talking about forgetful functors. There could be e.g. a function Ring_to_Group that associates with a Ring (as an extensible structure) its underlying additive group, and then one could write things like A e. ( SubStruct ` ( ( Ring_to_Group ` B ) ). But this is trying to do category theoretic things (on objects only) in a different framework, so it is necessarily clumsy.

Anyway, I'm not experienced in extensible structures (nor fond of them, though I admit I do not have a proposal for anything better, since it should encompass so many different things without a too heavy notation). From a mathematical point of view, structures à la Bourbaki (in the 1930's) were subsumed by categories (in the 1940's). I would like to try and stay close to the mathematical practice, though I do not know what is best suited to proof-formalization and set.mm.

[tirix]

@benjub right now RRfld is indeed as rich as possible, i.e. the same object (set) RRfld can be seen as a totally ordered set (~ retos), as a field (~ refld), or as a metric space (~ recms), etc., depending from what angle you look at it.

Thus there is no need for "Ring_to_Group" converters, all rings are groups. If you want to say "A is a sub-group of the real numbers", you can use A e. ( SubGrp ' RRfld ) , which considers RRfld as a group.

I guess in a first attempt we could define a new generic Sub-X construct like Sub X = ( w e. X |-> { a e. ~P ( Base ' w ) | ( w |'s a ) e. X } )

I.e. for an X (Group) w, define a sub-x (subgroup) of w as a subset of the base of w, which itself also defines an X (group). This could be used for different X, like monoids. However, that condition is not always sufficient: for rings, subrings are also required to contain the multiplicative identity, and this would not be ensured here, so there is not generic rule for all X, no such easy one-fits-all "subspace" solution.

~ prds and ~imas are constructing new structures based on existing ones. If the input structures are poorer (e.g. no inner product defined), the resulting structures will still be valid for other operations (e.g. group operation), but not for the more advanced ones.

I don't think there would be any practical use in the same approach for "subspaces", because you would have to define a "sub-everything" and include all constraints, unless there are special provisions like "ensure that the multiplicative identity is in the subspace only if there is one" or "only if the original structure is a ring". That does not sound practical.

[avekens]

Although I find the discussion about a general definition of "substructures" very interesting, I agree with Thierry that it is very difficult or even impossible to find a definition which is comprehensive on the one hand and practical on the other hand. Maybe it would be better to continue this discussion for categories (I do not know if this is easier because I do not know much about category theory...).

Coming back to the original question, Thierry had good arguments for defining substructures as sets (and not structures). Meanwhile, I would also prefer these definitions (DMatALT, ScMatALT), because they better fit to the way substructures are currently used in set.mm. Furthermore, it will be easier to revise the existing theorems about diagonal/scalar matrices, because they are based on the set-like definitions already.

If nobody has arguments for a structure-like definition, I will switch the names of the definitions (ALT vs. non-ALT) and start to revise the theorems about diagonal/scalar matrices using the set-like definitions. @nmegill @digama0 @david-a-wheeler @sorear what do you think?

[benjub]

(I'm continuing the discussion about extensible structures; let this not hold @avekens from doing his modifications.)

Yes, there is a use for SubStruct. For instance, it makes sense to define the monoid of natural numbers, NNmnd. Then, provided that RRfield was defined as merely a field, you could state |- NNmnd e. ( SubStruct ( Ring_to_Monoid RRfield ) ). You wrote: "A is a sub-group of the real numbers", you can use A e. ( SubGrp ' RRfld ) It is indeed the current way to do it, but I do not find it very satisfying. The statement says rather something like "the set A, when equipped with the induced operations from RRfield, is a subgroup". This may seem pedantic because this is almost the same thing for algebraic structures, but it is not the case for other kinds of structures (but for these generalizations, my proposal of SubStruct may also fail).

Indeed, as I wrote above, it will be impossible to find a definition which encompasses all cases (this is also the case for df-prds and df-imas, by the way). As you say, it is even harder for substructures because of "ensure that the substructure has an identity if the original structure has one". But from the very beginning, the framework encompasses only some cases, since extensible structures correspond roughly to (the objects of) certain concrete categories.

Extensible structures are sets with extra structure or extra stuff, but not with extra property, IIRC. But the boundary between "extra structure" and "extra property" is thin. For instance, do groups have extra property or extra structure compared with monoids? (that is: is inversion part of the data or a consequence of the property that every element is invertible) There is no correct answer to this: it depends on your objectives. Similarly with monoids/magmas, fields/rings, etc.

I understand the benefits of defining extensible structures "as rich as possible": at first, it seems that you save notation: you do not have to define RRgrp, RRring, RRtop, RRtopgrp... But there are also drawbacks (which seem more severe to me). First, the extra notation is not a real drawback since anyway, RRgrp and RRtopgrp are indeed different mathematical objects, so having different notations is not surprising, even if it's a bit heavy. And you only need to introduce the ones you need. Second, with the "as rich as possible" method, the very nature of your object is uncertain. For instance, if/when manifolds are introduced in set.mm, you will want to say that RR is a manifold, so you will add a "slot" and RRfield will be a different object from what it used to be. So all the theorems already in set.mm before the introduction of manifolds will actually state something different from what they used to (even if extensible structures, and this is a smart device, hide these things under the hood by ignoring irrelevant slots, a bit like a built-in automatic forgetful functor -- but, being automatic, a bit too rigid). Also, the proposal I made above is incompatible with the "as rich as possible" method: one would need to update, roughly NNmnd e. ( SubStruct ( OrdTopRing_to_Mnd RRfield ) ) to NNmnd e. ( SubStruct ( OrdTopManRing_to_Mnd RRfield ) ) (or "to_TopMnd") and similarly, one would need to update df-prds, df-imas, df-substruct... We see that things will be getting out of hands very quickly.

Put shortly, the problem with "as rich as possible" is that "possible" changes over time with the development of set.mm. There is also a balance to find between the comfort of having this "built-in automatic forgetful functor" provided by extensible structures and the rigidity it entails.

As I said in a recent github issue (around the end of #1286 in a discussion with @nmegill), this is not a rant or a criticism of extensible structures. It is simply a reflection on its limitations, because one needs to be aware of them. And as I also wrote above, I am aware that I'm trying to do (object-level) categorical thinking on a framework not adapted to it, so it is necessarily clumsy. If it were up to me, I think I would adhere much more to categorical thinking, but in the proof-formalization domain, "ideas are cheap, execution is everything" and I humbly admit that I'm not the one building the long proofs.

[digama0]

I don't yet see what pressing issue with the current setup you are trying to solve, nor what your proposed solution is and how it is better. Yes, there are other ways to handle structures. They are more notationally cumbersome, though, especially in metamath's case because of the lack of any hidden arguments. Certainly the extensible structure framework doesn't solve all problems, but it does surprisingly well at most problems, and localized deviations can compensate for its weak points, as far as I have seen.

To my mind, SubStruct isn't a thing. There is a universal "substruct" operation already, and it is |`s. It restricts the base of the structure and nothing else, with all other slots being implicitly "substructed" so that you get the right results. NNmnd is simply ( CCfld |`s NN ), and similarly for all the other subsets of CC. It has all the structure we can show applies to it, not just a monoid but also a topological monoid, with a metric, etc. And this all comes for free. What you are proposing would seem to be a big step down in terms of expressivity.

Should we come up with some new structure in the future that we wish CC to inherit, then we change the definition of CCfld, reprove all the slot extraction theorems, add a new one, and that's it. None of the other downstream theorems have to change. You can say it is "different" but it is provably the same in the strong sense that the base set and the operations of the field are all the same as before, i.e. it is "equal as a field" to the old definition. Equality of structures is not meaningful, which is why theorems like ablpropd exist.

I disagree that "the nature of the object is uncertain"; you can extract the "group content" of a structure, which is the pair <. B , ( x e. B , y e. B |-> ( x + y ) ) >. where B and + are the base set and operation, respectively; but writing it this way is rarely helpful. Two structures with the same group content have all the same group properties: the same identity, the same inverse, the same set of p-subgroups, etc. It is a stronger notion than group isomorphism, being closer to "equal as sets", but it ignores all variation caused by extensible structures.

If you want to see the categorical approach play out in a real formal system, check out Lean's mathlib. It's much closer to what you are talking about, but instances (the chain of proofs that an X is a Y via a bunch of forgetful functors) cause serious performance problems, and they are long past the level where people would find it acceptable to look at them directly. Metamath is working under much stricter conditions than this, and it has still managed to achieve about the same level of flexibility.

[benjub]

There is no pressing issue I want to solve, as was clear from my previous messages. And as I also said, I am unable to propose a better approach. I agree with most of what you write, and there is mostly no contradiction with the above. Thanks for the pointer to Lean's mathlib; I'll have to have a look when I have time. I retain the notion of "built-in automatic forgetful functor" (on objects) that I used above, which I think conveys an important feature of extensible structures.

I think that SubStruct (which I will not write in set.mm since I admit it wouldn't be very useful) actually is a thing, different from structure restriction |s. The first example that comes to my mind is that of immersed submanifolds. Admittedly, it is not a great example since the good notion of subobject for manifolds is closer to that of embedded submanifolds (actually, there is a case for the notion of "initial submanifold", whose definition is roughly "the notion of submanifold which makes |s work", see for instance "Abstract and Concrete Categories, the Joy of Cats"). Here it is: consider a "figure of eight" curve (a lemniscate), say M, as a subset of R^2. Then, it can me made into a connected injectively immersed submanifold of R^2 in precisely two ways, say M1 and M2 (you see what I mean: the origin pertains to one or the other branch). Then, you have M1 e. ( SubStruct ( RichThing_to_Man R^2 ) ) and similarly with M2, but you cannot define, say, ( RR2man |` M ) as a manifold. Here, the problem is that the subset does not determine the substructure. And we are still in the realm of concrete categories. Things get "worse" for non-concrete ones.

So far in set.mm, extensible structures have been applied to (the objects of) algebro-topological concrete categories, so you will not see these problems happening (I haven't worked out the precise properties of the forgetful functors that are required, but probably monadic is sufficient and having a left adjoint (a free functor) is necessary). You might say that extensible structures were precisely designed for these cases only, and that I am objecting that it does not apply to something it has never been created to apply to. I readily accept this, and I am not, and have not been, demoting extensible structures. I just think these limitations are worth pointing out.

Finally, of course, there are different notions of subobjects, depending on the definitions of morphisms we take, and it will not be possible to deal with them simply. For instance, the categories of R-modules, of non-unital R-modules, of modules (over any ring), etc. each have a different notion of subobject. (I know you know that, but I mention it here for the record.)

[david-a-wheeler]

I think we ought to explain extensible structures, including some discussion about why they are the way they are, in some visible place such as mmset.html. maybe we can copy some of the discussion from here.

[nmegill]

Finally, of course, there are different notions of subobjects, depending on the definitions of morphisms we take, and it will not be possible to deal with them simply. For instance, the categories of R-modules, of non-unital R-modules, of modules (over any ring), etc. each have a different notion of subobject. (I know you know that, but I mention it here for the record.)

For the record, I didn't know that. :) What are the differences in their subobject definitions?

[avekens]

Since this issue is more about substructures of extensible structures in general, I opened a new issue #1333 for the original intend and copied the relevant parts from this issue to the new one. Furthermore, I changed the title and initial post of this issue accordingly.

So this issue can be used to continue the discussion about substructures of extensible structures ...

[benjub]

Forget about non-unital modules, this was a stupid idea. Instead, consider the two categories: Ring, the category of (unital) rings and their (unital) morphisms, Rng, the category of (non-unital) rings and their (non-unital) morphisms. As usual, "non-unital" means "non-necessarily unital". As for the notation, "Rng" was chosen because a rng is a ring which lost the "i" of its identity (this is rather well-spread, and this is why I insist that things related to rings in set.mm be spelled out "ring" to avoid ambiguity). Then, the zero ring is a subobject of \Z (or any rng) in the category Rng, while it is not so in the category Ring (even though it is a (unital) ring). This is not completely anecdotical: this entails that the category Rng has a zero object (an object which is both initial and terminal) while the category Ring does not (its initial object is \Z while its terminal object is the zero ring).

For the second example, let R be a ring and consider the two categories: R-Mod, the category of R-modules and their morphisms, Mod, the category of modules and their morphisms, where a morphism from an R-module M to an S-module N is a pair of maps (a, f) with $a$ a ring morphism from R to S and f : M \to N a group morphism such that f(\lambda x) = a(\lambda) f(x) for \lambda \in R and x \in M. Obviously, an R-module will typically have far more submodules in Mod than in R-Mod. The more natural and important category is R-Mod for a fixed R, but the category Mod is sometimes useful. I saw examples of its use in representation theory, but I don't remember them well enough.

[digama0]

But what does this mean for practical formalization? We already have a number of different substructure predicates which have their own names: ( SubGroup ` G ), ( SubRing ` R ), etc. They all take the same kind of input, namely an extensible structure, and they return a set of subsets of the base set of that structure which are "subobjects" in the appropriate sense. We can use ( G |`s H ) to manifest a subgroup of a group as a group in its own right. There is nothing at all stopping us from having a ( SubRng ` R ) predicate if we care to (but AFAIK we have never formalized non-unital rings and have no current need for them).

Of course, extensible structures only work well when they represent concrete categories, where there is a "base set", homs are functions, and subobjects are subsets with induced operations (although the meaning of "induced operation" can vary depending on the slot). For more complicated things, extensible structures may not suffice, but I prefer to be goal directed in my considerations here and so prefer to plan for this eventuality when a need for it actually arrives and not before. None of the categories discussed thus far fall outside the purview of extensible structures, as far as I have seen. (The category Mod of modules over many rings is not a concrete category but you can still represent it with more structured homs.)

[digama0]

I will also remark that if you have literal categories, as in an element of Cat, then you can define the set of subobjects in the categorical way and get the right answer in all cases, more or less by definition.

[benjub]

If you say that SubStruct is useless because one already has SubGroup, SubRing, etc., you could similarly say that df-prds is useless because one could define GroupProd, RingProd, etc., or instead of |`s, GroupRes, RingRes, etc... Although I agree there is a difference in the fact that there are in set.mm probably more theorems about general products than about general substructures, so having a general notion of StructProd is more important than having SubStruct. And also, product and restriction "create" new structures rather than provide a set of structures.

The phenomenon I described above in the category of manifolds, which is concrete, shows that not only the "induced operation" can vary, but it may not exist at all. It is indeed a bit far-fetched since one could simply discard immersed submanifolds, and consider only embedded, or initial, submanifolds, for which things work. Of course, this is theoretical, and at the current state of development of set.mm, there is no pressing need.

By the way: the functor Mod \to Set which to the R-module M associates the set R \times M and to the morphism (f, a) described above associates the function (a, f) : R \times M \to S \times N is faithful so shows that Mod is concrete (maybe that's what you meant by "but you can still...").

[digama0]

There is a difference though. It is not possible to have SubGroup and SubRing be the same thing because they produce different outputs on the same input. The subgroups of an extensible structure treated as a group are not the same as the subrings of that same structure. With df-prds it can actually reasonably perform the task, that is, being the product group given a family of groups, while also being the product ring given a family of rings. There is no contradiction here because the group part of a product ring is a product group.

There is also a general theory of "substructure algebras", in the form of df-mre and df-acs. SubGroup is a moore collection, as is SubRing, SubRng and many other substructure collections. But it's no good for picking out a particular collection of interest; SubRing and SubGroup still need to be defined and they are distinct -- nothing is going to select these definitions for us.

As for manifolds, I don't see very much use for |`s subsetting, as you will normally not get closed manifolds by taking subsets of other such manifolds. Maybe connected pieces, but that's all. Manifold embeddings or immersions are something else entirely; you clearly need a function to perform that mapping so the implicit subset morphism doesn't cut it. But there is no issue with having a set ( M ManifoldImmersion N ) encoding all these details.

It's possible that the categorical definition of concrete category doesn't quite capture what I mean in this instance; I would want to impose that the functor be the "obvious" one, rather than there merely exist some functor, and while maybe it's not so obvious for Mod which functor to take, I would have mapped the R-module M to the set M, and similarly map (f, a) to just f, and clearly this functor is not faithful.

[benjub]

There is a difference though. It is not possible to have SubGroup and SubRing be the same thing because they produce different outputs on the same input. The subgroups of an extensible structure treated as a group are not the same as the subrings of that same structure. With df-prds it can actually reasonably perform the task, that is, being the product group given a family of groups, while also being the product ring given a family of rings. There is no contradiction here because the group part of a product ring is a product group.

Agreed. That's what I was trying to say with fewer details at the end of my first paragraph, but you made it clearer. There is a choice of "where to forget the structure", and the current policy is to keep the structure as rich as possible all the way (when defining it, when taking products, etc.), and only when considering a subobject, then use SubGroup, etc. to forget the extra structure. It's probably more economical in terms of notation and proof building.

There is also a general theory of "substructure algebras", in the form of df-mre and df-acs. SubGroup is a moore collection, as is SubRing, SubRng and many other substructure collections.

Thanks for these links! I had begun doing some ground work on "collections closed under intersections" since I want to study convex sets, and I hadn't located df-mre (I didn't know the term "Moore collection"). I'll be able to reuse that section.

As for manifolds, I don't see very much use for |`s subsetting, as you will normally not get closed manifolds by taking subsets of other such manifolds. Maybe connected pieces, but that's all. Manifold embeddings or immersions are something else entirely; you clearly need a function to perform that mapping so the implicit subset morphism doesn't cut it. But there is no issue with having a set ( M ManifoldImmersion N ) encoding all these details.

The category of manifolds has notoriously bad categorical properties. You probably know that there is this general compromise between "bad category of well-behaved objects" and "well-behaved category of bad objects". You can see this in schemes vs. varieties for instance. The "correct" notion of subobject for manifolds is actually that of "initial submanifold", which is in between "immersed" and "embedded". It roughly corresponds to the subsets for which there is a unique induced smooth substructure. But it crucially uses the fact that Man is concrete.

It's possible that the categorical definition of concrete category doesn't quite capture what I mean in this instance.

You're right. Sometimes, people use the word "concretisable" for the mere existence of a faithful functor to Set (or another category in the relative case) and maybe I should have used that one.

[david-a-wheeler]

I tried to summarize some of this discussion here: https://github.com/metamath/set.mm/pull/1335

I think there are important clarifications about extensible structures that aren't documented in set.mm (until now).

If there's an error, or a way to improve it, let me know there!

[benjub]

A "historical" question came in a discussion I was having with Gérard: who introduced extensible structures ? @nmegill and/or @digama0 ? (possibly with "preliminary work by" or "improvements by") And were they inspired by Bourbaki's "espèces de structures" ("kinds/species of structures") ? They are in any case reminiscent of them. Thanks.

[nmegill]

I introduced the basic idea, around 2012 I think, but Mario and Stefan added some significant improvements.

I basically wanted something simple that would allow me to reuse, as directly as possible, theorems from more general structures, such as using group theory theorems for the additive operation of a ring, so they wouldn't have to be reproved.

Category theory required morphisms to relate structures, which seemed far too complex for my purposes when you had to express them formally with everything explicit like Metamath requires. Upon FL's suggestion, I took a cursory look at Bourbaki's structures (just a few pages on Google books since I didn't have the book), but it also seemed to require morphisms IIRC.

Before introducing them in set.mm, I went through several iterations and discussions on the old AsteroidMeta wiki, but archive.org unfortunately didn't archive it (although it has most of the rest of that wiki), and my last backup of that wiki was before that discussion.

On this page: https://web.archive.org/web/20141010075854/http://wiki.planetmath.org/cgi-bin/wiki.pl/metamath you can see "Extensible structure builder" under the first bullet but the link is dead.