comap_surjective_of_injective — Mathlib

English

Let L be a language, M,N be L-structured sets, and f: M →[L] N an injective homomorphism. Then the pullback map comap f from substructures of N to substructures of M is surjective; i.e., for every L-substructure S of M there exists an L-substructure T of N such that comap f (T) = S.

Русский

Пусть L — язык, M и N — L-структуры, и f: M →[L] N — инъекция-гомоморфизм. Тогда отображение backward по f, comap f, из подструктур N на подструктуры M — сюръективно: для любой L-подструктуры S M существует L-подструктура T N такая, что comap f (T) = S.

LaTeX

$$$\forall S \in \mathrm{Sub}_L(M), \ exists\ T \in \mathrm{Sub}_L(N) \text{ with } \mathrm{comap}_f(T)=S,$ given that $f$ is injective.$$

Lean4

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

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