English
Assume the value group is cyclic and nontrivial. Then every ideal I in the ring K₀ is principal; equivalently, the ring is a principal ideal ring.
Русский
Пусть значение группы циклично и не тривиально. Тогда любой идеал I в кольце K₀ является главной, то есть кольцо является кольцом главных идеалов.
LaTeX
$$$ [IsCyclic (valueGroup\\ v)] \\land [Nontrivial (valueGroup\\ v)] \\Rightarrow (\\forall I \\in \\mathrm{Ideal}(K_0),\\ I\\text{ is principal}).$$$
Lean4
theorem ideal_isPrincipal [IsCyclic (valueGroup v)] [Nontrivial (valueGroup v)] (I : Ideal K₀) : I.IsPrincipal :=
by
suffices ∀ P : Ideal K₀, P.IsPrime → Submodule.IsPrincipal P by exact (IsPrincipalIdealRing.of_prime this).principal I
intro P hP
by_cases h_ne_bot : P = ⊥
· rw [h_ne_bot]; exact bot_isPrincipal
· let π : Uniformizer v := Nonempty.some (by infer_instance)
obtain ⟨x, ⟨hx_mem, hx₀⟩⟩ := Submodule.exists_mem_ne_zero_of_ne_bot h_ne_bot
obtain ⟨n, ⟨u, hu⟩⟩ := exists_pow_Uniformizer hx₀ π
by_cases hn : n = 0
· rw [← Subring.coe_mul, hn, pow_zero, one_mul, SetLike.coe_eq_coe] at hu
refine (hP.ne_top (Ideal.eq_top_of_isUnit_mem P hx_mem ?_)).elim
simp only [hu, Units.isUnit]
· rw [← Subring.coe_mul, SetLike.coe_eq_coe] at hu
rw [hu, Ideal.mul_unit_mem_iff_mem P u.isUnit, IsPrime.pow_mem_iff_mem hP _ (pos_iff_ne_zero.mpr hn), ←
Ideal.span_singleton_le_iff_mem, ← π.is_generator] at hx_mem
rw [← Ideal.IsMaximal.eq_of_le (IsLocalRing.maximalIdeal.isMaximal K₀) hP.ne_top hx_mem]
exact ⟨π.1, π.is_generator⟩
