map_add — Mathlib

English

Negation commutes with base change of Jacobians and addition maps under compatible algebra structures.

Русский

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

LaTeX

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

Lean4

@[simp]
protected theorem map_add (f : F →+* K) {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) :
    (W.map f).toJacobian.add (f ∘ P) (f ∘ Q) = f ∘ W.add P Q :=
  by
  by_cases h : P ≈ Q
  · rw [add_of_equiv <| (comp_equiv_comp f hP hQ).mpr h, add_of_equiv h, map_dblXYZ]
  · rw [add_of_not_equiv <| h.comp (comp_equiv_comp f hP hQ).mp, add_of_not_equiv h, map_addXYZ]

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