quotient_artinian_of_mem_minimalPrimes_of_isLocalRing

English

In a local Noetherian ring R, if a maximal ideal is among the minimal primes over I, then R/I is Artinian.

Русский

В локальном кольце Ноetherian R, если максимальный идеал лежит среди минимальных идей над I, то R/I является артинановым.

LaTeX

$$$\text{IsArtinianRing}(R/ I)$$$

Lean4

theorem quotient_artinian_of_mem_minimalPrimes_of_isLocalRing [IsLocalRing R] (I : Ideal R)
    (hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes) : IsArtinianRing (R ⧸ I) :=
  have : Ring.KrullDimLE 0 (R ⧸ I) :=
    Ring.krullDimLE_zero_iff.mpr fun J prime ↦
      Ideal.isMaximal_of_isIntegral_of_isMaximal_comap _ <|
        by
        convert IsLocalRing.maximalIdeal.isMaximal R
        rw [Ideal.minimalPrimes, Set.mem_setOf] at hp
        have := prime.comap (Ideal.Quotient.mk I)
        exact hp.eq_of_le ⟨this, .trans (by simp) (Ideal.ker_le_comap _)⟩ (le_maximalIdeal this.1)
  IsNoetherianRing.isArtinianRing_of_krullDimLE_zero

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