baseChange_add — Mathlib

English

The addition operation is compatible with base change for Jacobians under compatible algebra maps.

Русский

Сложение совместимо с переносом по основанию для Якобианов при совместимых отображениях алгебры.

LaTeX

$$$ (W'.baseChange F).toJacobian.add P Q = f \\circ (W'.baseChange F).toJacobian.add P Q $$$

Lean4

theorem baseChange_add [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K]
    [IsScalarTower R S K] (f : F →ₐ[S] K) {P Q : Fin 3 → F} (hP : (W'.baseChange F).toJacobian.Nonsingular P)
    (hQ : (W'.baseChange F).toJacobian.Nonsingular Q) :
    (W'.baseChange K).toJacobian.add (f ∘ P) (f ∘ Q) = f ∘ (W'.baseChange F).toJacobian.add P Q := by
  rw [← RingHom.coe_coe, ← WeierstrassCurve.Jacobian.map_add _ hP hQ, map_baseChange]

Похожие утверждения