English
Under Noetherian, local, and domain hypotheses, if the maximal ideal is principal, every nonzero ideal I equals a power of the maximal ideal: I = m^n for some n ∈ ℕ.
Русский
При условиях Noetherian, локальности и домена, если максимальный идеал порожден одним элементом, каждый ненулевой идеал I равен степени максимального идеала: I = m^n.
LaTeX
$$∃ n ∈ ℕ, I = maximalIdeal(R) ^ n$$
Lean4
theorem exists_maximalIdeal_pow_eq_of_principal [IsNoetherianRing R] [IsLocalRing R] [IsDomain R]
(h' : (maximalIdeal R).IsPrincipal) (I : Ideal R) (hI : I ≠ ⊥) : ∃ n : ℕ, I = maximalIdeal R ^ n :=
by
by_cases h : IsField R
· let _ := h.toField
exact ⟨0, by simp [(eq_bot_or_eq_top I).resolve_left hI]⟩
classical
obtain ⟨x, hx : _ = Ideal.span _⟩ := h'
by_cases hI' : I = ⊤
· use 0; rw [pow_zero, hI', Ideal.one_eq_top]
have H : ∀ r : R, ¬IsUnit r ↔ x ∣ r := fun r => (SetLike.ext_iff.mp hx r).trans Ideal.mem_span_singleton
have : x ≠ 0 := by
rintro rfl
apply Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h
simp [hx]
have hx' := IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal x this hx
have H' : ∀ r : R, r ≠ 0 → r ∈ nonunits R → ∃ n : ℕ, Associated (x ^ n) r :=
by
intro r hr₁ hr₂
obtain ⟨f, hf₁, rfl, hf₂⟩ := (WfDvdMonoid.not_unit_iff_exists_factors_eq r hr₁).mp hr₂
have : ∀ b ∈ f, Associated x b := by
intro b hb
exact Irreducible.associated_of_dvd hx' (hf₁ b hb) ((H b).mp (hf₁ b hb).1)
clear hr₁ hr₂ hf₁
induction f using Multiset.induction with
| empty => exact (hf₂ rfl).elim
| cons fa fs fh => ?_
rcases eq_or_ne fs ∅ with (rfl | hf')
· use 1
rw [pow_one, Multiset.prod_cons, Multiset.empty_eq_zero, Multiset.prod_zero, mul_one]
exact this _ (Multiset.mem_cons_self _ _)
· obtain ⟨n, hn⟩ := fh hf' fun b hb => this _ (Multiset.mem_cons_of_mem hb)
use n + 1
rw [pow_add, Multiset.prod_cons, mul_comm, pow_one]
exact Associated.mul_mul (this _ (Multiset.mem_cons_self _ _)) hn
have : ∃ n : ℕ, x ^ n ∈ I :=
by
obtain ⟨r, hr₁, hr₂⟩ : ∃ r : R, r ∈ I ∧ r ≠ 0 := by by_contra! h; apply hI; rw [eq_bot_iff]; exact h
obtain ⟨n, u, rfl⟩ := H' r hr₂ (le_maximalIdeal hI' hr₁)
use n
rwa [← I.unit_mul_mem_iff_mem u.isUnit, mul_comm]
use Nat.find this
apply le_antisymm
· change ∀ s ∈ I, s ∈ _
by_contra! hI''
obtain ⟨s, hs₁, hs₂⟩ := hI''
apply hs₂
by_cases hs₃ : s = 0; · rw [hs₃]; exact zero_mem _
obtain ⟨n, u, rfl⟩ := H' s hs₃ (le_maximalIdeal hI' hs₁)
rw [mul_comm, Ideal.unit_mul_mem_iff_mem _ u.isUnit] at hs₁ ⊢
apply Ideal.pow_le_pow_right (Nat.find_min' this hs₁)
apply Ideal.pow_mem_pow
exact (H _).mpr (dvd_refl _)
· rw [hx, Ideal.span_singleton_pow, Ideal.span_le, Set.singleton_subset_iff]
exact Nat.find_spec this
