Theorems · Theorem · algebraic geometry

WeierstrassCurve.Affine.Point.map_map

∀ {R : Type r} {S : Type s} {F : Type u} {K : Type v} {L : Type w} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Field F] [inst_3 : Field K] [inst_4 : Field L] {W' : WeierstrassCurve.Affine R} [inst_5 : DecidableEq F]
  [inst_6 : DecidableEq K] [inst_7 : DecidableEq L] [inst_8 : Algebra R S] [inst_9 : Algebra R F]
  [inst_10 : Algebra S F] [inst_11 : IsScalarTower R S F] [inst_12 : Algebra R K] [inst_13 : Algebra S K]
  [inst_14 : IsScalarTower R S K] [inst_15 : Algebra R L] [inst_16 : Algebra S L] [inst_17 : IsScalarTower R S L]
  (f : F →ₐ[S] K) (g : K →ₐ[S] L) (P : (W'.baseChange F).Point),
  (WeierstrassCurve.Affine.Point.map g) ((WeierstrassCurve.Affine.Point.map f) P) =
    (WeierstrassCurve.Affine.Point.map (g.comp f)) P

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

CommRingCommRingFieldFieldFieldDecidableEqDecidableEqDecidableEqAlgebraAlgebraAlgebraIsScalarTowerAlgebraAlgebraIsScalarTowerAlgebraAlgebraIsScalarTower