English
Let K be a division ring and consider the ring of dual numbers K[ε] with ε^2 = 0. Then every ideal I of K[ε] is either the zero ideal, the principal ideal generated by ε, or the whole ring.
Русский
Пусть K — деление кольцо, и рассмотрим кольцо двойственных чисел K[ε] с ε^2 = 0. Тогда любой идеал I в K[ε] равен либо нулевому идеалу, либо порожденному ε идеалу, либо всему кольцу.
LaTeX
$$$ I = \bot \lor I = \langle \varepsilon \rangle \lor I = \top $$$
Lean4
theorem ideal_trichotomy [DivisionRing K] (I : Ideal K[ε]) : I = ⊥ ∨ I = .span {ε} ∨ I = ⊤ :=
by
refine (eq_or_ne I ⊥).imp_right fun hb ↦ ?_
refine (eq_or_ne I ⊤).symm.imp_left fun ht ↦ ?_
have hd : ∀ x ∈ I, ε ∣ x := by
intro x hxI
rcases isUnit_or_isNilpotent x with hx | hx
· exact absurd (Ideal.eq_top_of_isUnit_mem _ hxI hx) ht
· rwa [← isNilpotent_iff_eps_dvd]
have hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x := by
intro x hxI hx0
obtain ⟨r, rfl⟩ := hd _ hxI
have : ε * r = (fst r) • ε := by ext <;> simp
rw [this] at hxI hx0 ⊢
have hr : fst r ≠ 0 := by
contrapose! hx0
simp [hx0]
refine ⟨r⁻¹, ?_⟩
simp [TrivSqZeroExt.ext_iff, inv_mul_cancel₀ hr]
refine le_antisymm ?_ ?_ <;> intro x <;>
simp_rw [Ideal.mem_span_singleton', (commute_eps_right _).eq, eq_comm, ← dvd_def]
· intro hx
simp_rw [hd _ hx]
· intro hx
obtain ⟨p, rfl⟩ := hx
obtain ⟨y, hyI, hy0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hb
obtain ⟨r, hr⟩ := hd' _ hyI hy0
rw [(commute_eps_left _).eq, hr, ← mul_assoc]
exact Ideal.mul_mem_left _ _ hyI
