baseChange_neg — Mathlib

English

Negation and base change commute in the Jacobian context under appropriate algebra maps.

Русский

Отрицание и перенос по основанию коммутируют в контексте Якобиана при соответствующих отображениях алгебры.

LaTeX

$$$\\text{baseChange neg} \\Rightarrow$ compatibility with map_neg under base change$$

Lean4

theorem baseChange_neg [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B]
    [IsScalarTower R S B] (f : A →ₐ[S] B) (P : Fin 3 → A) :
    (W'.baseChange B).toJacobian.neg (f ∘ P) = f ∘ (W'.baseChange A).toJacobian.neg P := by
  rw [← RingHom.coe_coe, ← WeierstrassCurve.Jacobian.map_neg, map_baseChange]

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