[Merged by Bors] - refactor(AlgebraicGeometry/EllipticCurve/*): refactor base change for ring homomorphisms

[Multramate]

Refactor Weierstrass curves and nonsingular rational points to allow for base changes over an arbitrary ring homomorphism φ : K →+* L. This generalises the natural map algebraMap K L and removes the necessity for Algebra K L, but also gives an easy way to define DistribMulAction for the action of L ≃ₐ[K] L on the nonsingular rational points over L, since L ≃ₐ[K] L restricts to L →ₐ[K] L that restricts to L →+* L. The old notation W⟮L⟯ is preserved for base change over algebraMap K L.

Also remove some unnecessary coercions in the Weierstrass file.

---

[riccardobrasca]

Are you sure this modification is worth? In practice people will base change from R to an R-algebra A 95% of the times, and they will have to write algebraMap R A everywhere...

[riccardobrasca]

Personally I prefer the previous spelling with the parenthesis, here I think it helps readability, but as you prefer.

[Multramate]

They should not need to write algebraMap R A in most cases, as the notation W⟮A⟯ still exists for a Weierstrass curve W over R and an algebra A over R. I think it is worth it, as in the following use case:

variable {R : Type} [CommRing R] (W : Affine R) {A : Type} [Field A] [Algebra R A]

instance : DistribMulAction (A ≃ₐ[R] A) (W⟮A⟯) where
  smul := fun σ => Point.ofBaseChange W σ.toAlgHom
  one_smul := fun P => by cases P <;> rfl
  mul_smul := fun _ _ P => by cases P <;> rfl
  smul_add := fun _ => map_add _
  smul_zero := fun _ => rfl

Here, the proof for smul_add follows trivially from map_add' in ofBaseChange. In the old definition, I can't consider an arbitrary automorphism of A that fixes R since there is only algebraMap R A, and would have to rewrite the same proof.

[riccardobrasca]

If there is no need to write algebraMap I am happy with the modifications, thanks!

bors d+

[mathlib-bors]

✌️ Multramate can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[Multramate]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style