feat (RingTheory/PowerSeries): Add basic lemmas aiming at proving tha…

…t power series over a field are a DVR (#12160)

Add some basic lemmas about (univariate) power series over fields and their inverses, aiming at proving that they form a DVR.

Co-authored-by: María Inés de Frutos Fernández @mariainesdff

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -166,6 +166,10 @@ theorem ext_iff {φ ψ : R⟦X⟧} : φ = ψ ↔ ∀ n, coeff R n φ = coeff R n
   ⟨fun h n => congr_arg (coeff R n) h, ext⟩
 #align power_series.ext_iff PowerSeries.ext_iff
 
+instance [Subsingleton R] : Subsingleton R⟦X⟧ := by
+  simp only [subsingleton_iff, ext_iff]
+  exact fun _ _ _ ↦ (subsingleton_iff).mp (by infer_instance) _ _
+
 /-- Constructor for formal power series. -/
 def mk {R} (f : ℕ → R) : R⟦X⟧ := fun s => f (s ())
 #align power_series.mk PowerSeries.mk
@@ -261,6 +265,16 @@ theorem coeff_ne_zero_C {a : R} {n : ℕ} (h : n ≠ 0) : coeff R n (C R a) = 0
 theorem coeff_succ_C {a : R} {n : ℕ} : coeff R (n + 1) (C R a) = 0 :=
   coeff_ne_zero_C n.succ_ne_zero
 
+theorem C_injective : Function.Injective (C R) := by
+  intro a b H
+  have := (ext_iff (φ := C R a) (ψ := C R b)).mp H 0
+  rwa [coeff_zero_C, coeff_zero_C] at this
+
+protected theorem subsingleton_iff : Subsingleton R⟦X⟧ ↔ Subsingleton R := by
+  refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
+  rw [subsingleton_iff] at h ⊢
+  exact fun a b ↦ C_injective (h (C R a) (C R b))
+
 theorem X_eq : (X : R⟦X⟧) = monomial R 1 1 :=
   rfl
 set_option linter.uppercaseLean3 false in
@@ -400,6 +414,9 @@ theorem coeff_zero_X_mul (φ : R⟦X⟧) : coeff R 0 (X * φ) = 0 := by simp
 set_option linter.uppercaseLean3 false in
 #align power_series.coeff_zero_X_mul PowerSeries.coeff_zero_X_mul
 
+theorem constantCoeff_surj : Function.Surjective (constantCoeff R) :=
+  fun r => ⟨(C R) r, constantCoeff_C r⟩
+
 -- The following section duplicates the API of `Data.Polynomial.Coeff` and should attempt to keep
 -- up to date with that
 section
@@ -655,6 +672,19 @@ section CommRing
 
 variable {A : Type*} [CommRing A]
 
+theorem not_isField : ¬IsField A⟦X⟧ := by
+  by_cases hA : Subsingleton A
+  · exact not_isField_of_subsingleton _
+  · nontriviality A
+    rw [Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]
+    use Ideal.span {X}
+    constructor
+    · rw [bot_lt_iff_ne_bot, Ne.def, Ideal.span_singleton_eq_bot]
+      exact X_ne_zero
+    · rw [lt_top_iff_ne_top, Ne.def, Ideal.eq_top_iff_one, Ideal.mem_span_singleton,
+        X_dvd_iff, constantCoeff_one]
+      exact one_ne_zero
+
 @[simp]
 theorem rescale_X (a : A) : rescale a X = C A a * X := by
   ext
@@ -758,6 +788,9 @@ theorem X_prime : Prime (X : R⟦X⟧) := by
 set_option linter.uppercaseLean3 false in
 #align power_series.X_prime PowerSeries.X_prime
 
+/-- The variable of the power series ring over an integral domain is irreducible. -/
+theorem X_irreducible : Irreducible (X : R⟦X⟧) := X_prime.irreducible
+
 theorem rescale_injective {a : R} (ha : a ≠ 0) : Function.Injective (rescale a) := by
   intro p q h
   rw [PowerSeries.ext_iff] at *

Mathlib/RingTheory/PowerSeries/Inverse.lean

@@ -4,8 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Kenny Lau
 -/
 
-import Mathlib.RingTheory.PowerSeries.Basic
+import Mathlib.RingTheory.DedekindDomain.Basic
+import Mathlib.RingTheory.DiscreteValuationRing.Basic
 import Mathlib.RingTheory.MvPowerSeries.Inverse
+import Mathlib.RingTheory.PowerSeries.Basic
+import Mathlib.RingTheory.PowerSeries.Order
+
+
 
 #align_import ring_theory.power_series.basic from "leanprover-community/mathlib"@"2d5739b61641ee4e7e53eca5688a08f66f2e6a60"
 
@@ -18,6 +23,9 @@ the construction.)
 
 Formal (univariate) power series over a local ring form a local ring.
 
+Formal (univariate) power series over a field form a discrete valuation ring, and a normalization
+monoid. The definition `residueFieldOfPowerSeries` provides the isomorphism between the residue
+field of `k⟦X⟧` and `k`, when `k` is a field.
 
 -/
 
@@ -120,18 +128,17 @@ section Field
 variable {k : Type*} [Field k]
 
 /-- The inverse 1/f of a power series f defined over a field -/
-protected def inv : PowerSeries k → PowerSeries k :=
+protected def inv : k⟦X⟧ → k⟦X⟧ :=
   MvPowerSeries.inv
 #align power_series.inv PowerSeries.inv
 
-instance : Inv (PowerSeries k) :=
-  ⟨PowerSeries.inv⟩
+instance : Inv k⟦X⟧ := ⟨PowerSeries.inv⟩
 
-theorem inv_eq_inv_aux (φ : PowerSeries k) : φ⁻¹ = inv.aux (constantCoeff k φ)⁻¹ φ :=
+theorem inv_eq_inv_aux (φ : k⟦X⟧) : φ⁻¹ = inv.aux (constantCoeff k φ)⁻¹ φ :=
   rfl
 #align power_series.inv_eq_inv_aux PowerSeries.inv_eq_inv_aux
 
-theorem coeff_inv (n) (φ : PowerSeries k) :
+theorem coeff_inv (n) (φ : k⟦X⟧) :
     coeff k n φ⁻¹ =
       if n = 0 then (constantCoeff k φ)⁻¹
       else
@@ -142,63 +149,63 @@ theorem coeff_inv (n) (φ : PowerSeries k) :
 #align power_series.coeff_inv PowerSeries.coeff_inv
 
 @[simp]
-theorem constantCoeff_inv (φ : PowerSeries k) : constantCoeff k φ⁻¹ = (constantCoeff k φ)⁻¹ :=
+theorem constantCoeff_inv (φ : k⟦X⟧) : constantCoeff k φ⁻¹ = (constantCoeff k φ)⁻¹ :=
   MvPowerSeries.constantCoeff_inv φ
 #align power_series.constant_coeff_inv PowerSeries.constantCoeff_inv
 
-theorem inv_eq_zero {φ : PowerSeries k} : φ⁻¹ = 0 ↔ constantCoeff k φ = 0 :=
+theorem inv_eq_zero {φ : k⟦X⟧} : φ⁻¹ = 0 ↔ constantCoeff k φ = 0 :=
   MvPowerSeries.inv_eq_zero
 #align power_series.inv_eq_zero PowerSeries.inv_eq_zero
 
 @[simp]
-theorem zero_inv : (0 : PowerSeries k)⁻¹ = 0 :=
+theorem zero_inv : (0 : k⟦X⟧)⁻¹ = 0 :=
   MvPowerSeries.zero_inv
 #align power_series.zero_inv PowerSeries.zero_inv
 
 -- Porting note (#10618): simp can prove this.
 -- @[simp]
-theorem invOfUnit_eq (φ : PowerSeries k) (h : constantCoeff k φ ≠ 0) :
+theorem invOfUnit_eq (φ : k⟦X⟧) (h : constantCoeff k φ ≠ 0) :
     invOfUnit φ (Units.mk0 _ h) = φ⁻¹ :=
   MvPowerSeries.invOfUnit_eq _ _
 #align power_series.inv_of_unit_eq PowerSeries.invOfUnit_eq
 
 @[simp]
-theorem invOfUnit_eq' (φ : PowerSeries k) (u : Units k) (h : constantCoeff k φ = u) :
+theorem invOfUnit_eq' (φ : k⟦X⟧) (u : Units k) (h : constantCoeff k φ = u) :
     invOfUnit φ u = φ⁻¹ :=
   MvPowerSeries.invOfUnit_eq' φ _ h
 #align power_series.inv_of_unit_eq' PowerSeries.invOfUnit_eq'
 
 @[simp]
-protected theorem mul_inv_cancel (φ : PowerSeries k) (h : constantCoeff k φ ≠ 0) : φ * φ⁻¹ = 1 :=
+protected theorem mul_inv_cancel (φ : k⟦X⟧) (h : constantCoeff k φ ≠ 0) : φ * φ⁻¹ = 1 :=
   MvPowerSeries.mul_inv_cancel φ h
 #align power_series.mul_inv_cancel PowerSeries.mul_inv_cancel
 
 @[simp]
-protected theorem inv_mul_cancel (φ : PowerSeries k) (h : constantCoeff k φ ≠ 0) : φ⁻¹ * φ = 1 :=
+protected theorem inv_mul_cancel (φ : k⟦X⟧) (h : constantCoeff k φ ≠ 0) : φ⁻¹ * φ = 1 :=
   MvPowerSeries.inv_mul_cancel φ h
 #align power_series.inv_mul_cancel PowerSeries.inv_mul_cancel
 
-theorem eq_mul_inv_iff_mul_eq {φ₁ φ₂ φ₃ : PowerSeries k} (h : constantCoeff k φ₃ ≠ 0) :
+theorem eq_mul_inv_iff_mul_eq {φ₁ φ₂ φ₃ : k⟦X⟧} (h : constantCoeff k φ₃ ≠ 0) :
     φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂ :=
   MvPowerSeries.eq_mul_inv_iff_mul_eq h
 #align power_series.eq_mul_inv_iff_mul_eq PowerSeries.eq_mul_inv_iff_mul_eq
 
-theorem eq_inv_iff_mul_eq_one {φ ψ : PowerSeries k} (h : constantCoeff k ψ ≠ 0) :
+theorem eq_inv_iff_mul_eq_one {φ ψ : k⟦X⟧} (h : constantCoeff k ψ ≠ 0) :
     φ = ψ⁻¹ ↔ φ * ψ = 1 :=
   MvPowerSeries.eq_inv_iff_mul_eq_one h
 #align power_series.eq_inv_iff_mul_eq_one PowerSeries.eq_inv_iff_mul_eq_one
 
-theorem inv_eq_iff_mul_eq_one {φ ψ : PowerSeries k} (h : constantCoeff k ψ ≠ 0) :
+theorem inv_eq_iff_mul_eq_one {φ ψ : k⟦X⟧} (h : constantCoeff k ψ ≠ 0) :
     ψ⁻¹ = φ ↔ φ * ψ = 1 :=
   MvPowerSeries.inv_eq_iff_mul_eq_one h
 #align power_series.inv_eq_iff_mul_eq_one PowerSeries.inv_eq_iff_mul_eq_one
 
 @[simp]
-protected theorem mul_inv_rev (φ ψ : PowerSeries k) : (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹ :=
+protected theorem mul_inv_rev (φ ψ : k⟦X⟧) : (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹ :=
   MvPowerSeries.mul_inv_rev _ _
 #align power_series.mul_inv_rev PowerSeries.mul_inv_rev
 
-instance : InvOneClass (PowerSeries k) :=
+instance : InvOneClass k⟦X⟧ :=
   { inferInstanceAs <| InvOneClass <| MvPowerSeries Unit k with }
 
 @[simp]
@@ -208,16 +215,80 @@ set_option linter.uppercaseLean3 false in
 #align power_series.C_inv PowerSeries.C_inv
 
 @[simp]
-theorem X_inv : (X : PowerSeries k)⁻¹ = 0 :=
+theorem X_inv : (X : k⟦X⟧)⁻¹ = 0 :=
   MvPowerSeries.X_inv _
 set_option linter.uppercaseLean3 false in
 #align power_series.X_inv PowerSeries.X_inv
 
 @[simp]
-theorem smul_inv (r : k) (φ : PowerSeries k) : (r • φ)⁻¹ = r⁻¹ • φ⁻¹ :=
+theorem smul_inv (r : k) (φ : k⟦X⟧) : (r • φ)⁻¹ = r⁻¹ • φ⁻¹ :=
   MvPowerSeries.smul_inv _ _
 #align power_series.smul_inv PowerSeries.smul_inv
 
+/-- `firstUnitCoeff` is the non-zero coefficient whose index is `f.order`, seen as a unit of the
+  field. It is obtained using `divided_by_X_pow_order`, defined in `PowerSeries.Order`-/
+def firstUnitCoeff {f : k⟦X⟧} (hf : f ≠ 0) : kˣ :=
+  let d := f.order.get (order_finite_iff_ne_zero.mpr hf)
+  have f_const : coeff k d f ≠ 0 := by apply coeff_order
+  have : Invertible (constantCoeff k (divided_by_X_pow_order hf)) := by
+    apply invertibleOfNonzero
+    convert f_const using 1
+    rw [← coeff_zero_eq_constantCoeff, ← zero_add d]
+    convert (coeff_X_pow_mul (exists_eq_mul_right_of_dvd (X_pow_order_dvd
+      (order_finite_iff_ne_zero.mpr hf))).choose d 0).symm
+    exact (self_eq_X_pow_order_mul_divided_by_X_pow_order hf).symm
+  unitOfInvertible (constantCoeff k (divided_by_X_pow_order hf))
+
+/-- `Inv_divided_by_X_pow_order` is the inverse of the element obtained by diving a non-zero power
+series by the largest power of `X` dividing it. Useful to create a term of type `Units`, done in
+`Unit_divided_by_X_pow_order` -/
+def Inv_divided_by_X_pow_order {f : k⟦X⟧} (hf : f ≠ 0) : k⟦X⟧ :=
+  invOfUnit (divided_by_X_pow_order hf) (firstUnitCoeff hf)
+
+@[simp]
+theorem Inv_divided_by_X_pow_order_rightInv {f : k⟦X⟧} (hf : f ≠ 0) :
+    divided_by_X_pow_order hf * Inv_divided_by_X_pow_order hf = 1 :=
+  mul_invOfUnit (divided_by_X_pow_order hf) (firstUnitCoeff hf) rfl
+
+@[simp]
+theorem Inv_divided_by_X_pow_order_leftInv {f : k⟦X⟧} (hf : f ≠ 0) :
+    (Inv_divided_by_X_pow_order hf) * (divided_by_X_pow_order hf) = 1 := by
+  rw [mul_comm]
+  exact mul_invOfUnit (divided_by_X_pow_order hf) (firstUnitCoeff hf) rfl
+
+open scoped Classical
+
+/-- `Unit_of_divided_by_X_pow_order` is the unit power series obtained by dividing a non-zero
+power series by the largest power of `X` that divides it. -/
+def Unit_of_divided_by_X_pow_order (f : k⟦X⟧) : k⟦X⟧ˣ :=
+  if hf : f = 0 then 1
+  else
+    { val := divided_by_X_pow_order hf
+      inv := Inv_divided_by_X_pow_order hf
+      val_inv := Inv_divided_by_X_pow_order_rightInv hf
+      inv_val := Inv_divided_by_X_pow_order_leftInv hf }
+
+theorem isUnit_divided_by_X_pow_order {f : k⟦X⟧} (hf : f ≠ 0) :
+    IsUnit (divided_by_X_pow_order hf) :=
+  ⟨Unit_of_divided_by_X_pow_order f,
+    by simp only [Unit_of_divided_by_X_pow_order, dif_neg hf, Units.val_mk]⟩
+
+theorem Unit_of_divided_by_X_pow_order_nonzero {f : k⟦X⟧} (hf : f ≠ 0) :
+    ↑(Unit_of_divided_by_X_pow_order f) = divided_by_X_pow_order hf := by
+  simp only [Unit_of_divided_by_X_pow_order, dif_neg hf, Units.val_mk]
+
+@[simp]
+theorem Unit_of_divided_by_X_pow_order_zero : Unit_of_divided_by_X_pow_order (0 : k⟦X⟧) = 1 := by
+  simp only [Unit_of_divided_by_X_pow_order, dif_pos]
+
+theorem eq_divided_by_X_pow_order_Iff_Unit {f : k⟦X⟧} (hf : f ≠ 0) :
+    f = divided_by_X_pow_order hf ↔ IsUnit f :=
+  ⟨fun h => by rw [h]; exact isUnit_divided_by_X_pow_order hf, fun h => by
+    have : f.order.get (order_finite_iff_ne_zero.mpr hf) = 0 := by
+      simp only [order_zero_of_unit h, PartENat.get_zero]
+    convert (self_eq_X_pow_order_mul_divided_by_X_pow_order hf).symm
+    simp only [this, pow_zero, one_mul]⟩
+
 end Field
 
 section LocalRing
@@ -236,6 +307,81 @@ instance : LocalRing R⟦X⟧ :=
 
 end LocalRing
 
+section DiscreteValuationRing
+
+variable {k : Type*} [Field k]
+
+open DiscreteValuationRing
+
+theorem hasUnitMulPowIrreducibleFactorization :
+    HasUnitMulPowIrreducibleFactorization k⟦X⟧ :=
+  ⟨X, And.intro X_irreducible
+      (by
+        intro f hf
+        use f.order.get (order_finite_iff_ne_zero.mpr hf)
+        use Unit_of_divided_by_X_pow_order f
+        simp only [Unit_of_divided_by_X_pow_order_nonzero hf]
+        exact self_eq_X_pow_order_mul_divided_by_X_pow_order hf)⟩
+
+instance : UniqueFactorizationMonoid k⟦X⟧ :=
+  hasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid
+
+instance : DiscreteValuationRing k⟦X⟧ :=
+  ofHasUnitMulPowIrreducibleFactorization hasUnitMulPowIrreducibleFactorization
+
+instance isNoetherianRing : IsNoetherianRing k⟦X⟧ :=
+  PrincipalIdealRing.isNoetherianRing
+
+/-- The maximal ideal of `k⟦X⟧` is generated by `X`. -/
+theorem maximalIdeal_eq_span_X : LocalRing.maximalIdeal (k⟦X⟧) = Ideal.span {X} := by
+  have hX : (Ideal.span {(X : k⟦X⟧)}).IsMaximal := by
+    rw [Ideal.isMaximal_iff]
+    constructor
+    · rw [Ideal.mem_span_singleton]
+      exact Prime.not_dvd_one X_prime
+    · intro I f hI hfX hfI
+      rw [Ideal.mem_span_singleton, X_dvd_iff] at hfX
+      have hfI0 : C k (f 0) ∈ I := by
+        have : C k (f 0) = f - (f - C k (f 0)) := by rw [sub_sub_cancel]
+        rw [this]
+        apply Ideal.sub_mem I hfI
+        apply hI
+        rw [Ideal.mem_span_singleton, X_dvd_iff, map_sub, constantCoeff_C, ←
+          coeff_zero_eq_constantCoeff_apply, sub_eq_zero, coeff_zero_eq_constantCoeff]
+        rfl
+      rw [← Ideal.eq_top_iff_one]
+      apply Ideal.eq_top_of_isUnit_mem I hfI0 (IsUnit.map (C k) (Ne.isUnit hfX))
+  rw [LocalRing.eq_maximalIdeal hX]
+
+instance : NormalizationMonoid k⟦X⟧ where
+  normUnit f := (Unit_of_divided_by_X_pow_order f)⁻¹
+  normUnit_zero := by simp only [Unit_of_divided_by_X_pow_order_zero, inv_one]
+  normUnit_mul  := fun hf hg => by
+    simp only [← mul_inv, inv_inj]
+    simp only [Unit_of_divided_by_X_pow_order_nonzero (mul_ne_zero hf hg),
+      Unit_of_divided_by_X_pow_order_nonzero hf, Unit_of_divided_by_X_pow_order_nonzero hg,
+      Units.ext_iff, val_unitOfInvertible, Units.val_mul, divided_by_X_pow_orderMul]
+  normUnit_coe_units := by
+    intro u
+    set u₀ := u.1 with hu
+    have h₀ : IsUnit u₀ := ⟨u, hu.symm⟩
+    rw [inv_inj, Units.ext_iff, ← hu, Unit_of_divided_by_X_pow_order_nonzero h₀.ne_zero]
+    exact ((eq_divided_by_X_pow_order_Iff_Unit h₀.ne_zero).mpr h₀).symm
+
+open LocalRing
+
+theorem ker_coeff_eq_max_ideal : RingHom.ker (constantCoeff k) = maximalIdeal _ :=
+  Ideal.ext fun _ => by
+    rw [RingHom.mem_ker, maximalIdeal_eq_span_X, Ideal.mem_span_singleton, X_dvd_iff]
+
+/-- The ring isomorphism between the residue field of the ring of power series valued in a field `K`
+and `K` itself. -/
+def residueFieldOfPowerSeries : ResidueField k⟦X⟧ ≃+* k :=
+  (Ideal.quotEquivOfEq (ker_coeff_eq_max_ideal).symm).trans
+    (RingHom.quotientKerEquivOfSurjective PowerSeries.constantCoeff_surj)
+
+end DiscreteValuationRing
+
 
 end PowerSeries