supportDim_le_of_surjective — Mathlib

English

Let f: M →_R N be surjective. Then the support dimension does not increase in the opposite direction: sdim_R(N) ≤ sdim_R(M).

Русский

Пусть f: M →_R N — сюръективное отображение. Тогда размерность поддержки не возрастает: sdim_R(N) ≤ sdim_R(M).

LaTeX

$$$\\operatorname{sdim}_R(N) \\le \\operatorname{sdim}_R(M)$$$

Lean4

theorem supportDim_le_of_surjective (f : M →ₗ[R] N) (h : Function.Surjective f) : supportDim R N ≤ supportDim R M :=
  krullDim_le_of_strictMono (fun a ↦ ⟨a.1, Module.support_subset_of_surjective f h a.2⟩) (fun {_ _} lt ↦ lt)

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