MulActionEquiv

Stream: Is there code for X?

[Kevin Buzzard]

docs#LinearMap extends docs#MulActionHom and docs#AddHom. We also have docs#LinearEquiv extending LinearMap and docs#AddEquiv. But we don't have docs#MulActionEquiv extending MulActionHom and docs#Equiv ? Is there a reason it's missing or have I just failed to find it?

[Edward van de Meent]

i don't know that there is a reason why it doesn't exist, but i imagine that similarly to how LinearEquiv takes extra RingHomInvPair arguments, this would too require such arguments but for general functions, but I don't think there is a good way to do this.

[Edward van de Meent]

perhaps it'd be a bit easier if there was FunLike (A -> B) A B...