An algebra hom equivalent to LinearMap.rTensor

Stream: Is there code for X?

[Michał Mrugała]

I want to change a LinearMap.rTensor to a defeq AlgHom.toLinearMap. Do we have this defined somewhere in Mathlib?

[Andrew Yang]

Algebra.TensorProduct.map _ .id

[Michał Mrugała]

I'm not sure how this helps. I know that I could construct the hom with map, but I don't see how to get something defeq here.

[Andrew Yang]

Then use convert perhaps and not rely on defeqs?

[Michał Mrugała]

I think since we have this defined for coalgebra and bialgebra homs I will just define it for algebra homs too. I think it's a useful definition.

[Michał Mrugała]

Or rather abbrev

[Eric Wieser]

Are the maps not defeq?

[Andrew Yang]

I checked. They are.

[Andrew Yang]

But I agree that AlgHom.rTensor is a useful abbrev to have too.