feat(RingTheory/DualNumber): dual numbers over a field are local and …

…PIR (#17317)

Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Yakov Pechersky <[email protected]>

Mathlib.lean

@@ -3884,6 +3884,7 @@ import Mathlib.RingTheory.Derivation.ToSquareZero
 import Mathlib.RingTheory.DiscreteValuationRing.Basic
 import Mathlib.RingTheory.DiscreteValuationRing.TFAE
 import Mathlib.RingTheory.Discriminant
+import Mathlib.RingTheory.DualNumber
 import Mathlib.RingTheory.EisensteinCriterion
 import Mathlib.RingTheory.EssentialFiniteness
 import Mathlib.RingTheory.Etale.Basic

Mathlib/Algebra/TrivSqZeroExt.lean

@@ -147,6 +147,12 @@ theorem snd_comp_inr [Zero R] : snd ∘ (inr : M → tsze R M) = id :=
 
 end
 
+theorem fst_surjective [Nonempty M] : Function.Surjective (fst : tsze R M → R) :=
+  Prod.fst_surjective
+
+theorem snd_surjective [Nonempty R] : Function.Surjective (snd : tsze R M → M) :=
+  Prod.snd_surjective
+
 theorem inl_injective [Zero M] : Function.Injective (inl : R → tsze R M) :=
   Function.LeftInverse.injective <| fst_inl _
 
@@ -226,6 +232,16 @@ instance module [Semiring S] [AddCommMonoid R] [AddCommMonoid M] [Module S R] [M
     Module S (tsze R M) :=
   Prod.instModule
 
+/-- The trivial square-zero extension is nontrivial if it is over a nontrivial ring. -/
+instance instNontrivial_of_left {R M : Type*} [Nontrivial R] [Nonempty M] :
+    Nontrivial (TrivSqZeroExt R M) :=
+  fst_surjective.nontrivial
+
+/-- The trivial square-zero extension is nontrivial if it is over a nontrivial module. -/
+instance instNontrivial_of_right {R M : Type*} [Nonempty R] [Nontrivial M] :
+    Nontrivial (TrivSqZeroExt R M) :=
+  snd_surjective.nontrivial
+
 @[simp]
 theorem fst_zero [Zero R] [Zero M] : (0 : tsze R M).fst = 0 :=
   rfl

Mathlib/RingTheory/DualNumber.lean

@@ -0,0 +1,168 @@
+/-
+Copyright (c) 2024 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+-/
+import Mathlib.Algebra.DualNumber
+import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
+
+/-!
+# Algebraic properties of dual numbers
+
+## Main results
+
+* `DualNumber.instLocalRing`: The dual numbers over a field `K` form a local ring.
+* `DualNumber.instPrincipalIdealRing`: The dual numbers over a field `K` form a principal ideal
+  ring.
+
+-/
+
+namespace TrivSqZeroExt
+
+variable {R M : Type*}
+
+section Semiring
+variable [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
+
+lemma isNilpotent_iff_isNilpotent_fst {x : TrivSqZeroExt R M} :
+    IsNilpotent x ↔ IsNilpotent x.fst := by
+  constructor <;> rintro ⟨n, hn⟩
+  · refine ⟨n, ?_⟩
+    rw [← fst_pow, hn, fst_zero]
+  · refine ⟨n * 2, ?_⟩
+    rw [pow_mul]
+    ext
+    · rw [fst_pow, fst_pow, hn, zero_pow two_ne_zero, fst_zero]
+    · rw [pow_two, snd_mul, fst_pow, hn, MulOpposite.op_zero, zero_smul, zero_smul, zero_add,
+        snd_zero]
+
+@[simp]
+lemma isNilpotent_inl_iff (r : R) : IsNilpotent (.inl r : TrivSqZeroExt R M) ↔ IsNilpotent r := by
+  rw [isNilpotent_iff_isNilpotent_fst, fst_inl]
+
+@[simp]
+lemma isNilpotent_inr (x : M) : IsNilpotent (.inr x : TrivSqZeroExt R M) := by
+  refine ⟨2, by simp [pow_two]⟩
+
+end Semiring
+
+lemma isUnit_or_isNilpotent_of_isMaximal_isNilpotent [CommSemiring R] [AddCommGroup M]
+    [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M]
+    (h : ∀ I : Ideal R, I.IsMaximal → IsNilpotent I)
+    (a : TrivSqZeroExt R M) :
+    IsUnit a ∨ IsNilpotent a := by
+  rw [isUnit_iff_isUnit_fst, isNilpotent_iff_isNilpotent_fst]
+  refine (em _).imp_right fun ha ↦ ?_
+  obtain ⟨I, hI, haI⟩ := exists_max_ideal_of_mem_nonunits (mem_nonunits_iff.mpr ha)
+  refine (h _ hI).imp fun n hn ↦ ?_
+  exact hn.le (Ideal.pow_mem_pow haI _)
+
+lemma isUnit_or_isNilpotent [DivisionSemiring R] [AddCommGroup M]
+    [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
+    (a : TrivSqZeroExt R M) :
+    IsUnit a ∨ IsNilpotent a := by
+  simp [isUnit_iff_isUnit_fst, isNilpotent_iff_isNilpotent_fst, em']
+
+end TrivSqZeroExt
+
+namespace DualNumber
+variable {R : Type*}
+
+lemma fst_eq_zero_iff_eps_dvd [Semiring R] {x : R[ε]} :
+    x.fst = 0 ↔ ε ∣ x := by
+  simp_rw [dvd_def, TrivSqZeroExt.ext_iff, TrivSqZeroExt.fst_mul, TrivSqZeroExt.snd_mul,
+    fst_eps, snd_eps, zero_mul, zero_smul, zero_add, MulOpposite.smul_eq_mul_unop,
+    MulOpposite.unop_op, one_mul, exists_and_left, iff_self_and]
+  intro
+  exact ⟨.inl x.snd, rfl⟩
+
+lemma isNilpotent_eps [Semiring R] :
+    IsNilpotent (ε : R[ε]) :=
+  TrivSqZeroExt.isNilpotent_inr 1
+
+open TrivSqZeroExt
+
+lemma isNilpotent_iff_eps_dvd [DivisionSemiring R] {x : R[ε]} :
+    IsNilpotent x ↔ ε ∣ x := by
+  simp only [isNilpotent_iff_isNilpotent_fst, isNilpotent_iff_eq_zero, fst_eq_zero_iff_eps_dvd]
+
+section Field
+
+variable {K : Type*}
+
+instance [DivisionRing K] : LocalRing K[ε] where
+  isUnit_or_isUnit_of_add_one {a b} h := by
+    rw [add_comm, ← eq_sub_iff_add_eq] at h
+    rcases eq_or_ne (fst a) 0 with ha|ha <;>
+    simp [isUnit_iff_isUnit_fst, h, ha]
+
+lemma 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
+
+lemma isMaximal_span_singleton_eps [DivisionRing K] :
+    (Ideal.span {ε} : Ideal K[ε]).IsMaximal := by
+  refine ⟨?_, fun I hI ↦ ?_⟩
+  · simp [ne_eq, Ideal.eq_top_iff_one, Ideal.mem_span_singleton', TrivSqZeroExt.ext_iff]
+  · rcases ideal_trichotomy I with rfl|rfl|rfl <;>
+    first | simp at hI | simp
+
+lemma maximalIdeal_eq_span_singleton_eps [Field K] :
+    LocalRing.maximalIdeal K[ε] = Ideal.span {ε} :=
+  (LocalRing.eq_maximalIdeal isMaximal_span_singleton_eps).symm
+
+instance [DivisionRing K] : IsPrincipalIdealRing K[ε] where
+  principal I := by
+    rcases ideal_trichotomy I with rfl|rfl|rfl
+    · exact bot_isPrincipal
+    · exact ⟨_, rfl⟩
+    · exact top_isPrincipal
+
+lemma exists_mul_left_or_mul_right [DivisionRing K] (a b : K[ε]) :
+    ∃ c, a * c = b ∨ b * c = a := by
+  rcases isUnit_or_isNilpotent a with ha|ha
+  · lift a to K[ε]ˣ using ha
+    exact ⟨a⁻¹ * b, by simp⟩
+  rcases isUnit_or_isNilpotent b with hb|hb
+  · lift b to K[ε]ˣ using hb
+    exact ⟨b⁻¹ * a, by simp⟩
+  rw [isNilpotent_iff_eps_dvd] at ha hb
+  obtain ⟨x, rfl⟩ := ha
+  obtain ⟨y, rfl⟩ := hb
+  suffices ∃ c, fst x * fst c = fst y ∨ fst y * fst c = fst x by
+    simpa [TrivSqZeroExt.ext_iff] using this
+  rcases eq_or_ne (fst x) 0 with hx|hx
+  · refine ⟨ε, Or.inr ?_⟩
+    simp [hx]
+  refine ⟨inl ((fst x)⁻¹ * fst y), ?_⟩
+  simp [← inl_mul, ← mul_assoc, mul_inv_cancel₀ hx]
+
+end Field
+
+end DualNumber

Mathlib/RingTheory/Nilpotent/Basic.lean

@@ -82,6 +82,15 @@ theorem IsNilpotent.isUnit_add_right_of_commute [Ring R] {r u : R}
     IsUnit (r + u) :=
   add_comm r u ▸ hnil.isUnit_add_left_of_commute hu h_comm
 
+lemma IsUnit.not_isNilpotent [Ring R] [Nontrivial R] {x : R} (hx : IsUnit x) :
+    ¬ IsNilpotent x := by
+  intro H
+  simpa using H.isUnit_add_right_of_commute hx.neg (by simp)
+
+lemma IsNilpotent.not_isUnit [Ring R] [Nontrivial R] {x : R} (hx : IsNilpotent x) :
+    ¬ IsUnit x :=
+  mt IsUnit.not_isNilpotent (by simpa only [not_not] using hx)
+
 instance [Zero R] [Pow R ℕ] [Zero S] [Pow S ℕ] [IsReduced R] [IsReduced S] : IsReduced (R × S) where
   eq_zero _ := fun ⟨n, hn⟩ ↦ have hn := Prod.ext_iff.1 hn
     Prod.ext (IsReduced.eq_zero _ ⟨n, hn.1⟩) (IsReduced.eq_zero _ ⟨n, hn.2⟩)