feat: Group scheme structure on Weierstrass curve

[alreadydone]

---

[github-actions[bot]]

PR summary 411e13dab0

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.AlgebraTower	869	908	+39 (+4.49%)
Mathlib.Algebra.GroupWithZero.NonZeroDivisors	562	575	+13 (+2.31%)

Import changes for all files

Files	Import difference
Too many changes (288)!

---

Declarations diff

+ AlgHom.equivHomOver + AlgHom.equivSchemeOver + Algebra.mkOver + Algebra.schemeSpecOver + CategoryTheory.Functor.FullyFaithful.mapOver + CategoryTheory.Functor.mapOver + CategoryTheory.Functor.mapOver_hom + Coeff + Field.two_ne_zero + Module.Free.trans + PBool + _root_.AlgebraicGeometry.IsOpenImmersion.of_isLocalization + _root_.Polynomial.algebraMap_comp_algebraMap + _root_.Polynomial.mapRingHom_comp_algebraMap + _root_.Polynomial.mapRingHom_mapRingHom_comp_algebraMap + _root_.quotientIdealSpanSingletonAlgHomEquiv + aevalAEval + aevalAEval_algHom + aevalAEval_eq_evalEval + aevalAEval_toRingHom + affinePoint + algHomEquiv + algHomPolynomial₂Equiv + algebraMap_mem_nonZeroDivisors_iff + algebraMap_mem_nonzeroDivisors_iff + comap_nonZeroDivisors_eq_nonZeroDivisors_of_injective + comap_nonZeroDivisors_le_nonZeroDivisors_of_injective + coordinateRingInfToLoc + coordinateRingToLoc + coordinateRingToLoc_Y + coordinateRingToLoc_Z + curveField_eq + curveRing_map_ringEval + curve_a₁ + curve_a₂ + curve_a₃ + curve_a₄ + curve_a₆ + cusp + cusp_equation_one_one + eval + evalEvalRingHom_comp_algebraMap + evalEvalRingHom_comp_map_mapRingHom_algebraMap + evalEval_CC + evalEval_map_mapRingHom_algebraMap + eval_comp_algebraMap + eval_comp_map + eval_comp_mk + eval_map + eval_mk + eval₂RingHom_aeval_C_X_Y + eval₂_aeval_C_X_Y + eval₂_affine_polynomial + eval₂_polynomialInf + glueData + instance : Algebra (CoordinateRingInf W) (LocalizationY W) := (coordinateRingInfToLoc W).toAlgebra + instance : IsLocalization.Away (CoordinateRingInf.mk W Y) (LocalizationY W) + instance : Module.Free R R[X] := .of_basis (basisMonomials R) + instance : Module.Free R W.CoordinateRing := .trans R[X] + instance : Module.Free R[X] W.CoordinateRing := .of_basis (CoordinateRing.basis W) + instance [Nontrivial R] : Nontrivial W.CoordinateRing := (algebraMap_injective W).nontrivial + isUnit_mk + isUnit_mk_one + jacobianPoint + locAlgEquiv + locRingEquiv + map_comp_algebraMap + map_comp_mk + map_specialize + mem_nonZeroDivisorsRight_of_ne_zero + mem_nonZeroSMulDivisors_of_ne_zero + mk + mkₐ + mkₐ_apply_eq + mkₐ_eq_mk + mkₐ₂ + mkₐ₂_apply_eq + mkₐ₂_eq_mkₐ + nonZeroSMulDivisors_self + openCover + pointedCurve + polyEval + polyEval_comp_eq_specialize + polynomialInf + polynomialZ + pullback_snd_comp_inv_fst + ringEval + ringEval_comp_eq_specialize + ringEval_comp_mk + ringEval_mk + scheme + schemeToBase + smoothLocus + smul_eq_zero_iff_of_mem_nonZeroDivisorsRight + smul_eq_zero_iff_of_mem_nonZeroSMulDivisors + smul_left_injective + specialize + Δ_curve_ne_zero ++ GlueData.mk₂ ++ aevalAEval_X_Y ++ algebraMap_injective ++ algebraMap_injective' ++ curve ++ equation_mk_X_mk_Y ++ instance : IsOpenImmersion <| Spec.map <| CommRingCat.ofHom <| ++ mk_comp_algebraMap ++ mk_polynomial

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[Multramate]

I'm not reviewing this, but maybe this should include #14130 as a prerequisite?

[jcommelin]

@Multramate @alreadydone Both #14167 and #14130 add the file Mathlib/AlgebraicGeometry/EllipticCurve/Scheme.lean. But with different contents. Could you please coordinate what should be in which PR, and how to move these PRs along? Possibly (common) prerequisites should be factored out into separate PRs. Feel free to start a discussion about this on Zulip.

(crossposting this on the other PR as well)