le_comap_map — Mathlib

English

For surjective f, map f preserves arbitrary infima: map f (⨅ i, p_i) = ⨅ i, map f (p_i).

Русский

При сюръективности f отображение сохраняет произвольный infimum: map f (⋂_i p_i) = ⋂_i map f(p_i).

LaTeX

$$$\operatorname{map} f \left( \bigwedge_{i} p_i \right) = \bigwedge_{i} \operatorname{map} f (p_i)$$$

Lean4

theorem le_comap_map [RingHomSurjective σ₁₂] (f : F) (p : Submodule R M) : p ≤ comap f (map f p) :=
  (gc_map_comap f).le_u_l _

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