comap_surjective_of_injective — Mathlib

English

Let f be an injective semilinear map (with the appropriate surjectivity on the ring hom). Then the map on submodules that sends a submodule of the domain to its image under f has the property that every submodule of the domain is the comap of some submodule of the codomain; equivalently, comap f is surjective on submodules.

Русский

Пусть f является инъективным полуприводом; тогда отображение подмодулов через образ подмодуля в области проображения охватывает всю решетку подмодулов: любому подмодулю p существует q такой, что comap f q = p.

LaTeX

$$$\forall p:\, Submodule\; R\; M, \exists q:\, Submodule\; R_2\; M_2,\ comap\ f\ q = p$$$

Lean4

theorem comap_surjective_of_injective : Function.Surjective (comap f) :=
  (gciMapComap hf).u_surjective

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