English
For a Noetherian local domain not a field, the following are equivalent: DVR, valuation ring, Dedekind domain, integrally closed with a single nonzero prime, maximal ideal principal, cotangent dimension equals 1, every nonzero ideal is a power of the maximal ideal.
Русский
Для Noetherian локального домена, не являющегося полем, эквивалентны: DVR, оценочное кольцо, Дедекиндово кольцо, интегрированно замкнутое с единственной ненулевой простотой, максимальный идеал порожден одним элементом, размерность cotangent пространства равна 1, каждый ненулевой идеал — степень максимального идеала.
LaTeX
$$tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain$$
Lean4
theorem maximalIdeal_isPrincipal_of_isDedekindDomain [IsLocalRing R] [IsDomain R] [IsDedekindDomain R] :
(maximalIdeal R).IsPrincipal := by
classical
by_cases ne_bot : maximalIdeal R = ⊥
· rw [ne_bot]; infer_instance
obtain ⟨a, ha₁, ha₂⟩ : ∃ a ∈ maximalIdeal R, a ≠ (0 : R) := by by_contra! h'; apply ne_bot; rwa [eq_bot_iff]
have hle : Ideal.span { a } ≤ maximalIdeal R := by rwa [Ideal.span_le, Set.singleton_subset_iff]
have : (Ideal.span { a }).radical = maximalIdeal R :=
by
rw [Ideal.radical_eq_sInf]
apply le_antisymm
· exact sInf_le ⟨hle, inferInstance⟩
· refine le_sInf fun I hI => (eq_maximalIdeal <| hI.2.isMaximal (fun e => ha₂ ?_)).ge
rw [← Ideal.span_singleton_eq_bot, eq_bot_iff, ← e]; exact hI.1
have : ∃ n, maximalIdeal R ^ n ≤ Ideal.span { a } := by rw [← this]; apply Ideal.exists_radical_pow_le_of_fg;
exact IsNoetherian.noetherian _
rcases hn : Nat.find this with - | n
· have := Nat.find_spec this
rw [hn, pow_zero, Ideal.one_eq_top] at this
exact (Ideal.IsMaximal.ne_top inferInstance (eq_top_iff.mpr <| this.trans hle)).elim
obtain ⟨b, hb₁, hb₂⟩ : ∃ b ∈ maximalIdeal R ^ n, b ∉ Ideal.span { a } := by by_contra! h'; rw [Nat.find_eq_iff] at hn;
exact hn.2 n n.lt_succ_self fun x hx => h' x hx
have hb₃ : ∀ m ∈ maximalIdeal R, ∃ k : R, k * a = b * m :=
by
intro m hm; rw [← Ideal.mem_span_singleton']; apply Nat.find_spec this
rw [hn, pow_succ]; exact Ideal.mul_mem_mul hb₁ hm
have hb₄ : b ≠ 0 := by rintro rfl; apply hb₂; exact zero_mem _
let K := FractionRing R
let x : K := algebraMap R K b / algebraMap R K a
let M := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
have ha₃ : algebraMap R K a ≠ 0 := IsFractionRing.to_map_eq_zero_iff.not.mpr ha₂
by_cases hx : ∀ y ∈ M, x * y ∈ M
· have := isIntegral_of_smul_mem_submodule M ?_ ?_ x hx
· obtain ⟨y, e⟩ := IsIntegrallyClosed.algebraMap_eq_of_integral this
refine (hb₂ (Ideal.mem_span_singleton'.mpr ⟨y, ?_⟩)).elim
apply IsFractionRing.injective R K
rw [map_mul, e, div_mul_cancel₀ _ ha₃]
· rw [Submodule.ne_bot_iff]; refine ⟨_, ⟨a, ha₁, rfl⟩, ?_⟩
exact (IsFractionRing.to_map_eq_zero_iff (K := K)).not.mpr ha₂
· apply Submodule.FG.map; exact IsNoetherian.noetherian _
· have : (M.map (DistribMulAction.toLinearMap R K x)).comap (Algebra.linearMap R K) = ⊤ :=
by
by_contra h; apply hx
rintro m' ⟨m, hm, rfl : algebraMap R K m = m'⟩
obtain ⟨k, hk⟩ := hb₃ m hm
have hk' : x * algebraMap R K m = algebraMap R K k := by
rw [← mul_div_right_comm, ← map_mul, ← hk, map_mul, mul_div_cancel_right₀ _ ha₃]
exact ⟨k, le_maximalIdeal h ⟨_, ⟨_, hm, rfl⟩, hk'⟩, hk'.symm⟩
obtain ⟨y, hy₁, hy₂⟩ : ∃ y ∈ maximalIdeal R, b * y = a :=
by
rw [Ideal.eq_top_iff_one, Submodule.mem_comap] at this
obtain ⟨_, ⟨y, hy, rfl⟩, hy' : x * algebraMap R K y = algebraMap R K 1⟩ := this
rw [map_one, ← mul_div_right_comm, div_eq_one_iff_eq ha₃, ← map_mul] at hy'
exact ⟨y, hy, IsFractionRing.injective R K hy'⟩
refine ⟨⟨y, ?_⟩⟩
apply le_antisymm
· intro m hm; obtain ⟨k, hk⟩ := hb₃ m hm; rw [← hy₂, mul_comm, mul_assoc] at hk
rw [← mul_left_cancel₀ hb₄ hk, mul_comm]; exact Ideal.mem_span_singleton'.mpr ⟨_, rfl⟩
· rwa [Submodule.span_le, Set.singleton_subset_iff]
