Theorems · Definition · algebraic geometry

WeierstrassCurve.Affine.CoordinateRing.map

{R : Type r} →
  {S : Type s} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (W' : WeierstrassCurve.Affine R) → (f : R →+* S) → W'.CoordinateRing →+* (W'.map f).CoordinateRing

The ring homomorphism R[W] →+* S[W.map f] induced by a ring homomorphism f : R →+* S.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Cited by

3 results in Mathlib

Foundations

Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRing