Scalar extension of an affine Weierstrass coordinate ring

For a homomorphism f : R →+* S, the coordinate ring of W.map f is the scalar extension of the coordinate ring of W along the coefficientwise map Polynomial.map f : R[X] → S[X]. More precisely, CoordinateRing.map induces an S[X]-linear isomorphism S[X] ⊗[R[X]] W.CoordinateRing ≃ₗ[S[X]] (W.map f).CoordinateRing sending p ⊗ₜ z to p • CoordinateRing.map W f z. This coordinate-ring comparison is an input to a later comparison of the function fields of W and W.map f, used to compare degrees of isogenies under base change.

Main definitions

• WeierstrassCurve.Affine.CoordinateRing.mapLinear: CoordinateRing.map, viewed as a linear map over the coefficientwise map R[X] → S[X].

Main results

• WeierstrassCurve.Affine.CoordinateRing.isBaseChange_mapLinear: the target coordinate ring is the module base change of the source coordinate ring.

noncomputable def WeierstrassCurve.Affine.CoordinateRing.mapLinear {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Affine R) (f : R →+* S) : have x := Module.compHom (W.map f).CoordinateRing (Polynomial.mapRingHom f); W.CoordinateRing →ₗ[Polynomial R] (W.map f).CoordinateRing

CoordinateRing.map, as a linear map over the coefficientwise homomorphism R[X] → S[X].

Equations

• WeierstrassCurve.Affine.CoordinateRing.mapLinear W f = { toFun := ⇑(WeierstrassCurve.Affine.CoordinateRing.map W f), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.mapLinear_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Affine R) (f : R →+* S) (z : W.CoordinateRing) : (mapLinear W f) z = (map W f) z

theorem WeierstrassCurve.Affine.CoordinateRing.isBaseChange_mapLinear {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Affine R) (f : R →+* S) : IsBaseChange (Polynomial S) (mapLinear W f)

The coordinate ring of W.map f is the module base change of the coordinate ring of W along the coefficientwise map R[X] → S[X].