map_neg — Mathlib

English

Under a ring homomorphism f, the negation on projective points commutes with map: map_neg(W', f) respects negation.

Русский

При отображении кольца через односвязное отображение f, отрицание на проективных точках сохраняется через отображение.

LaTeX

$$$(W'.map f).toProjective.neg (f \\circ P) = f \\circ W'.neg P$$$

Lean4

@[simp]
protected theorem map_neg (f : R →+* S) (P : Fin 3 → R) : (W'.map f).toProjective.neg (f ∘ P) = f ∘ W'.neg P :=
  by
  simp only [neg, map_negY, comp_fin3]
  map_simp

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