supportDim_le_of_injective — Mathlib

English

Let f: M →_R N be an injective linear map. Then the support dimension does not increase: sdim_R(M) ≤ sdim_R(N).

Русский

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

LaTeX

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

Lean4

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

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