map_add — Mathlib

English

Under a ring homomorphism f, the addition commutes with map: map_add(W,f) preserves addition.

Русский

При отображении кольца через отображение f сложение сохраняется: map_add(W,f) сохраняет сложение.

LaTeX

$$$(W.map f).toProjective.add (f \\circ P) (f \\circ Q) = f \\circ W.add P Q$$$

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).toProjective.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]

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