Theorems · Theorem · algebraic geometry

WeierstrassCurve.map_baseChange

∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {S : Type s} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {A : Type v} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : Type w}
  [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B] (g : A →ₐ[S] B),
  (W.baseChange A).map ↑g = W.baseChange B

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Cited by

14 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebraIsScalarTowerCommRingAlgebraAlgebraIsScalarTower