comap_map_eq — Mathlib

English

Let f: M → M₂ be a Lie-module hom with kernel zero. Then for every LieSubmodule N ⊆ M, the preimage of the image of N equals N; equivalently comap f (map f N) = N.

Русский

Пусть f: M → M₂ — гомоморфизм Ли-модулей с ядром {0}. Тогда для любого подмодуля N ⊆ M выполнено, что прообраз образа равен самому N; то есть comap f (map f N) = N.

LaTeX

$$$$\ker f = \{0\} \Rightarrow f^{-1}(f(N)) = N.$$$$

Lean4

theorem comap_map_eq (hf : f.ker = ⊥) : comap f (map f N) = N :=
  by
  rw [SetLike.ext'_iff]
  exact (N : Set M).preimage_image_eq (f.ker_eq_bot.mp hf)

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