ringKrullDim_le_of_surjective — Mathlib

English

If f : R →+* S is surjective, then ringKrullDim S ≤ ringKrullDim R.

Русский

Если отображение окружений R →+* S сюръективно, то ringKrullDim S ≤ ringKrullDim R.

LaTeX

$$$ringKrullDim S \\le ringKrullDim R$$$

Lean4

/-- If `f : R →+* S` is surjective, then `ringKrullDim S ≤ ringKrullDim R`. -/
theorem ringKrullDim_le_of_surjective (f : R →+* S) (hf : Function.Surjective f) : ringKrullDim S ≤ ringKrullDim R :=
  krullDim_le_of_strictMono (fun I ↦ ⟨Ideal.comap f I.asIdeal, inferInstance⟩)
    (Monotone.strictMono_of_injective (fun _ _ hab ↦ Ideal.comap_mono hab)
      (fun _ _ h => PrimeSpectrum.ext_iff.mpr <| Ideal.comap_injective_of_surjective f hf <| by simpa using h))

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