specTargetImageRingHom_surjective

Mathlib.AlgebraicGeometry.AffineScheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.specTargetImageRingHom_surjective

English

The appTop map of the factorization f → Spec A is injective.

Русский

По факторизации f → Spec A отображение appTop инъективно.

LaTeX

$$$ \text{Injective} \left| (\mathrm{specTargetImageFactorization} f).appTop \right.$$$

Lean4

theorem specTargetImageRingHom_surjective : Function.Surjective (specTargetImageRingHom f) :=
  Ideal.Quotient.mk_surjective

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru