weierstrass `map_id` signature

Stream: mathlib4

[Edward van de Meent]

i noticed that WeierstrassCurve.Affine.Point.map_id can be generalized (sort of). Currently its statement uses Algebra.ofId F F to denote the identity AlgHom from F to itself over itself. However, i have a usecase where i need a weaker(?) version, as in my case i'd like to use AlgHom.id R F. These all use the same underlying functions, however they are different enough to the point that rw doesn't like using one in when another could be used. i am tempted to change map_id to use AlgHom.id S F (where there is IsScalarTower R S F). This at least proves the statement in the same generality as map is defined, and as such allows map W (AlgHom.id R F) P = P, map W (AlgHom.id F F) P = P to be proven using rw. However, this no longer allows rw to prove the orignal statement(!!)...

I'm more than happy to make a PR changing the statement to using AlgHom.id S F (i'm a buttonclick away), however just in case someone has an opinion on this i thought it would be good to ask for opinions...

[Edward van de Meent]

all of these statements do seem to be "equal" though, as simply using by exact map_id _ _ does work...

[Edward van de Meent]

it's really just the rw behaviour i'm interested in