Algebra S (RestrictScalars R S M)

Stream: mathlib4

[Kenny Lau]

If we have R-algebra S and S-algebra M, then RestrictScalars R S M is the canonical way to make it an R-algebra M. (canonical when constructing, not when proving; when proving use IsScalarTower instead)

But my problem is, now we no longer have an instance of Algebra S (RestrictScalars R S M). What is the canonical way to build a scalar tower then?

[Kevin Buzzard]

If you already have [Algebra R S] and [Algebra S M] then why not just add extra hypotheses [Algebra R M] [IsScalarTower R S M]?

[Kenny Lau]

that is for proving, but not for using

[Kevin Buzzard]

Can you explain to me a concrete situation where my suggestion is not the answer? (I don't follow what you're saying yet)

[Kenny Lau]

I think in practice I ended up using Algebra.compHom to construct the instance

[Kenny Lau]

Kevin Buzzard said:

Can you explain to me a concrete situation where my suggestion is not the answer? (I don't follow what you're saying yet)

Basically, let's say you proved a theorem for R S M using the scalartower hypothesis, and now you have a concrete values for R S M (e.g. S K K[x]/(x^2)), and now I need to apply the theorem to this situation, then you basically need compHom to first define a structure of S-algebra on K[x]/(x^2)

[Kenny Lau]

and then now you can use the theorem