English
IsDedekindDomainInv A implies Krull dimension of A is at most one.
Русский
IsDedekindDomainInv A влечет за собой, что размерность Круля не превышает единицу.
LaTeX
$$$$\\dim(A) \\le 1.$$$$
Lean4
theorem dimensionLEOne : DimensionLEOne A :=
⟨by
-- We're going to show that `P` is maximal because any (maximal) ideal `M`
-- that is strictly larger would be `⊤`.
rintro P P_ne hP
refine
Ideal.isMaximal_def.mpr
⟨hP.ne_top, fun M hM => ?_⟩
-- We may assume `P` and `M` (as fractional ideals) are nonzero.
have P'_ne : (P : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr P_ne
have M'_ne : (M : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hM.ne_bot
suffices (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ P
by
rw [eq_top_iff, ← coeIdeal_le_coeIdeal (FractionRing A), coeIdeal_top]
calc
(1 : FractionalIdeal A⁰ (FractionRing A)) = _ * _ * _ := ?_
_ ≤ _ * _ :=
(mul_right_mono ((P : FractionalIdeal A⁰ (FractionRing A))⁻¹ * M : FractionalIdeal A⁰ (FractionRing A)) this)
_ = M := ?_
·
rw [mul_assoc, ← mul_assoc (P : FractionalIdeal A⁰ (FractionRing A)), h.mul_inv_eq_one P'_ne, one_mul,
h.inv_mul_eq_one M'_ne]
·
rw [← mul_assoc (P : FractionalIdeal A⁰ (FractionRing A)), h.mul_inv_eq_one P'_ne, one_mul]
-- Suppose we have `x ∈ M⁻¹ * P`, then in fact `x = algebraMap _ _ y` for some `y`.
intro x hx
have le_one : (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ 1 :=
by
rw [← h.inv_mul_eq_one M'_ne]
exact mul_left_mono _ ((coeIdeal_le_coeIdeal (FractionRing A)).mpr hM.le)
obtain ⟨y, _hy, rfl⟩ :=
(mem_coeIdeal _).mp
(le_one hx)
-- Since `M` is strictly greater than `P`, let `z ∈ M \ P`.
obtain ⟨z, hzM, hzp⟩ := SetLike.exists_of_lt hM
have zy_mem := mul_mem_mul (mem_coeIdeal_of_mem A⁰ hzM) hx
rw [← RingHom.map_mul, ← mul_assoc, h.mul_inv_eq_one M'_ne, one_mul] at zy_mem
obtain ⟨zy, hzy, zy_eq⟩ := (mem_coeIdeal A⁰).mp zy_mem
rw [IsFractionRing.injective A (FractionRing A) zy_eq] at hzy
exact mem_coeIdeal_of_mem A⁰ (Or.resolve_left (hP.mem_or_mem hzy) hzp)⟩
