About the `LinearMap.CompatibleSMul` typeclass

Stream: mathlib4

[Brendan Seamas Murphy]

It seems like the standard usage of the LinearMap.CompatibleSMul M M₂ R S typeclass, at least the one which is generated by instance resolution, is the case where [IsScalarTower R S M] and [IsScalarTower R S M₂] (in standard math language, when S is an R-algebra and M, M₂ are S-modules). But the predicate is also be true if R is a solid S-algebra, i.e. one for which the restriction of scalars R-Mod -> S-Mod is fully faithful (hence a reflective embedding). We can't express this in terms of typeclasses (unless we add a [IsSolid S R] typeclass, which might be useful?) but in the specific cases where R is a localization or quotient of S we could add an instance [LinearMap.CompatibleSMul M M₂ R S]. Is there a reason not to do this? I think the LinearMap.CompatibleSMul typeclass is intended for the case where S is an R-algebra, but I don't see any place things would break in the reverse situation.

[Brendan Seamas Murphy]

(this usage of the term solid is unrelated to and predates its usage in condensed mathematics)

[Eric Wieser]

I created docs#LinearMap.CompatibleSMul` pretty much just to allow some questionable generalizations on the border of rings and semirings; if you only care about rings, I think you can stick to the more general scalar compatibility classes.

[Eric Wieser]

(#12671 fixes a typo in its docstring)

[Brendan Seamas Murphy]

Oh huh I thought it served a different purpose because it showed up in LinearEquiv.restrictScalars. It was that that I wanted to use to go from an R-linear equivalence to an (R/I)-linear equivalence

[Brendan Seamas Murphy]

Well I guess I have the same questions about scalar towers. But I'd guess there's a reason we don't want to have cycles there...

[Kevin Buzzard]

There was a reason we didn't want to have cycles (lean 3 didn't like them...)

[Eric Wieser]

I think nontrivial cycles can still be pretty bad for performance