Induce structures on linear subspaces

[benjub]

As I noted in https://github.com/metamath/set.mm/pull/2877#discussion_r989416318 with @avekens, the current definition of linear subspaces of modules (https://us.metamath.org/mpeuni/df-lss.html) is set-theoretic only, that is, its value ( LSubSp ` V) (where V is a module) is (the set of) the underlying sets of the linear subspaces of V, and not the (set of) linear subspaces of V. This leads to peculiar statements in later theorems.

I propose to use the restriction of structures https://us.metamath.org/mpeuni/df-ress.html in df-lss so that it produces linear subspaces as extensible structures (in particular, with induced topological structures in the case that triggered this issue). If the underlying set is needed, we can always use Base, e.g., |- ( V e. LMod -> ( M e. ( LSubSp ` V ) -> ( Base ` M ) C_ ( Base ` V ) ) ). Similarly for closed subspaces, etc.

Thoughts ? (@digama0 ?)

[avekens]

Already subgroups are defined as being subsets of the base set of a group (~df-subgr), and the definition uses the restriction of structures:

SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Grp } )

Subgroups as structures are already given by restrictions of structures, and an element of ( SubGrp `` G ) is its base set, for example:

    subggrp.h $e |- H = ( G |`s S ) $.
    subggrp $p |- ( S e. ( SubGrp ` G ) -> H e. Grp ) $=
    subgbas $p |- ( S e. ( SubGrp ` G ) -> S = ( Base ` H ) ) $

Here, H is the subgroup as structure, and S is its base set. Maybe reading S e. ( SubGrp `` G ) as "S is a subgroup of G" is misleading, maybe "S induces a subgroup of G" would be more appropriate.

I think there are reasons why substructures are defined in this way (maybe @digama0 can explain them or give a hint to a place where this is explained).

Nevertheless, it would make no sense to switch the definition for linear subspaces only: it would be necessary to switch all the definitions for substructures - to keep/obtain theorems like ~lssubg:

( ( W e. LMod /\ U e. ( LSubSp ` W ) ) -> U e. ( SubGrp ` W ) )

[digama0]

The "indexing type" of a substructure is the underlying set, this is what it means to be able to form a substructure (with |`s). Collecting all the structures isn't a good idea because these tend to be a proper class when you consider all the irrelevant components that can vary. Sets are a much more well behaved collection - they have a nice complete lattice structure, and you can take any set and find it (or not) in the set of sub-things of a group. If you have a structure, asking whether it is a sub-thing of a group doesn't make much sense on its own - it is better to ask whether the structure is equivalent (in some sense) to a subgroup of the group, where "a subgroup of the group" means a quantifier over subsets of the group that are closed under group operations.

In short, I don't think the resulting change would be for the better, you would need a lot more operations to e.g. take the intersection of two subgroups by first getting their base set, intersecting them, and then pulling that back to a structure. Sets have a lot of API in set.mm and you would lose all that and replace it with an API which isn't usable for much other than these particular operations on structures-that-are-subsets-of-other-structures.

[benjub]

@avekens: yes, I took LsubSp as an example but the proposed change would have to be done consistently of course.

Collecting all the structures isn't a good idea because these tend to be a proper class when you consider all the irrelevant components that can vary.

@digama0: Here, we would only collect induced substructures of a given structure, and they form a set. Concretely, compare the current

df-subg $a |- SubGrp =
    ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Grp } ) $.

with the proposed

df-subgNEW $a |- SubGrpNEW =
    ( w e. Grp |-> { g e. Grp | E. s e. ~P ( Base ` w ) g = ( w |`s s ) } ) $.

One can of course translate back and forth: |- ( h e. ( SubGrpNEW ` g ) -> ( Base ` h ) e. ( SubGrp ` g ) ) and |- ( h e. ( SubGrp ` g ) -> ( g |`s h ) e. ( SubGrpNEW ` g ) ) (note that the latter statement is a bit more complex). One can also use direct images: ( Base " ( SubGrpNEW ` g ) ) = ( SubGrp ` g ) (and also in the other direction, currying |`s, but this is already more complex).

You take the example of intersections. As you wrote, if h, k are subgroups of g, then their "group-intersection" is ( g |`s ( ( Base ` h ) i^i ( Base ` k ) ) ). It is indeed longer, but I'm not sure it outweighs the other shortenings. And more importantly, the idea of "subroup of G" is more faithfully described by df-subgNEW than by df-subg. After all, a subgroup is a group. It looks to me like the more we're going to formalize more advanced parts (e.g., the Banach and Hilbert spaces that triggered this issue, or other rich structures with interplay of several structures), the more the proposed change would show its advantages.

Or maybe you're referring to something subtler ? Also, I have not practiced extensible structures a lot, so maybe you saw the arguments above and you still think the drawbacks outweigh the advantages ? (ping @digama0)