baseChange_neg — Mathlib

English

Negation commutes with base change: under a base change f, the negation on the base-changed curve aligns with the base-changed negation.

Русский

Отрицание сохраняется при базовом изменении: изменение базиса согласуется с отрицанием на новой базе.

LaTeX

$$$(W'.baseChange B).toProjective.neg (f \\circ P) = f \\circ (W'.baseChange A).toProjective.neg P$$$

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).toProjective.neg (f ∘ P) = f ∘ (W'.baseChange A).toProjective.neg P := by
  rw [← RingHom.coe_coe, ← WeierstrassCurve.Projective.map_neg, map_baseChange]

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