range_comap_of_surjective

Mathlib.RingTheory.Spectrum.Prime.Topology

URI: https://scilib.ai/kg/mathlib#PrimeSpectrum.range_comap_of_surjective

English

For surjective f, the range of comap f equals the zero locus of the kernel of f.

Русский

Для сюрьективного f образ comap f равен нильрадикалу ker f.

LaTeX

$$range_comap_of_surjective hf : Set.range (comap f) = zeroLocus (ker f).$$

Lean4

theorem range_comap_of_surjective (hf : Surjective f) : Set.range (comap f) = zeroLocus (ker f) :=
  range_specComap_of_surjective _ f hf

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

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

Разделы

Аффилиация

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