finrank namespace naming convention

Stream: general

[Kevin Buzzard]

A couple of years ago I did a twitch livestream where I formalised an example sheet question (if $A$,$B$ are two 5-dimensional subspaces of a 9-dimensional vector space then $A\cap B\not=0$). I just tried this again and noticed a couple of things; firstly we can't write vector_space any more (this much I knew and I'm a bit sad but it's on my job list to get this notation back in a locale and then I'll be happy again) and secondly (perhaps when findim got refactored to finrank?) namespaces are all over the place. If you import linear_algebra.finite_dimensional then you get finite_dimensional.finrank (the nat-valued dimension of a f.d. vector space) and then lemmas like finrank_bot (in the root namespace) and also lemmas like submodule.finrank_le (in the submodule namespace).

I am never really clear on how these things should work; for example I never remember whether map f : subgroup G -> subgroup H is supposed to be subgroup.map or monoid_hom.map, so I don't quite know whether all this inconsistency is somehow expected (i.e. it's a consequence of our conventions) or whether everything should just be in the finite_dimensional namespace really.

Note also that dim_sup_add_dim_inf_eq is a statement about module.rank but submodule.dim_sup_add_dim_inf_eq is a statement about finranks. Should we expect the naming convention (whatever it is) to do better here? Why are either of these things called dim anyway if the convention now is to call things rank or finrank? Is this just an oversight?

I guess maybe it's actually time I understood the naming convention properly. Is there logic to whether map above is monoid_hom.map or subgroup.map? If so, does that same logic tell us anything here?

[Yaël Dillies]

monoid_hom.map could refer to a zillion things so I would be against using this name at all.

[Eric Wieser]

Unless we had a has_monoid_hom_map typeclass, then it could just mean the Right Thing™ on whatever type you have