Theorems · Definition · algebraic geometry

WeierstrassCurve.Affine.Point.baseChange

{R : Type r} →
  (F : Type u) →
    (K : Type v) →
      [inst : CommRing R] →
        [inst_1 : Field F] →
          [inst_2 : Field K] →
            {W' : WeierstrassCurve.Affine R} →
              [inst_3 : DecidableEq F] →
                [inst_4 : DecidableEq K] →
                  [inst_5 : Algebra R F] →
                    [inst_6 : Algebra R K] →
                      [inst_7 : Algebra F K] →
                        [IsScalarTower R F K] → (W'.baseChange F).Point →+ (W'.baseChange K).Point

The group homomorphism on nonsingular points induced by the base change from F to K, where W is defined over a subring of a ring S, and F and K are field extensions of S.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFieldFieldDecidableEqDecidableEqAlgebraAlgebraAlgebraIsScalarTower