map_iInf_of_ker_le — Mathlib

English

If ker f ≤ ⨅ i, p_i, then map f (⨅ i, p_i) = ⨅ i, map f(p_i).

Русский

Если ker f ≤ ⨅ i, p_i, то map f(⨅ i, p_i) = ⨅ i, map f(p_i).

LaTeX

$$$\operatorname{map}_f\Bigl(\bigwedge_i p_i\Bigr) = \bigwedge_i \operatorname{map}_f(p_i)$$$

Lean4

theorem map_iInf_of_ker_le {f : F} (hf : Surjective f) {ι} {p : ι → Submodule R M} (h : LinearMap.ker f ≤ ⨅ i, p i) :
    map f (⨅ i, p i) = ⨅ i, map f (p i) :=
  by
  conv_rhs => rw [← map_comap_eq_of_surjective hf (⨅ _, _), comap_iInf]
  simp_rw [fun i ↦ comap_map_eq_self (le_iInf_iff.mp h i)]

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