Deprecate Submodule.IsHomogeneous

Stream: mathlib4

[Kenny Lau]

Should we deprecate Submodule.IsHomogeneous? It's defined to be just:

• p.IsHomogeneous ℳ = DirectSum.SetLike.IsHomogeneous ℳ p

which I think is an unnecessary additional layer, with the only advantage being that it makes dot notation work and maybe makes the typeclass searches marginally faster.

I propose additionally that we should move DirectSum.SetLike.IsHomogeneous to the main namespace as IsHomogeneous, which then various kinds of homogeneous objects (not yet defined) can all call.

cc @Jujian Zhang

[Kenny Lau]

I think another potential disadvantage of deprecating is that Ideal.IsHomogeneous.bot might have to be renamed to IsHomogeneous.botIdeal, but I think that's a small cost

[Andrew Yang]

I don't think it makes sense for there to be a IsHomogeneous in the root namespace. For there could be a bunch of things that are homogeneous. Polynomials, functions, spaces etc.

[Kenny Lau]

that makes sense, but the double namespace situation we currently have is also very unfortunate, can we drop DirectSum.?