krullDimLE_one — Mathlib

English

In a principal ideal domain that is not a field, the Krull dimension is at most 1: ringKrullDim R ≤ 1.

Русский

В главном кольце идеалов (PID), не являющемся полем, размерность Крулля не превышает 1: ringKrullDim R ≤ 1.

LaTeX

$$$\\operatorname{ringKrullDim} R \\le 1$$$

Lean4

instance krullDimLE_one (R : Type*) [CommRing R] [IsPrincipalIdealRing R] : Ring.KrullDimLE 1 R :=
  by
  refine Ring.krullDimLE_one_iff.2 fun I hI ↦ or_iff_not_imp_left.2 fun hI' ↦ ?_
  rw [minimalPrimes_eq_minimals, Set.notMem_setOf_iff, not_minimal_iff_exists_lt hI] at hI'
  obtain ⟨P, hlt, hP⟩ := hI'
  have := IsPrincipalIdealRing.of_surjective (Ideal.Quotient.mk P) Ideal.Quotient.mk_surjective
  have : (I.map (Ideal.Quotient.mk P)).IsMaximal :=
    by
    have :=
      Ideal.map_isPrime_of_surjective (f := Ideal.Quotient.mk P) Ideal.Quotient.mk_surjective (I := I)
        (by simpa using hlt.le)
    refine IsPrime.to_maximal_ideal ?_
    rw [ne_eq, Ideal.map_eq_bot_iff_le_ker, Ideal.mk_ker]
    exact hlt.not_ge
  have :=
    Ideal.comap_isMaximal_of_surjective (Ideal.Quotient.mk P) Ideal.Quotient.mk_surjective (K :=
      I.map (Ideal.Quotient.mk P))
  simpa [Ideal.comap_map_of_surjective' (Ideal.Quotient.mk P) Ideal.Quotient.mk_surjective, hlt.le] using this

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