comap_supp

Mathlib.RingTheory.Valuation.Quotient

URI: https://scilib.ai/kg/mathlib#AddValuation.comap_supp

English

The comap of a valuation under a ring hom preserves the support via comap.

Русский

Обратное отображение опоры через кольцо сохраняет опору через comap.

LaTeX

$$$\\mathrm{comap\_supp}(f) = \\mathrm{Ideal.comap}(f)(\\mathrm{supp}(v))$$$

Lean4

theorem comap_supp {S : Type*} [CommRing S] (f : S →+* R) : supp (v.comap f) = Ideal.comap f v.supp :=
  Valuation.comap_supp v f

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

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

Разделы

Аффилиация

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