map_neg — Mathlib

English

Taking the comap along the negated map is the same as along the original map.

Русский

Обратный образ по отрицательному отображению совпадает с обратным образом по исходному отображению.

LaTeX

$$$\forall p:\, Submodule R M_2,\ comap\ (-f)\ p = comap\ f\ p$$$

Lean4

@[simp]
protected theorem map_neg (f : M →ₗ[R] M₂) : map (-f) p = map f p :=
  ext fun _ =>
    ⟨fun ⟨x, hx, hy⟩ => hy ▸ ⟨-x, show -x ∈ p from neg_mem hx, map_neg f x⟩, fun ⟨x, hx, hy⟩ =>
      hy ▸ ⟨-x, show -x ∈ p from neg_mem hx, (map_neg (-f) _).trans (neg_neg (f x))⟩⟩

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