feat(RingTheory/LaurentSeries): add notation

Refs: leanprover/vscode-lean4#523
leanprover-community · Sep 9, 2024 · 9959af2 · 9959af2
1 parent 8c811c9
commit 9959af2
Showing 1 changed file with 47 additions and 38 deletions.
diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean
@@ -58,12 +58,21 @@ variable {R : Type*}
 
 namespace LaurentSeries
 
+section
+
+/--
+`R⸨X⸩` is notation for `LaurentSeries R`,
+-/
+scoped notation:9000 R "⸨X⸩" => LaurentSeries R
+
+end
+
 section HasseDeriv
 
 /-- The Hasse derivative of Laurent series, as a linear map. -/
 @[simps]
 def hasseDeriv (R : Type*) {V : Type*} [AddCommGroup V] [Semiring R] [Module R V] (k : ℕ) :
-    LaurentSeries V →ₗ[R] LaurentSeries V where
+    V⸨X⸩ →ₗ[R] V⸨X⸩ where
   toFun f := HahnSeries.ofSuppBddBelow (fun (n : ℤ) => (Ring.choose (n + k) k) • f.coeff (n + k))
     (forallLTEqZero_supp_BddBelow _ (f.order - k : ℤ)
     (fun _ h_lt ↦ by rw [coeff_eq_zero_of_lt_order <| lt_sub_iff_add_lt.mp h_lt, smul_zero]))
@@ -76,7 +85,7 @@ def hasseDeriv (R : Type*) {V : Type*} [AddCommGroup V] [Semiring R] [Module R V
 
 variable [Semiring R] {V : Type*} [AddCommGroup V] [Module R V]
 
-theorem hasseDeriv_coeff (k : ℕ) (f : LaurentSeries V) (n : ℤ) :
+theorem hasseDeriv_coeff (k : ℕ) (f : V⸨X⸩) (n : ℤ) :
     (hasseDeriv R k f).coeff n = Ring.choose (n + k) k • f.coeff (n + k) :=
   rfl
 
@@ -86,37 +95,37 @@ section Semiring
 
 variable [Semiring R]
 
-instance : Coe (PowerSeries R) (LaurentSeries R) :=
+instance : Coe (PowerSeries R) R⸨X⸩ :=
   ⟨HahnSeries.ofPowerSeries ℤ R⟩
 
 /- Porting note: now a syntactic tautology and not needed elsewhere
 theorem coe_powerSeries (x : PowerSeries R) :
-    (x : LaurentSeries R) = HahnSeries.ofPowerSeries ℤ R x :=
+    (x : R⸨X⸩) = HahnSeries.ofPowerSeries ℤ R x :=
   rfl -/
 
 @[simp]
 theorem coeff_coe_powerSeries (x : PowerSeries R) (n : ℕ) :
-    HahnSeries.coeff (x : LaurentSeries R) n = PowerSeries.coeff R n x := by
+    HahnSeries.coeff (x : R⸨X⸩) n = PowerSeries.coeff R n x := by
   rw [ofPowerSeries_apply_coeff]
 
 /-- This is a power series that can be multiplied by an integer power of `X` to give our
   Laurent series. If the Laurent series is nonzero, `powerSeriesPart` has a nonzero
   constant term. -/
-def powerSeriesPart (x : LaurentSeries R) : PowerSeries R :=
+def powerSeriesPart (x : R⸨X⸩) : PowerSeries R :=
   PowerSeries.mk fun n => x.coeff (x.order + n)
 
 @[simp]
-theorem powerSeriesPart_coeff (x : LaurentSeries R) (n : ℕ) :
+theorem powerSeriesPart_coeff (x : R⸨X⸩) (n : ℕ) :
     PowerSeries.coeff R n x.powerSeriesPart = x.coeff (x.order + n) :=
   PowerSeries.coeff_mk _ _
 
 @[simp]
-theorem powerSeriesPart_zero : powerSeriesPart (0 : LaurentSeries R) = 0 := by
+theorem powerSeriesPart_zero : powerSeriesPart (0 : R⸨X⸩) = 0 := by
   ext
   simp [(PowerSeries.coeff _ _).map_zero] -- Note: this doesn't get picked up any more
 
 @[simp]
-theorem powerSeriesPart_eq_zero (x : LaurentSeries R) : x.powerSeriesPart = 0 ↔ x = 0 := by
+theorem powerSeriesPart_eq_zero (x : R⸨X⸩) : x.powerSeriesPart = 0 ↔ x = 0 := by
   constructor
   · contrapose!
     simp only [ne_eq]
@@ -128,8 +137,8 @@ theorem powerSeriesPart_eq_zero (x : LaurentSeries R) : x.powerSeriesPart = 0
     simp
 
 @[simp]
-theorem single_order_mul_powerSeriesPart (x : LaurentSeries R) :
-    (single x.order 1 : LaurentSeries R) * x.powerSeriesPart = x := by
+theorem single_order_mul_powerSeriesPart (x : R⸨X⸩) :
+    (single x.order 1 : R⸨X⸩) * x.powerSeriesPart = x := by
   ext n
   rw [← sub_add_cancel n x.order, single_mul_coeff_add, sub_add_cancel, one_mul]
   by_cases h : x.order ≤ n
@@ -145,25 +154,25 @@ theorem single_order_mul_powerSeriesPart (x : LaurentSeries R) :
       rw [← sub_nonneg, ← hm]
       simp only [Nat.cast_nonneg]
 
-theorem ofPowerSeries_powerSeriesPart (x : LaurentSeries R) :
+theorem ofPowerSeries_powerSeriesPart (x : R⸨X⸩) :
     ofPowerSeries ℤ R x.powerSeriesPart = single (-x.order) 1 * x := by
   refine Eq.trans ?_ (congr rfl x.single_order_mul_powerSeriesPart)
   rw [← mul_assoc, single_mul_single, neg_add_cancel, mul_one, ← C_apply, C_one, one_mul]
 
 end Semiring
 
-instance [CommSemiring R] : Algebra (PowerSeries R) (LaurentSeries R) :=
+instance [CommSemiring R] : Algebra (PowerSeries R) (R⸨X⸩) :=
   (HahnSeries.ofPowerSeries ℤ R).toAlgebra
 
 @[simp]
 theorem coe_algebraMap [CommSemiring R] :
-    ⇑(algebraMap (PowerSeries R) (LaurentSeries R)) = HahnSeries.ofPowerSeries ℤ R :=
+    ⇑(algebraMap (PowerSeries R) R⸨X⸩) = HahnSeries.ofPowerSeries ℤ R :=
   rfl
 
 /-- The localization map from power series to Laurent series. -/
 @[simps (config := { rhsMd := .all, simpRhs := true })]
 instance of_powerSeries_localization [CommRing R] :
-    IsLocalization (Submonoid.powers (PowerSeries.X : PowerSeries R)) (LaurentSeries R) where
+    IsLocalization (Submonoid.powers (PowerSeries.X : PowerSeries R)) R⸨X⸩ where
   map_units' := by
     rintro ⟨_, n, rfl⟩
     refine ⟨⟨single (n : ℤ) 1, single (-n : ℤ) 1, ?_, ?_⟩, ?_⟩
@@ -187,7 +196,7 @@ instance of_powerSeries_localization [CommRing R] :
     rintro rfl
     exact ⟨1, rfl⟩
 
-instance {K : Type*} [Field K] : IsFractionRing (PowerSeries K) (LaurentSeries K) :=
+instance {K : Type*} [Field K] : IsFractionRing (PowerSeries K) K⸨X⸩ :=
   IsLocalization.of_le (Submonoid.powers (PowerSeries.X : PowerSeries K)) _
     (powers_le_nonZeroDivisors_of_noZeroDivisors PowerSeries.X_ne_zero) fun _ hf =>
     isUnit_of_mem_nonZeroDivisors <| map_mem_nonZeroDivisors _ HahnSeries.ofPowerSeries_injective hf
@@ -201,31 +210,31 @@ open LaurentSeries
 variable {R' : Type*} [Semiring R] [Ring R'] (f g : PowerSeries R) (f' g' : PowerSeries R')
 
 @[norm_cast] -- Porting note (#10618): simp can prove this
-theorem coe_zero : ((0 : PowerSeries R) : LaurentSeries R) = 0 :=
+theorem coe_zero : ((0 : PowerSeries R) : R⸨X⸩) = 0 :=
   (ofPowerSeries ℤ R).map_zero
 
 @[norm_cast] -- Porting note (#10618): simp can prove this
-theorem coe_one : ((1 : PowerSeries R) : LaurentSeries R) = 1 :=
+theorem coe_one : ((1 : PowerSeries R) : R⸨X⸩) = 1 :=
   (ofPowerSeries ℤ R).map_one
 
 @[norm_cast] -- Porting note (#10618): simp can prove this
-theorem coe_add : ((f + g : PowerSeries R) : LaurentSeries R) = f + g :=
+theorem coe_add : ((f + g : PowerSeries R) : R⸨X⸩) = f + g :=
   (ofPowerSeries ℤ R).map_add _ _
 
 @[norm_cast]
-theorem coe_sub : ((f' - g' : PowerSeries R') : LaurentSeries R') = f' - g' :=
+theorem coe_sub : ((f' - g' : PowerSeries R') : R'⸨X⸩) = f' - g' :=
   (ofPowerSeries ℤ R').map_sub _ _
 
 @[norm_cast]
-theorem coe_neg : ((-f' : PowerSeries R') : LaurentSeries R') = -f' :=
+theorem coe_neg : ((-f' : PowerSeries R') : R'⸨X⸩) = -f' :=
   (ofPowerSeries ℤ R').map_neg _
 
 @[norm_cast] -- Porting note (#10618): simp can prove this
-theorem coe_mul : ((f * g : PowerSeries R) : LaurentSeries R) = f * g :=
+theorem coe_mul : ((f * g : PowerSeries R) : R⸨X⸩) = f * g :=
   (ofPowerSeries ℤ R).map_mul _ _
 
 theorem coeff_coe (i : ℤ) :
-    ((f : PowerSeries R) : LaurentSeries R).coeff i =
+    ((f : PowerSeries R) : R⸨X⸩).coeff i =
       if i < 0 then 0 else PowerSeries.coeff R i.natAbs f := by
   cases i
   · rw [Int.ofNat_eq_coe, coeff_coe_powerSeries, if_neg (Int.natCast_nonneg _).not_lt,
@@ -237,23 +246,23 @@ theorem coeff_coe (i : ℤ) :
 
 -- Porting note (#10618): simp can prove this
 -- Porting note: removed norm_cast attribute
-theorem coe_C (r : R) : ((C R r : PowerSeries R) : LaurentSeries R) = HahnSeries.C r :=
+theorem coe_C (r : R) : ((C R r : PowerSeries R) : R⸨X⸩) = HahnSeries.C r :=
   ofPowerSeries_C _
 
 -- @[simp] -- Porting note (#10618): simp can prove this
-theorem coe_X : ((X : PowerSeries R) : LaurentSeries R) = single 1 1 :=
+theorem coe_X : ((X : PowerSeries R) : R⸨X⸩) = single 1 1 :=
   ofPowerSeries_X
 
 @[simp, norm_cast]
 theorem coe_smul {S : Type*} [Semiring S] [Module R S] (r : R) (x : PowerSeries S) :
-    ((r • x : PowerSeries S) : LaurentSeries S) = r • (ofPowerSeries ℤ S x) := by
+    ((r • x : PowerSeries S) : S⸨X⸩) = r • (ofPowerSeries ℤ S x) := by
   ext
   simp [coeff_coe, coeff_smul, smul_ite]
 
 -- Porting note: RingHom.map_bit0 and RingHom.map_bit1 no longer exist
 
 @[norm_cast]
-theorem coe_pow (n : ℕ) : ((f ^ n : PowerSeries R) : LaurentSeries R) = (ofPowerSeries ℤ R f) ^ n :=
+theorem coe_pow (n : ℕ) : ((f ^ n : PowerSeries R) : R⸨X⸩) = (ofPowerSeries ℤ R f) ^ n :=
   (ofPowerSeries ℤ R).map_pow _ _
 
 end PowerSeries
@@ -466,18 +475,18 @@ namespace LaurentSeries
 
 open IsDedekindDomain.HeightOneSpectrum PowerSeries RatFunc
 
-instance : Valued (LaurentSeries K) ℤₘ₀ := Valued.mk' (PowerSeries.idealX K).valuation
+instance : Valued K⸨X⸩ ℤₘ₀ := Valued.mk' (PowerSeries.idealX K).valuation
 
 theorem valuation_X_pow (s : ℕ) :
-    Valued.v (((X : K⟦X⟧) : LaurentSeries K) ^ s) = Multiplicative.ofAdd (-(s : ℤ)) := by
+    Valued.v (((X : K⟦X⟧) : K⸨X⸩) ^ s) = Multiplicative.ofAdd (-(s : ℤ)) := by
   erw [map_pow, ← one_mul (s : ℤ), ← neg_mul (1 : ℤ) s, Int.ofAdd_mul,
     WithZero.coe_zpow, ofAdd_neg, WithZero.coe_inv, zpow_natCast, valuation_of_algebraMap,
     intValuation_toFun, intValuation_X, ofAdd_neg, WithZero.coe_inv, inv_pow]
 
 theorem valuation_single_zpow (s : ℤ) :
-    Valued.v (HahnSeries.single s (1 : K) : LaurentSeries K) =
+    Valued.v (HahnSeries.single s (1 : K) : K⸨X⸩) =
       Multiplicative.ofAdd (-(s : ℤ)) := by
-  have : Valued.v (1 : LaurentSeries K) = (1 : ℤₘ₀) := Valued.v.map_one
+  have : Valued.v (1 : K⸨X⸩) = (1 : ℤₘ₀) := Valued.v.map_one
   rw [← single_zero_one, ← add_neg_cancel s, ← mul_one 1, ← single_mul_single, map_mul,
     mul_eq_one_iff_eq_inv₀] at this
   · rw [this]
@@ -490,18 +499,18 @@ theorem valuation_single_zpow (s : ℤ) :
 
 /- The coefficients of a power series vanish in degree strictly less than its valuation. -/
 theorem coeff_zero_of_lt_intValuation {n d : ℕ} {f : K⟦X⟧}
-    (H : Valued.v (f : LaurentSeries K) ≤ Multiplicative.ofAdd (-d : ℤ)) :
+    (H : Valued.v (f : K⸨X⸩) ≤ Multiplicative.ofAdd (-d : ℤ)) :
     n < d → coeff K n f = 0 := by
   intro hnd
   apply (PowerSeries.X_pow_dvd_iff).mp _ n hnd
   erw [← span_singleton_dvd_span_singleton_iff_dvd, ← Ideal.span_singleton_pow,
     ← (intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d), ← intValuation_apply,
-    ← valuation_of_algebraMap (R := K⟦X⟧) (K := (LaurentSeries K))]
+    ← valuation_of_algebraMap (R := K⟦X⟧) (K := K⸨X⸩)]
   exact H
 
 /- The valuation of a power series is the order of the first non-zero coefficient. -/
 theorem intValuation_le_iff_coeff_lt_eq_zero {d : ℕ} (f : K⟦X⟧) :
-    Valued.v (f : LaurentSeries K) ≤ Multiplicative.ofAdd (-d : ℤ) ↔
+    Valued.v (f : K⸨X⸩) ≤ Multiplicative.ofAdd (-d : ℤ) ↔
       ∀ n : ℕ, n < d → coeff K n f = 0 := by
   have : PowerSeries.X ^ d ∣ f ↔ ∀ n : ℕ, n < d → (PowerSeries.coeff K n) f = 0 :=
     ⟨PowerSeries.X_pow_dvd_iff.mp, PowerSeries.X_pow_dvd_iff.mpr⟩
@@ -510,7 +519,7 @@ theorem intValuation_le_iff_coeff_lt_eq_zero {d : ℕ} (f : K⟦X⟧) :
   apply intValuation_le_pow_iff_dvd
 
 /- The coefficients of a Laurent series vanish in degree strictly less than its valuation. -/
-theorem coeff_zero_of_lt_valuation {n D : ℤ} {f : LaurentSeries K}
+theorem coeff_zero_of_lt_valuation {n D : ℤ} {f : K⸨X⸩}
     (H : Valued.v f ≤ Multiplicative.ofAdd (-D)) : n < D → f.coeff n = 0 := by
   intro hnd
   by_cases h_n_ord : n < f.order
@@ -538,7 +547,7 @@ theorem coeff_zero_of_lt_valuation {n D : ℤ} {f : LaurentSeries K}
       mul_le_mul_left (by simp only [ne_eq, WithZero.coe_ne_zero, not_false_iff, zero_lt_iff])]
 
 /- The valuation of a Laurent series is the order of the first non-zero coefficient. -/
-theorem valuation_le_iff_coeff_lt_eq_zero {D : ℤ} {f : LaurentSeries K} :
+theorem valuation_le_iff_coeff_lt_eq_zero {D : ℤ} {f : K⸨X⸩} :
     Valued.v f ≤ ↑(Multiplicative.ofAdd (-D : ℤ)) ↔ ∀ n : ℤ, n < D → f.coeff n = 0 := by
   refine ⟨fun hnD n hn => coeff_zero_of_lt_valuation K hnD hn, fun h_val_f => ?_⟩
   let F := powerSeriesPart f
@@ -580,7 +589,7 @@ theorem valuation_le_iff_coeff_lt_eq_zero {D : ℤ} {f : LaurentSeries K} :
 
 /- Two Laurent series whose difference has small valuation have the same coefficients for
 small enough indices. -/
-theorem eq_coeff_of_valuation_sub_lt {d n : ℤ} {f g : LaurentSeries K}
+theorem eq_coeff_of_valuation_sub_lt {d n : ℤ} {f g : K⸨X⸩}
     (H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))) : n < d → g.coeff n = f.coeff n := by
   by_cases triv : g = f
   · exact fun _ => by rw [triv]
@@ -590,7 +599,7 @@ theorem eq_coeff_of_valuation_sub_lt {d n : ℤ} {f g : LaurentSeries K}
     apply coeff_zero_of_lt_valuation K H hn
 
 /- Every Laurent series of valuation less than `(1 : ℤₘ₀)` comes from a power series. -/
-theorem val_le_one_iff_eq_coe (f : LaurentSeries K) : Valued.v f ≤ (1 : ℤₘ₀) ↔
+theorem val_le_one_iff_eq_coe (f : K⸨X⸩) : Valued.v f ≤ (1 : ℤₘ₀) ↔
     ∃ F : PowerSeries K, F = f := by
   rw [← WithZero.coe_one, ← ofAdd_zero, ← neg_zero, valuation_le_iff_coeff_lt_eq_zero]
   refine ⟨fun h => ⟨PowerSeries.mk fun n => f.coeff n, ?_⟩, ?_⟩