From 73d45f44c3ebcface215d09fafb2250674bc8fa9 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Thu, 29 Feb 2024 12:38:35 +0000 Subject: [PATCH] split power series in several files (#10866) This PR split the files devoted to power series (especially RingTheory/PowerSeries/Basic) into several ones: * RingTheory/MvPowerSeries/Basic - initial definitions (multivariate) * RingTheory/MvPowerSeries/Trunc - truncation * RingTheory/MvPowerSeries/Inverse - stuff pertaining to inverses * RingTheory/PowerSeries/Basic - initial definitions (univariate) * RingTheory/PowerSeries/Trunc - truncation * RingTheory/PowerSeries/Inverse - stuff pertaining to inverses * RingTheory/PowerSeries/Order - stuff pertaining to order it remains to adjust the other files (PowerSeries/Derivative and PowerSeries/WellKnown) Co-authored-by: Antoine Chambert-Loir Co-authored-by: Johan Commelin Co-authored-by: faenuccio --- Archive/Wiedijk100Theorems/Partition.lean | 3 +- Mathlib.lean | 6 + Mathlib/NumberTheory/Bernoulli.lean | 1 + Mathlib/RingTheory/MvPowerSeries/Basic.lean | 951 ++++++++ Mathlib/RingTheory/MvPowerSeries/Inverse.lean | 308 +++ Mathlib/RingTheory/MvPowerSeries/Trunc.lean | 111 + Mathlib/RingTheory/PowerSeries/Basic.lean | 2008 +---------------- .../RingTheory/PowerSeries/Derivative.lean | 3 +- Mathlib/RingTheory/PowerSeries/Inverse.lean | 242 ++ Mathlib/RingTheory/PowerSeries/Order.lean | 350 +++ Mathlib/RingTheory/PowerSeries/Trunc.lean | 226 ++ 11 files changed, 2232 insertions(+), 1977 deletions(-) create mode 100644 Mathlib/RingTheory/MvPowerSeries/Basic.lean create mode 100644 Mathlib/RingTheory/MvPowerSeries/Inverse.lean create mode 100644 Mathlib/RingTheory/MvPowerSeries/Trunc.lean create mode 100644 Mathlib/RingTheory/PowerSeries/Inverse.lean create mode 100644 Mathlib/RingTheory/PowerSeries/Order.lean create mode 100644 Mathlib/RingTheory/PowerSeries/Trunc.lean diff --git a/Archive/Wiedijk100Theorems/Partition.lean b/Archive/Wiedijk100Theorems/Partition.lean index 7cd19cde08a1d..ae7a60cb10b66 100644 --- a/Archive/Wiedijk100Theorems/Partition.lean +++ b/Archive/Wiedijk100Theorems/Partition.lean @@ -3,7 +3,8 @@ Copyright (c) 2020 Bhavik Mehta, Aaron Anderson. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Bhavik Mehta, Aaron Anderson -/ -import Mathlib.RingTheory.PowerSeries.Basic +import Mathlib.RingTheory.PowerSeries.Inverse +import Mathlib.RingTheory.PowerSeries.Order import Mathlib.Combinatorics.Partition import Mathlib.Data.Nat.Parity import Mathlib.Data.Finset.NatAntidiagonal diff --git a/Mathlib.lean b/Mathlib.lean index 7ceb3a22d8024..c6e6c7f8b9bbb 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3308,6 +3308,9 @@ import Mathlib.RingTheory.MvPolynomial.NewtonIdentities import Mathlib.RingTheory.MvPolynomial.Symmetric import Mathlib.RingTheory.MvPolynomial.Tower import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous +import Mathlib.RingTheory.MvPowerSeries.Basic +import Mathlib.RingTheory.MvPowerSeries.Inverse +import Mathlib.RingTheory.MvPowerSeries.Trunc import Mathlib.RingTheory.Nakayama import Mathlib.RingTheory.Nilpotent import Mathlib.RingTheory.Noetherian @@ -3349,6 +3352,9 @@ import Mathlib.RingTheory.PolynomialAlgebra import Mathlib.RingTheory.PowerBasis import Mathlib.RingTheory.PowerSeries.Basic import Mathlib.RingTheory.PowerSeries.Derivative +import Mathlib.RingTheory.PowerSeries.Inverse +import Mathlib.RingTheory.PowerSeries.Order +import Mathlib.RingTheory.PowerSeries.Trunc import Mathlib.RingTheory.PowerSeries.WellKnown import Mathlib.RingTheory.Prime import Mathlib.RingTheory.PrincipalIdealDomain diff --git a/Mathlib/NumberTheory/Bernoulli.lean b/Mathlib/NumberTheory/Bernoulli.lean index e3201fd409bbc..f0b709e7335e9 100644 --- a/Mathlib/NumberTheory/Bernoulli.lean +++ b/Mathlib/NumberTheory/Bernoulli.lean @@ -6,6 +6,7 @@ Authors: Johan Commelin, Kevin Buzzard import Mathlib.Algebra.BigOperators.NatAntidiagonal import Mathlib.Algebra.GeomSum import Mathlib.Data.Fintype.BigOperators +import Mathlib.RingTheory.PowerSeries.Inverse import Mathlib.RingTheory.PowerSeries.WellKnown import Mathlib.Tactic.FieldSimp diff --git a/Mathlib/RingTheory/MvPowerSeries/Basic.lean b/Mathlib/RingTheory/MvPowerSeries/Basic.lean new file mode 100644 index 0000000000000..00fd879feb40e --- /dev/null +++ b/Mathlib/RingTheory/MvPowerSeries/Basic.lean @@ -0,0 +1,951 @@ +/- +Copyright (c) 2019 Johan Commelin. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johan Commelin, Kenny Lau +-/ + +import Mathlib.LinearAlgebra.StdBasis +import Mathlib.Tactic.Linarith +import Mathlib.Data.Finset.PiAntidiagonal +import Mathlib.Data.MvPolynomial.Basic + +#align_import ring_theory.power_series.basic from "leanprover-community/mathlib"@"2d5739b61641ee4e7e53eca5688a08f66f2e6a60" + +/-! +# Formal (multivariate) power series + +This file defines multivariate formal power series +and develops the basic properties of these objects. + +A formal power series is to a polynomial like an infinite sum is to a finite sum. + +We provide the natural inclusion from multivariate polynomials to multivariate formal power series. + +## Note + +This file sets up the (semi)ring structure on multivariate power series: +additional results are in: +* `Mathlib.RingTheory.MvPowerSeries.Inverse` : invertibility, + formal power series over a local ring form a local ring; +* `Mathlib.RingTheory.MvPowerSeries.Trunc`: truncation of power series. + +In `Mathlib.RingTheory.PowerSeries.Basic`, formal power series in one variable +will be obtained as a particular case, defined by + `PowerSeries R := MvPowerSeries Unit R`. +See that file for a specific description. + +## Implementation notes + +In this file we define multivariate formal power series with +variables indexed by `σ` and coefficients in `R` as +`MvPowerSeries σ R := (σ →₀ ℕ) → R`. +Unfortunately there is not yet enough API to show that they are the completion +of the ring of multivariate polynomials. However, we provide most of the infrastructure +that is needed to do this. Once I-adic completion (topological or algebraic) is available +it should not be hard to fill in the details. + +-/ + + +noncomputable section + +open BigOperators + +open Finset (antidiagonal mem_antidiagonal) + +/-- Multivariate formal power series, where `σ` is the index set of the variables +and `R` is the coefficient ring.-/ +def MvPowerSeries (σ : Type*) (R : Type*) := + (σ →₀ ℕ) → R +#align mv_power_series MvPowerSeries + +namespace MvPowerSeries + +open Finsupp + +variable {σ R : Type*} + +instance [Inhabited R] : Inhabited (MvPowerSeries σ R) := + ⟨fun _ => default⟩ + +instance [Zero R] : Zero (MvPowerSeries σ R) := + Pi.instZero + +instance [AddMonoid R] : AddMonoid (MvPowerSeries σ R) := + Pi.addMonoid + +instance [AddGroup R] : AddGroup (MvPowerSeries σ R) := + Pi.addGroup + +instance [AddCommMonoid R] : AddCommMonoid (MvPowerSeries σ R) := + Pi.addCommMonoid + +instance [AddCommGroup R] : AddCommGroup (MvPowerSeries σ R) := + Pi.addCommGroup + +instance [Nontrivial R] : Nontrivial (MvPowerSeries σ R) := + Function.nontrivial + +instance {A} [Semiring R] [AddCommMonoid A] [Module R A] : Module R (MvPowerSeries σ A) := + Pi.module _ _ _ + +instance {A S} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R A] [Module S A] [SMul R S] + [IsScalarTower R S A] : IsScalarTower R S (MvPowerSeries σ A) := + Pi.isScalarTower + +section Semiring + +variable (R) [Semiring R] + +/-- The `n`th monomial as multivariate formal power series: + it is defined as the `R`-linear map from `R` to the semi-ring + of multivariate formal power series associating to each `a` + the map sending `n : σ →₀ ℕ` to the value `a` + and sending all other `x : σ →₀ ℕ` different from `n` to `0`. -/ +def monomial (n : σ →₀ ℕ) : R →ₗ[R] MvPowerSeries σ R := + letI := Classical.decEq σ + LinearMap.stdBasis R (fun _ ↦ R) n +#align mv_power_series.monomial MvPowerSeries.monomial + +/-- The `n`th coefficient of a multivariate formal power series.-/ +def coeff (n : σ →₀ ℕ) : MvPowerSeries σ R →ₗ[R] R := + LinearMap.proj n +#align mv_power_series.coeff MvPowerSeries.coeff + +variable {R} + +/-- Two multivariate formal power series are equal if all their coefficients are equal.-/ +@[ext] +theorem ext {φ ψ} (h : ∀ n : σ →₀ ℕ, coeff R n φ = coeff R n ψ) : φ = ψ := + funext h +#align mv_power_series.ext MvPowerSeries.ext + +/-- Two multivariate formal power series are equal + if and only if all their coefficients are equal.-/ +theorem ext_iff {φ ψ : MvPowerSeries σ R} : φ = ψ ↔ ∀ n : σ →₀ ℕ, coeff R n φ = coeff R n ψ := + Function.funext_iff +#align mv_power_series.ext_iff MvPowerSeries.ext_iff + +theorem monomial_def [DecidableEq σ] (n : σ →₀ ℕ) : + (monomial R n) = LinearMap.stdBasis R (fun _ ↦ R) n := by + rw [monomial] + -- unify the `Decidable` arguments + convert rfl +#align mv_power_series.monomial_def MvPowerSeries.monomial_def + +theorem coeff_monomial [DecidableEq σ] (m n : σ →₀ ℕ) (a : R) : + coeff R m (monomial R n a) = if m = n then a else 0 := by + -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 + erw [coeff, monomial_def, LinearMap.proj_apply (i := m)] + dsimp only + -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 + erw [LinearMap.stdBasis_apply, Function.update_apply, Pi.zero_apply] +#align mv_power_series.coeff_monomial MvPowerSeries.coeff_monomial + +@[simp] +theorem coeff_monomial_same (n : σ →₀ ℕ) (a : R) : coeff R n (monomial R n a) = a := by + classical + rw [monomial_def] + exact LinearMap.stdBasis_same R (fun _ ↦ R) n a +#align mv_power_series.coeff_monomial_same MvPowerSeries.coeff_monomial_same + +theorem coeff_monomial_ne {m n : σ →₀ ℕ} (h : m ≠ n) (a : R) : coeff R m (monomial R n a) = 0 := by + classical + rw [monomial_def] + exact LinearMap.stdBasis_ne R (fun _ ↦ R) _ _ h a +#align mv_power_series.coeff_monomial_ne MvPowerSeries.coeff_monomial_ne + +theorem eq_of_coeff_monomial_ne_zero {m n : σ →₀ ℕ} {a : R} (h : coeff R m (monomial R n a) ≠ 0) : + m = n := + by_contra fun h' => h <| coeff_monomial_ne h' a +#align mv_power_series.eq_of_coeff_monomial_ne_zero MvPowerSeries.eq_of_coeff_monomial_ne_zero + +@[simp] +theorem coeff_comp_monomial (n : σ →₀ ℕ) : (coeff R n).comp (monomial R n) = LinearMap.id := + LinearMap.ext <| coeff_monomial_same n +#align mv_power_series.coeff_comp_monomial MvPowerSeries.coeff_comp_monomial + +-- Porting note (#10618): simp can prove this. +-- @[simp] +theorem coeff_zero (n : σ →₀ ℕ) : coeff R n (0 : MvPowerSeries σ R) = 0 := + rfl +#align mv_power_series.coeff_zero MvPowerSeries.coeff_zero + +variable (m n : σ →₀ ℕ) (φ ψ : MvPowerSeries σ R) + +instance : One (MvPowerSeries σ R) := + ⟨monomial R (0 : σ →₀ ℕ) 1⟩ + +theorem coeff_one [DecidableEq σ] : coeff R n (1 : MvPowerSeries σ R) = if n = 0 then 1 else 0 := + coeff_monomial _ _ _ +#align mv_power_series.coeff_one MvPowerSeries.coeff_one + +theorem coeff_zero_one : coeff R (0 : σ →₀ ℕ) 1 = 1 := + coeff_monomial_same 0 1 +#align mv_power_series.coeff_zero_one MvPowerSeries.coeff_zero_one + +theorem monomial_zero_one : monomial R (0 : σ →₀ ℕ) 1 = 1 := + rfl +#align mv_power_series.monomial_zero_one MvPowerSeries.monomial_zero_one + +instance : AddMonoidWithOne (MvPowerSeries σ R) := + { show AddMonoid (MvPowerSeries σ R) by infer_instance with + natCast := fun n => monomial R 0 n + natCast_zero := by simp [Nat.cast] + natCast_succ := by simp [Nat.cast, monomial_zero_one] + one := 1 } + +instance : Mul (MvPowerSeries σ R) := + letI := Classical.decEq σ + ⟨fun φ ψ n => ∑ p in antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ⟩ + +theorem coeff_mul [DecidableEq σ] : + coeff R n (φ * ψ) = ∑ p in antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ := by + refine Finset.sum_congr ?_ fun _ _ => rfl + rw [Subsingleton.elim (Classical.decEq σ) ‹DecidableEq σ›] +#align mv_power_series.coeff_mul MvPowerSeries.coeff_mul + +protected theorem zero_mul : (0 : MvPowerSeries σ R) * φ = 0 := + ext fun n => by classical simp [coeff_mul] +#align mv_power_series.zero_mul MvPowerSeries.zero_mul + +protected theorem mul_zero : φ * 0 = 0 := + ext fun n => by classical simp [coeff_mul] +#align mv_power_series.mul_zero MvPowerSeries.mul_zero + +theorem coeff_monomial_mul (a : R) : + coeff R m (monomial R n a * φ) = if n ≤ m then a * coeff R (m - n) φ else 0 := by + classical + have : + ∀ p ∈ antidiagonal m, + coeff R (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial R n a) * coeff R p.2 φ ≠ 0 → p.1 = n := + fun p _ hp => eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp) + rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_fst_eq_antidiagonal _ n, + Finset.sum_ite_index] + simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty] +#align mv_power_series.coeff_monomial_mul MvPowerSeries.coeff_monomial_mul + +theorem coeff_mul_monomial (a : R) : + coeff R m (φ * monomial R n a) = if n ≤ m then coeff R (m - n) φ * a else 0 := by + classical + have : + ∀ p ∈ antidiagonal m, + coeff R (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 φ * coeff R p.2 (monomial R n a) ≠ 0 → p.2 = n := + fun p _ hp => eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hp) + rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_snd_eq_antidiagonal _ n, + Finset.sum_ite_index] + simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty] +#align mv_power_series.coeff_mul_monomial MvPowerSeries.coeff_mul_monomial + +theorem coeff_add_monomial_mul (a : R) : + coeff R (m + n) (monomial R m a * φ) = a * coeff R n φ := by + rw [coeff_monomial_mul, if_pos, add_tsub_cancel_left] + exact le_add_right le_rfl +#align mv_power_series.coeff_add_monomial_mul MvPowerSeries.coeff_add_monomial_mul + +theorem coeff_add_mul_monomial (a : R) : + coeff R (m + n) (φ * monomial R n a) = coeff R m φ * a := by + rw [coeff_mul_monomial, if_pos, add_tsub_cancel_right] + exact le_add_left le_rfl +#align mv_power_series.coeff_add_mul_monomial MvPowerSeries.coeff_add_mul_monomial + +@[simp] +theorem commute_monomial {a : R} {n} : + Commute φ (monomial R n a) ↔ ∀ m, Commute (coeff R m φ) a := by + refine' ext_iff.trans ⟨fun h m => _, fun h m => _⟩ + · have := h (m + n) + rwa [coeff_add_mul_monomial, add_comm, coeff_add_monomial_mul] at this + · rw [coeff_mul_monomial, coeff_monomial_mul] + split_ifs <;> [apply h; rfl] +#align mv_power_series.commute_monomial MvPowerSeries.commute_monomial + +protected theorem one_mul : (1 : MvPowerSeries σ R) * φ = φ := + ext fun n => by simpa using coeff_add_monomial_mul 0 n φ 1 +#align mv_power_series.one_mul MvPowerSeries.one_mul + +protected theorem mul_one : φ * 1 = φ := + ext fun n => by simpa using coeff_add_mul_monomial n 0 φ 1 +#align mv_power_series.mul_one MvPowerSeries.mul_one + +protected theorem mul_add (φ₁ φ₂ φ₃ : MvPowerSeries σ R) : φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃ := + ext fun n => by + classical simp only [coeff_mul, mul_add, Finset.sum_add_distrib, LinearMap.map_add] +#align mv_power_series.mul_add MvPowerSeries.mul_add + +protected theorem add_mul (φ₁ φ₂ φ₃ : MvPowerSeries σ R) : (φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃ := + ext fun n => by + classical simp only [coeff_mul, add_mul, Finset.sum_add_distrib, LinearMap.map_add] +#align mv_power_series.add_mul MvPowerSeries.add_mul + +protected theorem mul_assoc (φ₁ φ₂ φ₃ : MvPowerSeries σ R) : φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃) := by + ext1 n + classical + simp only [coeff_mul, Finset.sum_mul, Finset.mul_sum, Finset.sum_sigma'] + apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩) + (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;> aesop (add simp [add_assoc, mul_assoc]) +#align mv_power_series.mul_assoc MvPowerSeries.mul_assoc + +instance : Semiring (MvPowerSeries σ R) := + { inferInstanceAs (AddMonoidWithOne (MvPowerSeries σ R)), + inferInstanceAs (Mul (MvPowerSeries σ R)), + inferInstanceAs (AddCommMonoid (MvPowerSeries σ R)) with + mul_one := MvPowerSeries.mul_one + one_mul := MvPowerSeries.one_mul + mul_assoc := MvPowerSeries.mul_assoc + mul_zero := MvPowerSeries.mul_zero + zero_mul := MvPowerSeries.zero_mul + left_distrib := MvPowerSeries.mul_add + right_distrib := MvPowerSeries.add_mul } + +end Semiring + +instance [CommSemiring R] : CommSemiring (MvPowerSeries σ R) := + { show Semiring (MvPowerSeries σ R) by infer_instance with + mul_comm := fun φ ψ => + ext fun n => by + classical + simpa only [coeff_mul, mul_comm] using + sum_antidiagonal_swap n fun a b => coeff R a φ * coeff R b ψ } + +instance [Ring R] : Ring (MvPowerSeries σ R) := + { inferInstanceAs (Semiring (MvPowerSeries σ R)), + inferInstanceAs (AddCommGroup (MvPowerSeries σ R)) with } + +instance [CommRing R] : CommRing (MvPowerSeries σ R) := + { inferInstanceAs (CommSemiring (MvPowerSeries σ R)), + inferInstanceAs (AddCommGroup (MvPowerSeries σ R)) with } + +section Semiring + +variable [Semiring R] + +theorem monomial_mul_monomial (m n : σ →₀ ℕ) (a b : R) : + monomial R m a * monomial R n b = monomial R (m + n) (a * b) := by + classical + ext k + simp only [coeff_mul_monomial, coeff_monomial] + split_ifs with h₁ h₂ h₃ h₃ h₂ <;> try rfl + · rw [← h₂, tsub_add_cancel_of_le h₁] at h₃ + exact (h₃ rfl).elim + · rw [h₃, add_tsub_cancel_right] at h₂ + exact (h₂ rfl).elim + · exact zero_mul b + · rw [h₂] at h₁ + exact (h₁ <| le_add_left le_rfl).elim +#align mv_power_series.monomial_mul_monomial MvPowerSeries.monomial_mul_monomial + +variable (σ) (R) + +/-- The constant multivariate formal power series.-/ +def C : R →+* MvPowerSeries σ R := + { monomial R (0 : σ →₀ ℕ) with + map_one' := rfl + map_mul' := fun a b => (monomial_mul_monomial 0 0 a b).symm + map_zero' := (monomial R (0 : _)).map_zero } +set_option linter.uppercaseLean3 false in +#align mv_power_series.C MvPowerSeries.C + +variable {σ} {R} + +@[simp] +theorem monomial_zero_eq_C : ⇑(monomial R (0 : σ →₀ ℕ)) = C σ R := + rfl +set_option linter.uppercaseLean3 false in +#align mv_power_series.monomial_zero_eq_C MvPowerSeries.monomial_zero_eq_C + +theorem monomial_zero_eq_C_apply (a : R) : monomial R (0 : σ →₀ ℕ) a = C σ R a := + rfl +set_option linter.uppercaseLean3 false in +#align mv_power_series.monomial_zero_eq_C_apply MvPowerSeries.monomial_zero_eq_C_apply + +theorem coeff_C [DecidableEq σ] (n : σ →₀ ℕ) (a : R) : + coeff R n (C σ R a) = if n = 0 then a else 0 := + coeff_monomial _ _ _ +set_option linter.uppercaseLean3 false in +#align mv_power_series.coeff_C MvPowerSeries.coeff_C + +theorem coeff_zero_C (a : R) : coeff R (0 : σ →₀ ℕ) (C σ R a) = a := + coeff_monomial_same 0 a +set_option linter.uppercaseLean3 false in +#align mv_power_series.coeff_zero_C MvPowerSeries.coeff_zero_C + +/-- The variables of the multivariate formal power series ring.-/ +def X (s : σ) : MvPowerSeries σ R := + monomial R (single s 1) 1 +set_option linter.uppercaseLean3 false in +#align mv_power_series.X MvPowerSeries.X + +theorem coeff_X [DecidableEq σ] (n : σ →₀ ℕ) (s : σ) : + coeff R n (X s : MvPowerSeries σ R) = if n = single s 1 then 1 else 0 := + coeff_monomial _ _ _ +set_option linter.uppercaseLean3 false in +#align mv_power_series.coeff_X MvPowerSeries.coeff_X + +theorem coeff_index_single_X [DecidableEq σ] (s t : σ) : + coeff R (single t 1) (X s : MvPowerSeries σ R) = if t = s then 1 else 0 := by + simp only [coeff_X, single_left_inj (one_ne_zero : (1 : ℕ) ≠ 0)] +set_option linter.uppercaseLean3 false in +#align mv_power_series.coeff_index_single_X MvPowerSeries.coeff_index_single_X + +@[simp] +theorem coeff_index_single_self_X (s : σ) : coeff R (single s 1) (X s : MvPowerSeries σ R) = 1 := + coeff_monomial_same _ _ +set_option linter.uppercaseLean3 false in +#align mv_power_series.coeff_index_single_self_X MvPowerSeries.coeff_index_single_self_X + +theorem coeff_zero_X (s : σ) : coeff R (0 : σ →₀ ℕ) (X s : MvPowerSeries σ R) = 0 := by + classical + rw [coeff_X, if_neg] + intro h + exact one_ne_zero (single_eq_zero.mp h.symm) +set_option linter.uppercaseLean3 false in +#align mv_power_series.coeff_zero_X MvPowerSeries.coeff_zero_X + +theorem commute_X (φ : MvPowerSeries σ R) (s : σ) : Commute φ (X s) := + φ.commute_monomial.mpr fun _m => Commute.one_right _ +set_option linter.uppercaseLean3 false in +#align mv_power_series.commute_X MvPowerSeries.commute_X + +theorem X_def (s : σ) : X s = monomial R (single s 1) 1 := + rfl +set_option linter.uppercaseLean3 false in +#align mv_power_series.X_def MvPowerSeries.X_def + +theorem X_pow_eq (s : σ) (n : ℕ) : (X s : MvPowerSeries σ R) ^ n = monomial R (single s n) 1 := by + induction' n with n ih + · simp + · rw [pow_succ', ih, Nat.succ_eq_add_one, Finsupp.single_add, X, monomial_mul_monomial, one_mul] +set_option linter.uppercaseLean3 false in +#align mv_power_series.X_pow_eq MvPowerSeries.X_pow_eq + +theorem coeff_X_pow [DecidableEq σ] (m : σ →₀ ℕ) (s : σ) (n : ℕ) : + coeff R m ((X s : MvPowerSeries σ R) ^ n) = if m = single s n then 1 else 0 := by + rw [X_pow_eq s n, coeff_monomial] +set_option linter.uppercaseLean3 false in +#align mv_power_series.coeff_X_pow MvPowerSeries.coeff_X_pow + +@[simp] +theorem coeff_mul_C (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) : + coeff R n (φ * C σ R a) = coeff R n φ * a := by simpa using coeff_add_mul_monomial n 0 φ a +set_option linter.uppercaseLean3 false in +#align mv_power_series.coeff_mul_C MvPowerSeries.coeff_mul_C + +@[simp] +theorem coeff_C_mul (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) : + coeff R n (C σ R a * φ) = a * coeff R n φ := by simpa using coeff_add_monomial_mul 0 n φ a +set_option linter.uppercaseLean3 false in +#align mv_power_series.coeff_C_mul MvPowerSeries.coeff_C_mul + +theorem coeff_zero_mul_X (φ : MvPowerSeries σ R) (s : σ) : coeff R (0 : σ →₀ ℕ) (φ * X s) = 0 := by + have : ¬single s 1 ≤ 0 := fun h => by simpa using h s + simp only [X, coeff_mul_monomial, if_neg this] +set_option linter.uppercaseLean3 false in +#align mv_power_series.coeff_zero_mul_X MvPowerSeries.coeff_zero_mul_X + +theorem coeff_zero_X_mul (φ : MvPowerSeries σ R) (s : σ) : coeff R (0 : σ →₀ ℕ) (X s * φ) = 0 := by + rw [← (φ.commute_X s).eq, coeff_zero_mul_X] +set_option linter.uppercaseLean3 false in +#align mv_power_series.coeff_zero_X_mul MvPowerSeries.coeff_zero_X_mul + +variable (σ) (R) + +/-- The constant coefficient of a formal power series.-/ +def constantCoeff : MvPowerSeries σ R →+* R := + { coeff R (0 : σ →₀ ℕ) with + toFun := coeff R (0 : σ →₀ ℕ) + map_one' := coeff_zero_one + map_mul' := fun φ ψ => by classical simp [coeff_mul, support_single_ne_zero] + map_zero' := LinearMap.map_zero _ } +#align mv_power_series.constant_coeff MvPowerSeries.constantCoeff + +variable {σ} {R} + +@[simp] +theorem coeff_zero_eq_constantCoeff : ⇑(coeff R (0 : σ →₀ ℕ)) = constantCoeff σ R := + rfl +#align mv_power_series.coeff_zero_eq_constant_coeff MvPowerSeries.coeff_zero_eq_constantCoeff + +theorem coeff_zero_eq_constantCoeff_apply (φ : MvPowerSeries σ R) : + coeff R (0 : σ →₀ ℕ) φ = constantCoeff σ R φ := + rfl +#align mv_power_series.coeff_zero_eq_constant_coeff_apply MvPowerSeries.coeff_zero_eq_constantCoeff_apply + +@[simp] +theorem constantCoeff_C (a : R) : constantCoeff σ R (C σ R a) = a := + rfl +set_option linter.uppercaseLean3 false in +#align mv_power_series.constant_coeff_C MvPowerSeries.constantCoeff_C + +@[simp] +theorem constantCoeff_comp_C : (constantCoeff σ R).comp (C σ R) = RingHom.id R := + rfl +set_option linter.uppercaseLean3 false in +#align mv_power_series.constant_coeff_comp_C MvPowerSeries.constantCoeff_comp_C + +-- Porting note (#10618): simp can prove this. +-- @[simp] +theorem constantCoeff_zero : constantCoeff σ R 0 = 0 := + rfl +#align mv_power_series.constant_coeff_zero MvPowerSeries.constantCoeff_zero + +-- Porting note (#10618): simp can prove this. +-- @[simp] +theorem constantCoeff_one : constantCoeff σ R 1 = 1 := + rfl +#align mv_power_series.constant_coeff_one MvPowerSeries.constantCoeff_one + +@[simp] +theorem constantCoeff_X (s : σ) : constantCoeff σ R (X s) = 0 := + coeff_zero_X s +set_option linter.uppercaseLean3 false in +#align mv_power_series.constant_coeff_X MvPowerSeries.constantCoeff_X + +/-- If a multivariate formal power series is invertible, + then so is its constant coefficient.-/ +theorem isUnit_constantCoeff (φ : MvPowerSeries σ R) (h : IsUnit φ) : + IsUnit (constantCoeff σ R φ) := + h.map _ +#align mv_power_series.is_unit_constant_coeff MvPowerSeries.isUnit_constantCoeff + +-- Porting note (#10618): simp can prove this. +-- @[simp] +theorem coeff_smul (f : MvPowerSeries σ R) (n) (a : R) : coeff _ n (a • f) = a * coeff _ n f := + rfl +#align mv_power_series.coeff_smul MvPowerSeries.coeff_smul + +theorem smul_eq_C_mul (f : MvPowerSeries σ R) (a : R) : a • f = C σ R a * f := by + ext + simp +set_option linter.uppercaseLean3 false in +#align mv_power_series.smul_eq_C_mul MvPowerSeries.smul_eq_C_mul + +theorem X_inj [Nontrivial R] {s t : σ} : (X s : MvPowerSeries σ R) = X t ↔ s = t := + ⟨by + classical + intro h + replace h := congr_arg (coeff R (single s 1)) h + rw [coeff_X, if_pos rfl, coeff_X] at h + split_ifs at h with H + · rw [Finsupp.single_eq_single_iff] at H + cases' H with H H + · exact H.1 + · exfalso + exact one_ne_zero H.1 + · exfalso + exact one_ne_zero h, congr_arg X⟩ +set_option linter.uppercaseLean3 false in +#align mv_power_series.X_inj MvPowerSeries.X_inj + +end Semiring + +section Map + +variable {S T : Type*} [Semiring R] [Semiring S] [Semiring T] + +variable (f : R →+* S) (g : S →+* T) + +variable (σ) + +/-- The map between multivariate formal power series induced by a map on the coefficients.-/ +def map : MvPowerSeries σ R →+* MvPowerSeries σ S where + toFun φ n := f <| coeff R n φ + map_zero' := ext fun _n => f.map_zero + map_one' := + ext fun n => + show f ((coeff R n) 1) = (coeff S n) 1 by + classical + rw [coeff_one, coeff_one] + split_ifs with h + · simp only [RingHom.map_ite_one_zero, ite_true, map_one, h] + · simp only [RingHom.map_ite_one_zero, ite_false, map_zero, h] + map_add' φ ψ := + ext fun n => show f ((coeff R n) (φ + ψ)) = f ((coeff R n) φ) + f ((coeff R n) ψ) by simp + map_mul' φ ψ := + ext fun n => + show f _ = _ by + classical + rw [coeff_mul, map_sum, coeff_mul] + apply Finset.sum_congr rfl + rintro ⟨i, j⟩ _; rw [f.map_mul]; rfl +#align mv_power_series.map MvPowerSeries.map + +variable {σ} + +@[simp] +theorem map_id : map σ (RingHom.id R) = RingHom.id _ := + rfl +#align mv_power_series.map_id MvPowerSeries.map_id + +theorem map_comp : map σ (g.comp f) = (map σ g).comp (map σ f) := + rfl +#align mv_power_series.map_comp MvPowerSeries.map_comp + +@[simp] +theorem coeff_map (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) : coeff S n (map σ f φ) = f (coeff R n φ) := + rfl +#align mv_power_series.coeff_map MvPowerSeries.coeff_map + +@[simp] +theorem constantCoeff_map (φ : MvPowerSeries σ R) : + constantCoeff σ S (map σ f φ) = f (constantCoeff σ R φ) := + rfl +#align mv_power_series.constant_coeff_map MvPowerSeries.constantCoeff_map + +@[simp] +theorem map_monomial (n : σ →₀ ℕ) (a : R) : map σ f (monomial R n a) = monomial S n (f a) := by + classical + ext m + simp [coeff_monomial, apply_ite f] +#align mv_power_series.map_monomial MvPowerSeries.map_monomial + +@[simp] +theorem map_C (a : R) : map σ f (C σ R a) = C σ S (f a) := + map_monomial _ _ _ +set_option linter.uppercaseLean3 false in +#align mv_power_series.map_C MvPowerSeries.map_C + +@[simp] +theorem map_X (s : σ) : map σ f (X s) = X s := by simp [MvPowerSeries.X] +set_option linter.uppercaseLean3 false in +#align mv_power_series.map_X MvPowerSeries.map_X + +end Map + +section Semiring + +variable [Semiring R] + +theorem X_pow_dvd_iff {s : σ} {n : ℕ} {φ : MvPowerSeries σ R} : + (X s : MvPowerSeries σ R) ^ n ∣ φ ↔ ∀ m : σ →₀ ℕ, m s < n → coeff R m φ = 0 := by + classical + constructor + · rintro ⟨φ, rfl⟩ m h + rw [coeff_mul, Finset.sum_eq_zero] + rintro ⟨i, j⟩ hij + rw [coeff_X_pow, if_neg, zero_mul] + contrapose! h + dsimp at h + subst i + rw [mem_antidiagonal] at hij + rw [← hij, Finsupp.add_apply, Finsupp.single_eq_same] + exact Nat.le_add_right n _ + · intro h + refine' ⟨fun m => coeff R (m + single s n) φ, _⟩ + ext m + by_cases H : m - single s n + single s n = m + · rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)] + · rw [coeff_X_pow, if_pos rfl, one_mul] + simpa using congr_arg (fun m : σ →₀ ℕ => coeff R m φ) H.symm + · rintro ⟨i, j⟩ hij hne + rw [mem_antidiagonal] at hij + rw [coeff_X_pow] + split_ifs with hi + · exfalso + apply hne + rw [← hij, ← hi, Prod.mk.inj_iff] + refine' ⟨rfl, _⟩ + ext t + simp only [add_tsub_cancel_left, Finsupp.add_apply, Finsupp.tsub_apply] + · exact zero_mul _ + · intro hni + exfalso + apply hni + rwa [mem_antidiagonal, add_comm] + · rw [h, coeff_mul, Finset.sum_eq_zero] + · rintro ⟨i, j⟩ hij + rw [mem_antidiagonal] at hij + rw [coeff_X_pow] + split_ifs with hi + · exfalso + apply H + rw [← hij, hi] + ext + rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm] + · exact zero_mul _ + · contrapose! H + ext t + by_cases hst : s = t + · subst t + simpa using tsub_add_cancel_of_le H + · simp [Finsupp.single_apply, hst] +set_option linter.uppercaseLean3 false in +#align mv_power_series.X_pow_dvd_iff MvPowerSeries.X_pow_dvd_iff + +theorem X_dvd_iff {s : σ} {φ : MvPowerSeries σ R} : + (X s : MvPowerSeries σ R) ∣ φ ↔ ∀ m : σ →₀ ℕ, m s = 0 → coeff R m φ = 0 := by + rw [← pow_one (X s : MvPowerSeries σ R), X_pow_dvd_iff] + constructor <;> intro h m hm + · exact h m (hm.symm ▸ zero_lt_one) + · exact h m (Nat.eq_zero_of_le_zero <| Nat.le_of_succ_le_succ hm) +set_option linter.uppercaseLean3 false in +#align mv_power_series.X_dvd_iff MvPowerSeries.X_dvd_iff + +end Semiring + +section CommSemiring + +open Finset.HasAntidiagonal Finset + +variable {R : Type*} [CommSemiring R] {ι : Type*} [DecidableEq ι] + +/-- Coefficients of a product of power series -/ +theorem coeff_prod [DecidableEq σ] + (f : ι → MvPowerSeries σ R) (d : σ →₀ ℕ) (s : Finset ι) : + coeff R d (∏ j in s, f j) = + ∑ l in piAntidiagonal s d, + ∏ i in s, coeff R (l i) (f i) := by + induction s using Finset.induction_on generalizing d with + | empty => + simp only [prod_empty, sum_const, nsmul_eq_mul, mul_one, coeff_one, piAntidiagonal_empty] + split_ifs + · simp only [card_singleton, Nat.cast_one] + · simp only [card_empty, Nat.cast_zero] + | @insert a s ha ih => + rw [piAntidiagonal_insert ha, prod_insert ha, coeff_mul, sum_biUnion] + · apply Finset.sum_congr rfl + · simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall] + rintro u v rfl + rw [ih, Finset.mul_sum, ← Finset.sum_attach] + apply Finset.sum_congr rfl + simp only [mem_attach, Finset.prod_insert ha, Function.update_same, forall_true_left, + Subtype.forall] + rintro x - + rw [Finset.prod_congr rfl] + intro i hi + rw [Function.update_noteq] + exact ne_of_mem_of_not_mem hi ha + · simp only [Set.PairwiseDisjoint, Set.Pairwise, mem_coe, mem_antidiagonal, ne_eq, + disjoint_left, mem_map, mem_attach, Function.Embedding.coeFn_mk, true_and, Subtype.exists, + exists_prop, not_exists, not_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, + Prod.forall, Prod.mk.injEq] + rintro u v rfl u' v' huv h k - l - hkl + obtain rfl : u' = u := by + simpa only [Finsupp.coe_update, Function.update_same] using DFunLike.congr_fun hkl a + simp only [add_right_inj] at huv + exact h rfl huv.symm + +end CommSemiring + +section Algebra + +variable {A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] + +instance : Algebra R (MvPowerSeries σ A) := + { + show Module R (MvPowerSeries σ A) by infer_instance with + commutes' := fun a φ => by + ext n + simp [Algebra.commutes] + smul_def' := fun a σ => by + ext n + simp [(coeff A n).map_smul_of_tower a, Algebra.smul_def] + toRingHom := (MvPowerSeries.map σ (algebraMap R A)).comp (C σ R) } + +theorem c_eq_algebraMap : C σ R = algebraMap R (MvPowerSeries σ R) := + rfl +set_option linter.uppercaseLean3 false in +#align mv_power_series.C_eq_algebra_map MvPowerSeries.c_eq_algebraMap + +theorem algebraMap_apply {r : R} : + algebraMap R (MvPowerSeries σ A) r = C σ A (algebraMap R A r) := by + change (MvPowerSeries.map σ (algebraMap R A)).comp (C σ R) r = _ + simp +#align mv_power_series.algebra_map_apply MvPowerSeries.algebraMap_apply + +instance [Nonempty σ] [Nontrivial R] : Nontrivial (Subalgebra R (MvPowerSeries σ R)) := + ⟨⟨⊥, ⊤, by + classical + rw [Ne.def, SetLike.ext_iff, not_forall] + inhabit σ + refine' ⟨X default, _⟩ + simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true_iff, Algebra.mem_top] + intro x + rw [ext_iff, not_forall] + refine' ⟨Finsupp.single default 1, _⟩ + simp [algebraMap_apply, coeff_C]⟩⟩ + +end Algebra + + +end MvPowerSeries + +namespace MvPolynomial + +open Finsupp + +variable {σ : Type*} {R : Type*} [CommSemiring R] (φ ψ : MvPolynomial σ R) + +-- Porting note: added so we can add the `@[coe]` attribute +/-- The natural inclusion from multivariate polynomials into multivariate formal power series.-/ +@[coe] +def toMvPowerSeries : MvPolynomial σ R → MvPowerSeries σ R := + fun φ n => coeff n φ + +/-- The natural inclusion from multivariate polynomials into multivariate formal power series.-/ +instance coeToMvPowerSeries : Coe (MvPolynomial σ R) (MvPowerSeries σ R) := + ⟨toMvPowerSeries⟩ +#align mv_polynomial.coe_to_mv_power_series MvPolynomial.coeToMvPowerSeries + +theorem coe_def : (φ : MvPowerSeries σ R) = fun n => coeff n φ := + rfl +#align mv_polynomial.coe_def MvPolynomial.coe_def + +@[simp, norm_cast] +theorem coeff_coe (n : σ →₀ ℕ) : MvPowerSeries.coeff R n ↑φ = coeff n φ := + rfl +#align mv_polynomial.coeff_coe MvPolynomial.coeff_coe + +@[simp, norm_cast] +theorem coe_monomial (n : σ →₀ ℕ) (a : R) : + (monomial n a : MvPowerSeries σ R) = MvPowerSeries.monomial R n a := + MvPowerSeries.ext fun m => by + classical + rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial] + split_ifs with h₁ h₂ <;> first |rfl|subst m; contradiction +#align mv_polynomial.coe_monomial MvPolynomial.coe_monomial + +@[simp, norm_cast] +theorem coe_zero : ((0 : MvPolynomial σ R) : MvPowerSeries σ R) = 0 := + rfl +#align mv_polynomial.coe_zero MvPolynomial.coe_zero + +@[simp, norm_cast] +theorem coe_one : ((1 : MvPolynomial σ R) : MvPowerSeries σ R) = 1 := + coe_monomial _ _ +#align mv_polynomial.coe_one MvPolynomial.coe_one + +@[simp, norm_cast] +theorem coe_add : ((φ + ψ : MvPolynomial σ R) : MvPowerSeries σ R) = φ + ψ := + rfl +#align mv_polynomial.coe_add MvPolynomial.coe_add + +@[simp, norm_cast] +theorem coe_mul : ((φ * ψ : MvPolynomial σ R) : MvPowerSeries σ R) = φ * ψ := + MvPowerSeries.ext fun n => by + classical + simp only [coeff_coe, MvPowerSeries.coeff_mul, coeff_mul] +#align mv_polynomial.coe_mul MvPolynomial.coe_mul + +@[simp, norm_cast] +theorem coe_C (a : R) : ((C a : MvPolynomial σ R) : MvPowerSeries σ R) = MvPowerSeries.C σ R a := + coe_monomial _ _ +set_option linter.uppercaseLean3 false in +#align mv_polynomial.coe_C MvPolynomial.coe_C + +set_option linter.deprecated false in +@[simp, norm_cast] +theorem coe_bit0 : + ((bit0 φ : MvPolynomial σ R) : MvPowerSeries σ R) = bit0 (φ : MvPowerSeries σ R) := + coe_add _ _ +#align mv_polynomial.coe_bit0 MvPolynomial.coe_bit0 + +set_option linter.deprecated false in +@[simp, norm_cast] +theorem coe_bit1 : + ((bit1 φ : MvPolynomial σ R) : MvPowerSeries σ R) = bit1 (φ : MvPowerSeries σ R) := by + rw [bit1, bit1, coe_add, coe_one, coe_bit0] +#align mv_polynomial.coe_bit1 MvPolynomial.coe_bit1 + +@[simp, norm_cast] +theorem coe_X (s : σ) : ((X s : MvPolynomial σ R) : MvPowerSeries σ R) = MvPowerSeries.X s := + coe_monomial _ _ +set_option linter.uppercaseLean3 false in +#align mv_polynomial.coe_X MvPolynomial.coe_X + +variable (σ R) + +theorem coe_injective : Function.Injective (Coe.coe : MvPolynomial σ R → MvPowerSeries σ R) := + fun x y h => by + ext + simp_rw [← coeff_coe] + congr +#align mv_polynomial.coe_injective MvPolynomial.coe_injective + +variable {σ R φ ψ} + +@[simp, norm_cast] +theorem coe_inj : (φ : MvPowerSeries σ R) = ψ ↔ φ = ψ := + (coe_injective σ R).eq_iff +#align mv_polynomial.coe_inj MvPolynomial.coe_inj + +@[simp] +theorem coe_eq_zero_iff : (φ : MvPowerSeries σ R) = 0 ↔ φ = 0 := by rw [← coe_zero, coe_inj] +#align mv_polynomial.coe_eq_zero_iff MvPolynomial.coe_eq_zero_iff + +@[simp] +theorem coe_eq_one_iff : (φ : MvPowerSeries σ R) = 1 ↔ φ = 1 := by rw [← coe_one, coe_inj] +#align mv_polynomial.coe_eq_one_iff MvPolynomial.coe_eq_one_iff + +/-- The coercion from multivariate polynomials to multivariate power series +as a ring homomorphism. +-/ +def coeToMvPowerSeries.ringHom : MvPolynomial σ R →+* MvPowerSeries σ R where + toFun := (Coe.coe : MvPolynomial σ R → MvPowerSeries σ R) + map_zero' := coe_zero + map_one' := coe_one + map_add' := coe_add + map_mul' := coe_mul +#align mv_polynomial.coe_to_mv_power_series.ring_hom MvPolynomial.coeToMvPowerSeries.ringHom + +@[simp, norm_cast] +theorem coe_pow (n : ℕ) : + ((φ ^ n : MvPolynomial σ R) : MvPowerSeries σ R) = (φ : MvPowerSeries σ R) ^ n := + coeToMvPowerSeries.ringHom.map_pow _ _ +#align mv_polynomial.coe_pow MvPolynomial.coe_pow + +variable (φ ψ) + +@[simp] +theorem coeToMvPowerSeries.ringHom_apply : coeToMvPowerSeries.ringHom φ = φ := + rfl +#align mv_polynomial.coe_to_mv_power_series.ring_hom_apply MvPolynomial.coeToMvPowerSeries.ringHom_apply + +section Algebra + +variable (A : Type*) [CommSemiring A] [Algebra R A] + +/-- The coercion from multivariate polynomials to multivariate power series +as an algebra homomorphism. +-/ +def coeToMvPowerSeries.algHom : MvPolynomial σ R →ₐ[R] MvPowerSeries σ A := + { (MvPowerSeries.map σ (algebraMap R A)).comp coeToMvPowerSeries.ringHom with + commutes' := fun r => by simp [algebraMap_apply, MvPowerSeries.algebraMap_apply] } +#align mv_polynomial.coe_to_mv_power_series.alg_hom MvPolynomial.coeToMvPowerSeries.algHom + +@[simp] +theorem coeToMvPowerSeries.algHom_apply : + coeToMvPowerSeries.algHom A φ = MvPowerSeries.map σ (algebraMap R A) ↑φ := + rfl +#align mv_polynomial.coe_to_mv_power_series.alg_hom_apply MvPolynomial.coeToMvPowerSeries.algHom_apply + +end Algebra + +end MvPolynomial + +namespace MvPowerSeries + +variable {σ R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A] (f : MvPowerSeries σ R) + +instance algebraMvPolynomial : Algebra (MvPolynomial σ R) (MvPowerSeries σ A) := + RingHom.toAlgebra (MvPolynomial.coeToMvPowerSeries.algHom A).toRingHom +#align mv_power_series.algebra_mv_polynomial MvPowerSeries.algebraMvPolynomial + +instance algebraMvPowerSeries : Algebra (MvPowerSeries σ R) (MvPowerSeries σ A) := + (map σ (algebraMap R A)).toAlgebra +#align mv_power_series.algebra_mv_power_series MvPowerSeries.algebraMvPowerSeries + +variable (A) + +theorem algebraMap_apply' (p : MvPolynomial σ R) : + algebraMap (MvPolynomial σ R) (MvPowerSeries σ A) p = map σ (algebraMap R A) p := + rfl +#align mv_power_series.algebra_map_apply' MvPowerSeries.algebraMap_apply' + +theorem algebraMap_apply'' : + algebraMap (MvPowerSeries σ R) (MvPowerSeries σ A) f = map σ (algebraMap R A) f := + rfl +#align mv_power_series.algebra_map_apply'' MvPowerSeries.algebraMap_apply'' + +end MvPowerSeries + +end diff --git a/Mathlib/RingTheory/MvPowerSeries/Inverse.lean b/Mathlib/RingTheory/MvPowerSeries/Inverse.lean new file mode 100644 index 0000000000000..4b9547ecddaff --- /dev/null +++ b/Mathlib/RingTheory/MvPowerSeries/Inverse.lean @@ -0,0 +1,308 @@ +/- +Copyright (c) 2019 Johan Commelin. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johan Commelin, Kenny Lau +-/ + +import Mathlib.RingTheory.MvPowerSeries.Basic +import Mathlib.RingTheory.Ideal.LocalRing + + +#align_import ring_theory.power_series.basic from "leanprover-community/mathlib"@"2d5739b61641ee4e7e53eca5688a08f66f2e6a60" + +/-! +# Formal (multivariate) power series - Inverses + +This file defines multivariate formal power series and develops the basic +properties of these objects, when it comes about multiplicative inverses. + +For `φ : MvPowerSeries σ R` and `u : Rˣ` is the constant coefficient of `φ`, +`MvPowerSeries.invOfUnit φ u` is a formal power series such, +and `MvPowerSeries.mul_invOfUnit` proves that `φ * invOfUnit φ u = 1`. +The construction of the power series `invOfUnit` is done by writing that +relation and solving and for its coefficients by induction. + +Over a field, all power series `φ` have an “inverse” `MvPowerSeries.inv φ`, +which is `0` if and only if the constant coefficient of `φ` is zero +(by `MvPowerSeries.inv_eq_zero`), +and `MvPowerSeries.mul_inv_cancel` asserts the equality `φ * φ⁻¹ = 1` when +the constant coefficient of `φ` is nonzero. + +Instances are defined: + +* Formal power series over a local ring form a local ring. +* The morphism `MvPowerSeries.map σ f : MvPowerSeries σ A →* MvPowerSeries σ B` + induced by a local morphism `f : A →+* B` (`IsLocalRingHom f`) + of commutative rings is a *local* morphism. + +-/ + + +noncomputable section + +open BigOperators + +open Finset (antidiagonal mem_antidiagonal) + +namespace MvPowerSeries + +open Finsupp + +variable {σ R : Type*} + +section Ring + +variable [Ring R] + +/- +The inverse of a multivariate formal power series is defined by +well-founded recursion on the coefficients of the inverse. +-/ +/-- Auxiliary definition that unifies + the totalised inverse formal power series `(_)⁻¹` and + the inverse formal power series that depends on + an inverse of the constant coefficient `invOfUnit`.-/ +protected noncomputable def inv.aux (a : R) (φ : MvPowerSeries σ R) : MvPowerSeries σ R + | n => + letI := Classical.decEq σ + if n = 0 then a + else + -a * + ∑ x in antidiagonal n, if _ : x.2 < n then coeff R x.1 φ * inv.aux a φ x.2 else 0 +termination_by n => n +#align mv_power_series.inv.aux MvPowerSeries.inv.aux + +theorem coeff_inv_aux [DecidableEq σ] (n : σ →₀ ℕ) (a : R) (φ : MvPowerSeries σ R) : + coeff R n (inv.aux a φ) = + if n = 0 then a + else + -a * + ∑ x in antidiagonal n, if x.2 < n then coeff R x.1 φ * coeff R x.2 (inv.aux a φ) else 0 := + show inv.aux a φ n = _ by + cases Subsingleton.elim ‹DecidableEq σ› (Classical.decEq σ) + rw [inv.aux] + rfl +#align mv_power_series.coeff_inv_aux MvPowerSeries.coeff_inv_aux + +/-- A multivariate formal power series is invertible if the constant coefficient is invertible.-/ +def invOfUnit (φ : MvPowerSeries σ R) (u : Rˣ) : MvPowerSeries σ R := + inv.aux (↑u⁻¹) φ +#align mv_power_series.inv_of_unit MvPowerSeries.invOfUnit + +theorem coeff_invOfUnit [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (u : Rˣ) : + coeff R n (invOfUnit φ u) = + if n = 0 then ↑u⁻¹ + else + -↑u⁻¹ * + ∑ x in antidiagonal n, + if x.2 < n then coeff R x.1 φ * coeff R x.2 (invOfUnit φ u) else 0 := by + convert coeff_inv_aux n (↑u⁻¹) φ +#align mv_power_series.coeff_inv_of_unit MvPowerSeries.coeff_invOfUnit + +@[simp] +theorem constantCoeff_invOfUnit (φ : MvPowerSeries σ R) (u : Rˣ) : + constantCoeff σ R (invOfUnit φ u) = ↑u⁻¹ := by + classical + rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl] +#align mv_power_series.constant_coeff_inv_of_unit MvPowerSeries.constantCoeff_invOfUnit + +theorem mul_invOfUnit (φ : MvPowerSeries σ R) (u : Rˣ) (h : constantCoeff σ R φ = u) : + φ * invOfUnit φ u = 1 := + ext fun n => + letI := Classical.decEq (σ →₀ ℕ) + if H : n = 0 then by + rw [H] + simp [coeff_mul, support_single_ne_zero, h] + else by + classical + have : ((0 : σ →₀ ℕ), n) ∈ antidiagonal n := by rw [mem_antidiagonal, zero_add] + rw [coeff_one, if_neg H, coeff_mul, ← Finset.insert_erase this, + Finset.sum_insert (Finset.not_mem_erase _ _), coeff_zero_eq_constantCoeff_apply, h, + coeff_invOfUnit, if_neg H, neg_mul, mul_neg, Units.mul_inv_cancel_left, ← + Finset.insert_erase this, Finset.sum_insert (Finset.not_mem_erase _ _), + Finset.insert_erase this, if_neg (not_lt_of_ge <| le_rfl), zero_add, add_comm, ← + sub_eq_add_neg, sub_eq_zero, Finset.sum_congr rfl] + rintro ⟨i, j⟩ hij + rw [Finset.mem_erase, mem_antidiagonal] at hij + cases' hij with h₁ h₂ + subst n + rw [if_pos] + suffices (0 : _) + j < i + j by simpa + apply add_lt_add_right + constructor + · intro s + exact Nat.zero_le _ + · intro H + apply h₁ + suffices i = 0 by simp [this] + ext1 s + exact Nat.eq_zero_of_le_zero (H s) +#align mv_power_series.mul_inv_of_unit MvPowerSeries.mul_invOfUnit + +end Ring + +section CommRing + +variable [CommRing R] + +/-- Multivariate formal power series over a local ring form a local ring. -/ +instance [LocalRing R] : LocalRing (MvPowerSeries σ R) := + LocalRing.of_isUnit_or_isUnit_one_sub_self <| by + intro φ + rcases LocalRing.isUnit_or_isUnit_one_sub_self (constantCoeff σ R φ) with (⟨u, h⟩ | ⟨u, h⟩) <;> + [left; right] <;> + · refine' isUnit_of_mul_eq_one _ _ (mul_invOfUnit _ u _) + simpa using h.symm + +-- TODO(jmc): once adic topology lands, show that this is complete +end CommRing + +section LocalRing + +variable {S : Type*} [CommRing R] [CommRing S] (f : R →+* S) [IsLocalRingHom f] + +-- Thanks to the linter for informing us that this instance does +-- not actually need R and S to be local rings! +/-- The map between multivariate formal power series over the same indexing set + induced by a local ring hom `A → B` is local -/ +instance map.isLocalRingHom : IsLocalRingHom (map σ f) := + ⟨by + rintro φ ⟨ψ, h⟩ + replace h := congr_arg (constantCoeff σ S) h + rw [constantCoeff_map] at h + have : IsUnit (constantCoeff σ S ↑ψ) := isUnit_constantCoeff (↑ψ) ψ.isUnit + rw [h] at this + rcases isUnit_of_map_unit f _ this with ⟨c, hc⟩ + exact isUnit_of_mul_eq_one φ (invOfUnit φ c) (mul_invOfUnit φ c hc.symm)⟩ +#align mv_power_series.map.is_local_ring_hom MvPowerSeries.map.isLocalRingHom + +end LocalRing + +section Field + +variable {k : Type*} [Field k] + +/-- The inverse `1/f` of a multivariable power series `f` over a field -/ +protected def inv (φ : MvPowerSeries σ k) : MvPowerSeries σ k := + inv.aux (constantCoeff σ k φ)⁻¹ φ +#align mv_power_series.inv MvPowerSeries.inv + +instance : Inv (MvPowerSeries σ k) := + ⟨MvPowerSeries.inv⟩ + +theorem coeff_inv [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ k) : + coeff k n φ⁻¹ = + if n = 0 then (constantCoeff σ k φ)⁻¹ + else + -(constantCoeff σ k φ)⁻¹ * + ∑ x in antidiagonal n, if x.2 < n then coeff k x.1 φ * coeff k x.2 φ⁻¹ else 0 := + coeff_inv_aux n _ φ +#align mv_power_series.coeff_inv MvPowerSeries.coeff_inv + +@[simp] +theorem constantCoeff_inv (φ : MvPowerSeries σ k) : + constantCoeff σ k φ⁻¹ = (constantCoeff σ k φ)⁻¹ := by + classical + rw [← coeff_zero_eq_constantCoeff_apply, coeff_inv, if_pos rfl] +#align mv_power_series.constant_coeff_inv MvPowerSeries.constantCoeff_inv + +theorem inv_eq_zero {φ : MvPowerSeries σ k} : φ⁻¹ = 0 ↔ constantCoeff σ k φ = 0 := + ⟨fun h => by simpa using congr_arg (constantCoeff σ k) h, fun h => + ext fun n => by + classical + rw [coeff_inv] + split_ifs <;> + simp only [h, map_zero, zero_mul, inv_zero, neg_zero]⟩ +#align mv_power_series.inv_eq_zero MvPowerSeries.inv_eq_zero + +@[simp] +theorem zero_inv : (0 : MvPowerSeries σ k)⁻¹ = 0 := by + rw [inv_eq_zero, constantCoeff_zero] +#align mv_power_series.zero_inv MvPowerSeries.zero_inv + +-- Porting note (#10618): simp can prove this. +-- @[simp] +theorem invOfUnit_eq (φ : MvPowerSeries σ k) (h : constantCoeff σ k φ ≠ 0) : + invOfUnit φ (Units.mk0 _ h) = φ⁻¹ := + rfl +#align mv_power_series.inv_of_unit_eq MvPowerSeries.invOfUnit_eq + +@[simp] +theorem invOfUnit_eq' (φ : MvPowerSeries σ k) (u : Units k) (h : constantCoeff σ k φ = u) : + invOfUnit φ u = φ⁻¹ := by + rw [← invOfUnit_eq φ (h.symm ▸ u.ne_zero)] + apply congrArg (invOfUnit φ) + rw [Units.ext_iff] + exact h.symm +#align mv_power_series.inv_of_unit_eq' MvPowerSeries.invOfUnit_eq' + +@[simp] +protected theorem mul_inv_cancel (φ : MvPowerSeries σ k) (h : constantCoeff σ k φ ≠ 0) : + φ * φ⁻¹ = 1 := by rw [← invOfUnit_eq φ h, mul_invOfUnit φ (Units.mk0 _ h) rfl] +#align mv_power_series.mul_inv_cancel MvPowerSeries.mul_inv_cancel + +@[simp] +protected theorem inv_mul_cancel (φ : MvPowerSeries σ k) (h : constantCoeff σ k φ ≠ 0) : + φ⁻¹ * φ = 1 := by rw [mul_comm, φ.mul_inv_cancel h] +#align mv_power_series.inv_mul_cancel MvPowerSeries.inv_mul_cancel + +protected theorem eq_mul_inv_iff_mul_eq {φ₁ φ₂ φ₃ : MvPowerSeries σ k} + (h : constantCoeff σ k φ₃ ≠ 0) : φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂ := + ⟨fun k => by simp [k, mul_assoc, MvPowerSeries.inv_mul_cancel _ h], fun k => by + simp [← k, mul_assoc, MvPowerSeries.mul_inv_cancel _ h]⟩ +#align mv_power_series.eq_mul_inv_iff_mul_eq MvPowerSeries.eq_mul_inv_iff_mul_eq + +protected theorem eq_inv_iff_mul_eq_one {φ ψ : MvPowerSeries σ k} (h : constantCoeff σ k ψ ≠ 0) : + φ = ψ⁻¹ ↔ φ * ψ = 1 := by rw [← MvPowerSeries.eq_mul_inv_iff_mul_eq h, one_mul] +#align mv_power_series.eq_inv_iff_mul_eq_one MvPowerSeries.eq_inv_iff_mul_eq_one + +protected theorem inv_eq_iff_mul_eq_one {φ ψ : MvPowerSeries σ k} (h : constantCoeff σ k ψ ≠ 0) : + ψ⁻¹ = φ ↔ φ * ψ = 1 := by rw [eq_comm, MvPowerSeries.eq_inv_iff_mul_eq_one h] +#align mv_power_series.inv_eq_iff_mul_eq_one MvPowerSeries.inv_eq_iff_mul_eq_one + +@[simp] +protected theorem mul_inv_rev (φ ψ : MvPowerSeries σ k) : + (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹ := by + by_cases h : constantCoeff σ k (φ * ψ) = 0 + · rw [inv_eq_zero.mpr h] + simp only [map_mul, mul_eq_zero] at h + -- we don't have `NoZeroDivisors (MvPowerSeries σ k)` yet, + cases' h with h h <;> simp [inv_eq_zero.mpr h] + · rw [MvPowerSeries.inv_eq_iff_mul_eq_one h] + simp only [not_or, map_mul, mul_eq_zero] at h + rw [← mul_assoc, mul_assoc _⁻¹, MvPowerSeries.inv_mul_cancel _ h.left, mul_one, + MvPowerSeries.inv_mul_cancel _ h.right] +#align mv_power_series.mul_inv_rev MvPowerSeries.mul_inv_rev + +instance : InvOneClass (MvPowerSeries σ k) := + { inferInstanceAs (One (MvPowerSeries σ k)), + inferInstanceAs (Inv (MvPowerSeries σ k)) with + inv_one := by + rw [MvPowerSeries.inv_eq_iff_mul_eq_one, mul_one] + simp } + +@[simp] +theorem C_inv (r : k) : (C σ k r)⁻¹ = C σ k r⁻¹ := by + rcases eq_or_ne r 0 with (rfl | hr) + · simp + rw [MvPowerSeries.inv_eq_iff_mul_eq_one, ← map_mul, inv_mul_cancel hr, map_one] + simpa using hr +set_option linter.uppercaseLean3 false in +#align mv_power_series.C_inv MvPowerSeries.C_inv + +@[simp] +theorem X_inv (s : σ) : (X s : MvPowerSeries σ k)⁻¹ = 0 := by + rw [inv_eq_zero, constantCoeff_X] +set_option linter.uppercaseLean3 false in +#align mv_power_series.X_inv MvPowerSeries.X_inv + +@[simp] +theorem smul_inv (r : k) (φ : MvPowerSeries σ k) : (r • φ)⁻¹ = r⁻¹ • φ⁻¹ := by + simp [smul_eq_C_mul, mul_comm] +#align mv_power_series.smul_inv MvPowerSeries.smul_inv + +end Field + +end MvPowerSeries + +end diff --git a/Mathlib/RingTheory/MvPowerSeries/Trunc.lean b/Mathlib/RingTheory/MvPowerSeries/Trunc.lean new file mode 100644 index 0000000000000..c60e3b6f22994 --- /dev/null +++ b/Mathlib/RingTheory/MvPowerSeries/Trunc.lean @@ -0,0 +1,111 @@ +/- +Copyright (c) 2019 Johan Commelin. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johan Commelin, Kenny Lau +-/ + +import Mathlib.RingTheory.MvPowerSeries.Basic +import Mathlib.Data.Finsupp.Interval + +/-! + +# Formal (multivariate) power series - Truncation + +`MvPowerSeries.trunc n φ` truncates a formal multivariate power series +to the multivariate polynomial that has the same coefficients as `φ`, +for all `m < n`, and `0` otherwise. + +Note that here, `m` and `n` have types `σ →₀ ℕ`, +so that `m < n` means that `m ≠ n` and `m s ≤ n s` for all `s : σ`. + +-/ + + +noncomputable section + +open BigOperators + +open Finset (antidiagonal mem_antidiagonal) + +namespace MvPowerSeries + +open Finsupp + +variable {σ R : Type*} + +section Trunc + +variable [CommSemiring R] (n : σ →₀ ℕ) + +/-- Auxiliary definition for the truncation function. -/ +def truncFun (φ : MvPowerSeries σ R) : MvPolynomial σ R := + ∑ m in Finset.Iio n, MvPolynomial.monomial m (coeff R m φ) +#align mv_power_series.trunc_fun MvPowerSeries.truncFun + +theorem coeff_truncFun (m : σ →₀ ℕ) (φ : MvPowerSeries σ R) : + (truncFun n φ).coeff m = if m < n then coeff R m φ else 0 := by + classical + simp [truncFun, MvPolynomial.coeff_sum] +#align mv_power_series.coeff_trunc_fun MvPowerSeries.coeff_truncFun + +variable (R) + +/-- The `n`th truncation of a multivariate formal power series to a multivariate polynomial -/ +def trunc : MvPowerSeries σ R →+ MvPolynomial σ R where + toFun := truncFun n + map_zero' := by + classical + ext + simp [coeff_truncFun] + map_add' := by + classical + intros x y + ext m + simp only [coeff_truncFun, MvPolynomial.coeff_add] + split_ifs + · rw [map_add] + · rw [zero_add] + +#align mv_power_series.trunc MvPowerSeries.trunc + +variable {R} + +theorem coeff_trunc (m : σ →₀ ℕ) (φ : MvPowerSeries σ R) : + (trunc R n φ).coeff m = if m < n then coeff R m φ else 0 := by + classical simp [trunc, coeff_truncFun] +#align mv_power_series.coeff_trunc MvPowerSeries.coeff_trunc + +@[simp] +theorem trunc_one (n : σ →₀ ℕ) (hnn : n ≠ 0) : trunc R n 1 = 1 := + MvPolynomial.ext _ _ fun m => by + classical + rw [coeff_trunc, coeff_one] + split_ifs with H H' + · subst m + simp + · symm + rw [MvPolynomial.coeff_one] + exact if_neg (Ne.symm H') + · symm + rw [MvPolynomial.coeff_one] + refine' if_neg _ + rintro rfl + apply H + exact Ne.bot_lt hnn +#align mv_power_series.trunc_one MvPowerSeries.trunc_one + +@[simp] +theorem trunc_c (n : σ →₀ ℕ) (hnn : n ≠ 0) (a : R) : trunc R n (C σ R a) = MvPolynomial.C a := + MvPolynomial.ext _ _ fun m => by + classical + rw [coeff_trunc, coeff_C, MvPolynomial.coeff_C] + split_ifs with H <;> first |rfl|try simp_all + exfalso; apply H; subst m; exact Ne.bot_lt hnn +set_option linter.uppercaseLean3 false in +#align mv_power_series.trunc_C MvPowerSeries.trunc_c + +end Trunc + +end MvPowerSeries + +end diff --git a/Mathlib/RingTheory/PowerSeries/Basic.lean b/Mathlib/RingTheory/PowerSeries/Basic.lean index 5d1f25ebd4007..470f2580655f6 100644 --- a/Mathlib/RingTheory/PowerSeries/Basic.lean +++ b/Mathlib/RingTheory/PowerSeries/Basic.lean @@ -3,1294 +3,55 @@ Copyright (c) 2019 Johan Commelin. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin, Kenny Lau -/ -import Mathlib.Data.Finsupp.Interval -import Mathlib.Data.MvPolynomial.Basic +import Mathlib.RingTheory.MvPowerSeries.Basic +import Mathlib.Data.Polynomial.Basic import Mathlib.Data.Polynomial.AlgebraMap -import Mathlib.Data.Polynomial.Coeff -import Mathlib.LinearAlgebra.StdBasis -import Mathlib.RingTheory.Ideal.LocalRing -import Mathlib.RingTheory.Multiplicity -import Mathlib.Tactic.Linarith -import Mathlib.Data.Finset.PiAntidiagonal #align_import ring_theory.power_series.basic from "leanprover-community/mathlib"@"2d5739b61641ee4e7e53eca5688a08f66f2e6a60" /-! -# Formal power series +# Formal power series (in one variable) -This file defines (multivariate) formal power series +This file defines (univariate) formal power series and develops the basic properties of these objects. A formal power series is to a polynomial like an infinite sum is to a finite sum. -We provide the natural inclusion from polynomials to formal power series. - -## Generalities - -The file starts with setting up the (semi)ring structure on multivariate power series. - -`trunc n φ` truncates a formal power series to the polynomial -that has the same coefficients as `φ`, for all `m < n`, and `0` otherwise. - -If the constant coefficient of a formal power series is invertible, -then this formal power series is invertible. - -Formal power series over a local ring form a local ring. - -## Formal power series in one variable - -We prove that if the ring of coefficients is an integral domain, -then formal power series in one variable form an integral domain. - -The `order` of a formal power series `φ` is the multiplicity of the variable `X` in `φ`. - -If the coefficients form an integral domain, then `order` is a valuation -(`order_mul`, `le_order_add`). - -## Implementation notes - -In this file we define multivariate formal power series with -variables indexed by `σ` and coefficients in `R` as -`MvPowerSeries σ R := (σ →₀ ℕ) → R`. -Unfortunately there is not yet enough API to show that they are the completion -of the ring of multivariate polynomials. However, we provide most of the infrastructure -that is needed to do this. Once I-adic completion (topological or algebraic) is available -it should not be hard to fill in the details. - -Formal power series in one variable are defined as -`PowerSeries R := MvPowerSeries Unit R`. - -This allows us to port a lot of proofs and properties -from the multivariate case to the single variable case. -However, it means that formal power series are indexed by `Unit →₀ ℕ`, -which is of course canonically isomorphic to `ℕ`. -We then build some glue to treat formal power series as if they are indexed by `ℕ`. -Occasionally this leads to proofs that are uglier than expected. --/ - - -noncomputable section - -open BigOperators Polynomial - -open Finset (antidiagonal mem_antidiagonal) - -/-- Multivariate formal power series, where `σ` is the index set of the variables -and `R` is the coefficient ring.-/ -def MvPowerSeries (σ : Type*) (R : Type*) := - (σ →₀ ℕ) → R -#align mv_power_series MvPowerSeries - -namespace MvPowerSeries - -open Finsupp - -variable {σ R : Type*} - -instance [Inhabited R] : Inhabited (MvPowerSeries σ R) := - ⟨fun _ => default⟩ - -instance [Zero R] : Zero (MvPowerSeries σ R) := - Pi.instZero - -instance [AddMonoid R] : AddMonoid (MvPowerSeries σ R) := - Pi.addMonoid - -instance [AddGroup R] : AddGroup (MvPowerSeries σ R) := - Pi.addGroup - -instance [AddCommMonoid R] : AddCommMonoid (MvPowerSeries σ R) := - Pi.addCommMonoid - -instance [AddCommGroup R] : AddCommGroup (MvPowerSeries σ R) := - Pi.addCommGroup - -instance [Nontrivial R] : Nontrivial (MvPowerSeries σ R) := - Function.nontrivial - -instance {A} [Semiring R] [AddCommMonoid A] [Module R A] : Module R (MvPowerSeries σ A) := - Pi.module _ _ _ - -instance {A S} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R A] [Module S A] [SMul R S] - [IsScalarTower R S A] : IsScalarTower R S (MvPowerSeries σ A) := - Pi.isScalarTower - -section Semiring - -variable (R) [Semiring R] - -/-- The `n`th monomial with coefficient `a` as multivariate formal power series.-/ -def monomial (n : σ →₀ ℕ) : R →ₗ[R] MvPowerSeries σ R := - letI := Classical.decEq σ - LinearMap.stdBasis R (fun _ ↦ R) n -#align mv_power_series.monomial MvPowerSeries.monomial - -/-- The `n`th coefficient of a multivariate formal power series.-/ -def coeff (n : σ →₀ ℕ) : MvPowerSeries σ R →ₗ[R] R := - LinearMap.proj n -#align mv_power_series.coeff MvPowerSeries.coeff - -variable {R} - -/-- Two multivariate formal power series are equal if all their coefficients are equal.-/ -@[ext] -theorem ext {φ ψ} (h : ∀ n : σ →₀ ℕ, coeff R n φ = coeff R n ψ) : φ = ψ := - funext h -#align mv_power_series.ext MvPowerSeries.ext - -/-- Two multivariate formal power series are equal - if and only if all their coefficients are equal.-/ -theorem ext_iff {φ ψ : MvPowerSeries σ R} : φ = ψ ↔ ∀ n : σ →₀ ℕ, coeff R n φ = coeff R n ψ := - Function.funext_iff -#align mv_power_series.ext_iff MvPowerSeries.ext_iff - -theorem monomial_def [DecidableEq σ] (n : σ →₀ ℕ) : - (monomial R n) = LinearMap.stdBasis R (fun _ ↦ R) n := by - rw [monomial] - -- unify the `Decidable` arguments - convert rfl -#align mv_power_series.monomial_def MvPowerSeries.monomial_def - -theorem coeff_monomial [DecidableEq σ] (m n : σ →₀ ℕ) (a : R) : - coeff R m (monomial R n a) = if m = n then a else 0 := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [coeff, monomial_def, LinearMap.proj_apply (i := m)] - dsimp only - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [LinearMap.stdBasis_apply, Function.update_apply, Pi.zero_apply] -#align mv_power_series.coeff_monomial MvPowerSeries.coeff_monomial - -@[simp] -theorem coeff_monomial_same (n : σ →₀ ℕ) (a : R) : coeff R n (monomial R n a) = a := by - classical - rw [monomial_def] - exact LinearMap.stdBasis_same R (fun _ ↦ R) n a -#align mv_power_series.coeff_monomial_same MvPowerSeries.coeff_monomial_same - -theorem coeff_monomial_ne {m n : σ →₀ ℕ} (h : m ≠ n) (a : R) : coeff R m (monomial R n a) = 0 := by - classical - rw [monomial_def] - exact LinearMap.stdBasis_ne R (fun _ ↦ R) _ _ h a -#align mv_power_series.coeff_monomial_ne MvPowerSeries.coeff_monomial_ne - -theorem eq_of_coeff_monomial_ne_zero {m n : σ →₀ ℕ} {a : R} (h : coeff R m (monomial R n a) ≠ 0) : - m = n := - by_contra fun h' => h <| coeff_monomial_ne h' a -#align mv_power_series.eq_of_coeff_monomial_ne_zero MvPowerSeries.eq_of_coeff_monomial_ne_zero - -@[simp] -theorem coeff_comp_monomial (n : σ →₀ ℕ) : (coeff R n).comp (monomial R n) = LinearMap.id := - LinearMap.ext <| coeff_monomial_same n -#align mv_power_series.coeff_comp_monomial MvPowerSeries.coeff_comp_monomial - --- Porting note (#10618): simp can prove this. --- @[simp] -theorem coeff_zero (n : σ →₀ ℕ) : coeff R n (0 : MvPowerSeries σ R) = 0 := - rfl -#align mv_power_series.coeff_zero MvPowerSeries.coeff_zero - -variable (m n : σ →₀ ℕ) (φ ψ : MvPowerSeries σ R) - -instance : One (MvPowerSeries σ R) := - ⟨monomial R (0 : σ →₀ ℕ) 1⟩ - -theorem coeff_one [DecidableEq σ] : coeff R n (1 : MvPowerSeries σ R) = if n = 0 then 1 else 0 := - coeff_monomial _ _ _ -#align mv_power_series.coeff_one MvPowerSeries.coeff_one - -theorem coeff_zero_one : coeff R (0 : σ →₀ ℕ) 1 = 1 := - coeff_monomial_same 0 1 -#align mv_power_series.coeff_zero_one MvPowerSeries.coeff_zero_one - -theorem monomial_zero_one : monomial R (0 : σ →₀ ℕ) 1 = 1 := - rfl -#align mv_power_series.monomial_zero_one MvPowerSeries.monomial_zero_one - -instance : AddMonoidWithOne (MvPowerSeries σ R) := - { show AddMonoid (MvPowerSeries σ R) by infer_instance with - natCast := fun n => monomial R 0 n - natCast_zero := by simp [Nat.cast] - natCast_succ := by simp [Nat.cast, monomial_zero_one] - one := 1 } - -instance : Mul (MvPowerSeries σ R) := - letI := Classical.decEq σ - ⟨fun φ ψ n => ∑ p in antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ⟩ - -theorem coeff_mul [DecidableEq σ] : - coeff R n (φ * ψ) = ∑ p in antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ := by - refine Finset.sum_congr ?_ fun _ _ => rfl - rw [Subsingleton.elim (Classical.decEq σ) ‹DecidableEq σ›] -#align mv_power_series.coeff_mul MvPowerSeries.coeff_mul - -protected theorem zero_mul : (0 : MvPowerSeries σ R) * φ = 0 := - ext fun n => by classical simp [coeff_mul] -#align mv_power_series.zero_mul MvPowerSeries.zero_mul - -protected theorem mul_zero : φ * 0 = 0 := - ext fun n => by classical simp [coeff_mul] -#align mv_power_series.mul_zero MvPowerSeries.mul_zero - -theorem coeff_monomial_mul (a : R) : - coeff R m (monomial R n a * φ) = if n ≤ m then a * coeff R (m - n) φ else 0 := by - classical - have : - ∀ p ∈ antidiagonal m, - coeff R (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial R n a) * coeff R p.2 φ ≠ 0 → p.1 = n := - fun p _ hp => eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp) - rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_fst_eq_antidiagonal _ n, - Finset.sum_ite_index] - simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty] -#align mv_power_series.coeff_monomial_mul MvPowerSeries.coeff_monomial_mul - -theorem coeff_mul_monomial (a : R) : - coeff R m (φ * monomial R n a) = if n ≤ m then coeff R (m - n) φ * a else 0 := by - classical - have : - ∀ p ∈ antidiagonal m, - coeff R (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 φ * coeff R p.2 (monomial R n a) ≠ 0 → p.2 = n := - fun p _ hp => eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hp) - rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_snd_eq_antidiagonal _ n, - Finset.sum_ite_index] - simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty] -#align mv_power_series.coeff_mul_monomial MvPowerSeries.coeff_mul_monomial - -theorem coeff_add_monomial_mul (a : R) : - coeff R (m + n) (monomial R m a * φ) = a * coeff R n φ := by - rw [coeff_monomial_mul, if_pos, add_tsub_cancel_left] - exact le_add_right le_rfl -#align mv_power_series.coeff_add_monomial_mul MvPowerSeries.coeff_add_monomial_mul - -theorem coeff_add_mul_monomial (a : R) : - coeff R (m + n) (φ * monomial R n a) = coeff R m φ * a := by - rw [coeff_mul_monomial, if_pos, add_tsub_cancel_right] - exact le_add_left le_rfl -#align mv_power_series.coeff_add_mul_monomial MvPowerSeries.coeff_add_mul_monomial - -@[simp] -theorem commute_monomial {a : R} {n} : - Commute φ (monomial R n a) ↔ ∀ m, Commute (coeff R m φ) a := by - refine' ext_iff.trans ⟨fun h m => _, fun h m => _⟩ - · have := h (m + n) - rwa [coeff_add_mul_monomial, add_comm, coeff_add_monomial_mul] at this - · rw [coeff_mul_monomial, coeff_monomial_mul] - split_ifs <;> [apply h; rfl] -#align mv_power_series.commute_monomial MvPowerSeries.commute_monomial - -protected theorem one_mul : (1 : MvPowerSeries σ R) * φ = φ := - ext fun n => by simpa using coeff_add_monomial_mul 0 n φ 1 -#align mv_power_series.one_mul MvPowerSeries.one_mul - -protected theorem mul_one : φ * 1 = φ := - ext fun n => by simpa using coeff_add_mul_monomial n 0 φ 1 -#align mv_power_series.mul_one MvPowerSeries.mul_one - -protected theorem mul_add (φ₁ φ₂ φ₃ : MvPowerSeries σ R) : φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃ := - ext fun n => by - classical simp only [coeff_mul, mul_add, Finset.sum_add_distrib, LinearMap.map_add] -#align mv_power_series.mul_add MvPowerSeries.mul_add - -protected theorem add_mul (φ₁ φ₂ φ₃ : MvPowerSeries σ R) : (φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃ := - ext fun n => by - classical simp only [coeff_mul, add_mul, Finset.sum_add_distrib, LinearMap.map_add] -#align mv_power_series.add_mul MvPowerSeries.add_mul - -protected theorem mul_assoc (φ₁ φ₂ φ₃ : MvPowerSeries σ R) : φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃) := by - ext1 n - classical - simp only [coeff_mul, Finset.sum_mul, Finset.mul_sum, Finset.sum_sigma'] - apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩) - (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;> aesop (add simp [add_assoc, mul_assoc]) -#align mv_power_series.mul_assoc MvPowerSeries.mul_assoc - -instance : Semiring (MvPowerSeries σ R) := - { inferInstanceAs (AddMonoidWithOne (MvPowerSeries σ R)), - inferInstanceAs (Mul (MvPowerSeries σ R)), - inferInstanceAs (AddCommMonoid (MvPowerSeries σ R)) with - mul_one := MvPowerSeries.mul_one - one_mul := MvPowerSeries.one_mul - mul_assoc := MvPowerSeries.mul_assoc - mul_zero := MvPowerSeries.mul_zero - zero_mul := MvPowerSeries.zero_mul - left_distrib := MvPowerSeries.mul_add - right_distrib := MvPowerSeries.add_mul } - -end Semiring - -instance [CommSemiring R] : CommSemiring (MvPowerSeries σ R) := - { show Semiring (MvPowerSeries σ R) by infer_instance with - mul_comm := fun φ ψ => - ext fun n => by - classical - simpa only [coeff_mul, mul_comm] using - sum_antidiagonal_swap n fun a b => coeff R a φ * coeff R b ψ } - -instance [Ring R] : Ring (MvPowerSeries σ R) := - { inferInstanceAs (Semiring (MvPowerSeries σ R)), - inferInstanceAs (AddCommGroup (MvPowerSeries σ R)) with } - -instance [CommRing R] : CommRing (MvPowerSeries σ R) := - { inferInstanceAs (CommSemiring (MvPowerSeries σ R)), - inferInstanceAs (AddCommGroup (MvPowerSeries σ R)) with } - -section Semiring - -variable [Semiring R] - -theorem monomial_mul_monomial (m n : σ →₀ ℕ) (a b : R) : - monomial R m a * monomial R n b = monomial R (m + n) (a * b) := by - classical - ext k - simp only [coeff_mul_monomial, coeff_monomial] - split_ifs with h₁ h₂ h₃ h₃ h₂ <;> try rfl - · rw [← h₂, tsub_add_cancel_of_le h₁] at h₃ - exact (h₃ rfl).elim - · rw [h₃, add_tsub_cancel_right] at h₂ - exact (h₂ rfl).elim - · exact zero_mul b - · rw [h₂] at h₁ - exact (h₁ <| le_add_left le_rfl).elim -#align mv_power_series.monomial_mul_monomial MvPowerSeries.monomial_mul_monomial - -variable (σ) (R) - -/-- The constant multivariate formal power series.-/ -def C : R →+* MvPowerSeries σ R := - { monomial R (0 : σ →₀ ℕ) with - map_one' := rfl - map_mul' := fun a b => (monomial_mul_monomial 0 0 a b).symm - map_zero' := (monomial R (0 : _)).map_zero } -set_option linter.uppercaseLean3 false in -#align mv_power_series.C MvPowerSeries.C - -variable {σ} {R} - -@[simp] -theorem monomial_zero_eq_C : ⇑(monomial R (0 : σ →₀ ℕ)) = C σ R := - rfl -set_option linter.uppercaseLean3 false in -#align mv_power_series.monomial_zero_eq_C MvPowerSeries.monomial_zero_eq_C - -theorem monomial_zero_eq_C_apply (a : R) : monomial R (0 : σ →₀ ℕ) a = C σ R a := - rfl -set_option linter.uppercaseLean3 false in -#align mv_power_series.monomial_zero_eq_C_apply MvPowerSeries.monomial_zero_eq_C_apply - -theorem coeff_C [DecidableEq σ] (n : σ →₀ ℕ) (a : R) : - coeff R n (C σ R a) = if n = 0 then a else 0 := - coeff_monomial _ _ _ -set_option linter.uppercaseLean3 false in -#align mv_power_series.coeff_C MvPowerSeries.coeff_C - -theorem coeff_zero_C (a : R) : coeff R (0 : σ →₀ ℕ) (C σ R a) = a := - coeff_monomial_same 0 a -set_option linter.uppercaseLean3 false in -#align mv_power_series.coeff_zero_C MvPowerSeries.coeff_zero_C - -/-- The variables of the multivariate formal power series ring.-/ -def X (s : σ) : MvPowerSeries σ R := - monomial R (single s 1) 1 -set_option linter.uppercaseLean3 false in -#align mv_power_series.X MvPowerSeries.X - -theorem coeff_X [DecidableEq σ] (n : σ →₀ ℕ) (s : σ) : - coeff R n (X s : MvPowerSeries σ R) = if n = single s 1 then 1 else 0 := - coeff_monomial _ _ _ -set_option linter.uppercaseLean3 false in -#align mv_power_series.coeff_X MvPowerSeries.coeff_X - -theorem coeff_index_single_X [DecidableEq σ] (s t : σ) : - coeff R (single t 1) (X s : MvPowerSeries σ R) = if t = s then 1 else 0 := by - simp only [coeff_X, single_left_inj (one_ne_zero : (1 : ℕ) ≠ 0)] -set_option linter.uppercaseLean3 false in -#align mv_power_series.coeff_index_single_X MvPowerSeries.coeff_index_single_X - -@[simp] -theorem coeff_index_single_self_X (s : σ) : coeff R (single s 1) (X s : MvPowerSeries σ R) = 1 := - coeff_monomial_same _ _ -set_option linter.uppercaseLean3 false in -#align mv_power_series.coeff_index_single_self_X MvPowerSeries.coeff_index_single_self_X - -theorem coeff_zero_X (s : σ) : coeff R (0 : σ →₀ ℕ) (X s : MvPowerSeries σ R) = 0 := by - classical - rw [coeff_X, if_neg] - intro h - exact one_ne_zero (single_eq_zero.mp h.symm) -set_option linter.uppercaseLean3 false in -#align mv_power_series.coeff_zero_X MvPowerSeries.coeff_zero_X - -theorem commute_X (φ : MvPowerSeries σ R) (s : σ) : Commute φ (X s) := - φ.commute_monomial.mpr fun _m => Commute.one_right _ -set_option linter.uppercaseLean3 false in -#align mv_power_series.commute_X MvPowerSeries.commute_X - -theorem X_def (s : σ) : X s = monomial R (single s 1) 1 := - rfl -set_option linter.uppercaseLean3 false in -#align mv_power_series.X_def MvPowerSeries.X_def - -theorem X_pow_eq (s : σ) (n : ℕ) : (X s : MvPowerSeries σ R) ^ n = monomial R (single s n) 1 := by - induction' n with n ih - · simp - · rw [pow_succ', ih, Nat.succ_eq_add_one, Finsupp.single_add, X, monomial_mul_monomial, one_mul] -set_option linter.uppercaseLean3 false in -#align mv_power_series.X_pow_eq MvPowerSeries.X_pow_eq - -theorem coeff_X_pow [DecidableEq σ] (m : σ →₀ ℕ) (s : σ) (n : ℕ) : - coeff R m ((X s : MvPowerSeries σ R) ^ n) = if m = single s n then 1 else 0 := by - rw [X_pow_eq s n, coeff_monomial] -set_option linter.uppercaseLean3 false in -#align mv_power_series.coeff_X_pow MvPowerSeries.coeff_X_pow - -@[simp] -theorem coeff_mul_C (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) : - coeff R n (φ * C σ R a) = coeff R n φ * a := by simpa using coeff_add_mul_monomial n 0 φ a -set_option linter.uppercaseLean3 false in -#align mv_power_series.coeff_mul_C MvPowerSeries.coeff_mul_C - -@[simp] -theorem coeff_C_mul (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) : - coeff R n (C σ R a * φ) = a * coeff R n φ := by simpa using coeff_add_monomial_mul 0 n φ a -set_option linter.uppercaseLean3 false in -#align mv_power_series.coeff_C_mul MvPowerSeries.coeff_C_mul - -theorem coeff_zero_mul_X (φ : MvPowerSeries σ R) (s : σ) : coeff R (0 : σ →₀ ℕ) (φ * X s) = 0 := by - have : ¬single s 1 ≤ 0 := fun h => by simpa using h s - simp only [X, coeff_mul_monomial, if_neg this] -set_option linter.uppercaseLean3 false in -#align mv_power_series.coeff_zero_mul_X MvPowerSeries.coeff_zero_mul_X - -theorem coeff_zero_X_mul (φ : MvPowerSeries σ R) (s : σ) : coeff R (0 : σ →₀ ℕ) (X s * φ) = 0 := by - rw [← (φ.commute_X s).eq, coeff_zero_mul_X] -set_option linter.uppercaseLean3 false in -#align mv_power_series.coeff_zero_X_mul MvPowerSeries.coeff_zero_X_mul - -variable (σ) (R) - -/-- The constant coefficient of a formal power series.-/ -def constantCoeff : MvPowerSeries σ R →+* R := - { coeff R (0 : σ →₀ ℕ) with - toFun := coeff R (0 : σ →₀ ℕ) - map_one' := coeff_zero_one - map_mul' := fun φ ψ => by classical simp [coeff_mul, support_single_ne_zero] - map_zero' := LinearMap.map_zero _ } -#align mv_power_series.constant_coeff MvPowerSeries.constantCoeff - -variable {σ} {R} - -@[simp] -theorem coeff_zero_eq_constantCoeff : ⇑(coeff R (0 : σ →₀ ℕ)) = constantCoeff σ R := - rfl -#align mv_power_series.coeff_zero_eq_constant_coeff MvPowerSeries.coeff_zero_eq_constantCoeff - -theorem coeff_zero_eq_constantCoeff_apply (φ : MvPowerSeries σ R) : - coeff R (0 : σ →₀ ℕ) φ = constantCoeff σ R φ := - rfl -#align mv_power_series.coeff_zero_eq_constant_coeff_apply MvPowerSeries.coeff_zero_eq_constantCoeff_apply - -@[simp] -theorem constantCoeff_C (a : R) : constantCoeff σ R (C σ R a) = a := - rfl -set_option linter.uppercaseLean3 false in -#align mv_power_series.constant_coeff_C MvPowerSeries.constantCoeff_C - -@[simp] -theorem constantCoeff_comp_C : (constantCoeff σ R).comp (C σ R) = RingHom.id R := - rfl -set_option linter.uppercaseLean3 false in -#align mv_power_series.constant_coeff_comp_C MvPowerSeries.constantCoeff_comp_C - --- Porting note (#10618): simp can prove this. --- @[simp] -theorem constantCoeff_zero : constantCoeff σ R 0 = 0 := - rfl -#align mv_power_series.constant_coeff_zero MvPowerSeries.constantCoeff_zero - --- Porting note (#10618): simp can prove this. --- @[simp] -theorem constantCoeff_one : constantCoeff σ R 1 = 1 := - rfl -#align mv_power_series.constant_coeff_one MvPowerSeries.constantCoeff_one - -@[simp] -theorem constantCoeff_X (s : σ) : constantCoeff σ R (X s) = 0 := - coeff_zero_X s -set_option linter.uppercaseLean3 false in -#align mv_power_series.constant_coeff_X MvPowerSeries.constantCoeff_X - -/-- If a multivariate formal power series is invertible, - then so is its constant coefficient.-/ -theorem isUnit_constantCoeff (φ : MvPowerSeries σ R) (h : IsUnit φ) : - IsUnit (constantCoeff σ R φ) := - h.map _ -#align mv_power_series.is_unit_constant_coeff MvPowerSeries.isUnit_constantCoeff - --- Porting note (#10618): simp can prove this. --- @[simp] -theorem coeff_smul (f : MvPowerSeries σ R) (n) (a : R) : coeff _ n (a • f) = a * coeff _ n f := - rfl -#align mv_power_series.coeff_smul MvPowerSeries.coeff_smul - -theorem smul_eq_C_mul (f : MvPowerSeries σ R) (a : R) : a • f = C σ R a * f := by - ext - simp -set_option linter.uppercaseLean3 false in -#align mv_power_series.smul_eq_C_mul MvPowerSeries.smul_eq_C_mul - -theorem X_inj [Nontrivial R] {s t : σ} : (X s : MvPowerSeries σ R) = X t ↔ s = t := - ⟨by - classical - intro h - replace h := congr_arg (coeff R (single s 1)) h - rw [coeff_X, if_pos rfl, coeff_X] at h - split_ifs at h with H - · rw [Finsupp.single_eq_single_iff] at H - cases' H with H H - · exact H.1 - · exfalso - exact one_ne_zero H.1 - · exfalso - exact one_ne_zero h, congr_arg X⟩ -set_option linter.uppercaseLean3 false in -#align mv_power_series.X_inj MvPowerSeries.X_inj - -end Semiring - -section Map - -variable {S T : Type*} [Semiring R] [Semiring S] [Semiring T] - -variable (f : R →+* S) (g : S →+* T) - -variable (σ) - -/-- The map between multivariate formal power series induced by a map on the coefficients.-/ -def map : MvPowerSeries σ R →+* MvPowerSeries σ S where - toFun φ n := f <| coeff R n φ - map_zero' := ext fun _n => f.map_zero - map_one' := - ext fun n => - show f ((coeff R n) 1) = (coeff S n) 1 by - classical - rw [coeff_one, coeff_one] - split_ifs with h - · simp only [RingHom.map_ite_one_zero, ite_true, map_one, h] - · simp only [RingHom.map_ite_one_zero, ite_false, map_zero, h] - map_add' φ ψ := - ext fun n => show f ((coeff R n) (φ + ψ)) = f ((coeff R n) φ) + f ((coeff R n) ψ) by simp - map_mul' φ ψ := - ext fun n => - show f _ = _ by - classical - rw [coeff_mul, map_sum, coeff_mul] - apply Finset.sum_congr rfl - rintro ⟨i, j⟩ _; rw [f.map_mul]; rfl -#align mv_power_series.map MvPowerSeries.map - -variable {σ} - -@[simp] -theorem map_id : map σ (RingHom.id R) = RingHom.id _ := - rfl -#align mv_power_series.map_id MvPowerSeries.map_id - -theorem map_comp : map σ (g.comp f) = (map σ g).comp (map σ f) := - rfl -#align mv_power_series.map_comp MvPowerSeries.map_comp - -@[simp] -theorem coeff_map (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) : coeff S n (map σ f φ) = f (coeff R n φ) := - rfl -#align mv_power_series.coeff_map MvPowerSeries.coeff_map - -@[simp] -theorem constantCoeff_map (φ : MvPowerSeries σ R) : - constantCoeff σ S (map σ f φ) = f (constantCoeff σ R φ) := - rfl -#align mv_power_series.constant_coeff_map MvPowerSeries.constantCoeff_map - -@[simp] -theorem map_monomial (n : σ →₀ ℕ) (a : R) : map σ f (monomial R n a) = monomial S n (f a) := by - classical - ext m - simp [coeff_monomial, apply_ite f] -#align mv_power_series.map_monomial MvPowerSeries.map_monomial - -@[simp] -theorem map_C (a : R) : map σ f (C σ R a) = C σ S (f a) := - map_monomial _ _ _ -set_option linter.uppercaseLean3 false in -#align mv_power_series.map_C MvPowerSeries.map_C - -@[simp] -theorem map_X (s : σ) : map σ f (X s) = X s := by simp [MvPowerSeries.X] -set_option linter.uppercaseLean3 false in -#align mv_power_series.map_X MvPowerSeries.map_X - -end Map - -section Algebra - -variable {A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] - -instance : Algebra R (MvPowerSeries σ A) := - { - show Module R (MvPowerSeries σ A) by infer_instance with - commutes' := fun a φ => by - ext n - simp [Algebra.commutes] - smul_def' := fun a σ => by - ext n - simp [(coeff A n).map_smul_of_tower a, Algebra.smul_def] - toRingHom := (MvPowerSeries.map σ (algebraMap R A)).comp (C σ R) } - -theorem c_eq_algebraMap : C σ R = algebraMap R (MvPowerSeries σ R) := - rfl -set_option linter.uppercaseLean3 false in -#align mv_power_series.C_eq_algebra_map MvPowerSeries.c_eq_algebraMap - -theorem algebraMap_apply {r : R} : - algebraMap R (MvPowerSeries σ A) r = C σ A (algebraMap R A r) := by - change (MvPowerSeries.map σ (algebraMap R A)).comp (C σ R) r = _ - simp -#align mv_power_series.algebra_map_apply MvPowerSeries.algebraMap_apply - -instance [Nonempty σ] [Nontrivial R] : Nontrivial (Subalgebra R (MvPowerSeries σ R)) := - ⟨⟨⊥, ⊤, by - classical - rw [Ne.def, SetLike.ext_iff, not_forall] - inhabit σ - refine' ⟨X default, _⟩ - simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true_iff, Algebra.mem_top] - intro x - rw [ext_iff, not_forall] - refine' ⟨Finsupp.single default 1, _⟩ - simp [algebraMap_apply, coeff_C]⟩⟩ - -end Algebra - -section Trunc - -variable [CommSemiring R] (n : σ →₀ ℕ) - -/-- Auxiliary definition for the truncation function. -/ -def truncFun (φ : MvPowerSeries σ R) : MvPolynomial σ R := - ∑ m in Finset.Iio n, MvPolynomial.monomial m (coeff R m φ) -#align mv_power_series.trunc_fun MvPowerSeries.truncFun - -theorem coeff_truncFun (m : σ →₀ ℕ) (φ : MvPowerSeries σ R) : - (truncFun n φ).coeff m = if m < n then coeff R m φ else 0 := by - classical - simp [truncFun, MvPolynomial.coeff_sum] -#align mv_power_series.coeff_trunc_fun MvPowerSeries.coeff_truncFun - -variable (R) - -/-- The `n`th truncation of a multivariate formal power series to a multivariate polynomial -/ -def trunc : MvPowerSeries σ R →+ MvPolynomial σ R where - toFun := truncFun n - map_zero' := by - classical - ext - simp [coeff_truncFun] - map_add' := by - classical - intros x y - ext m - simp only [coeff_truncFun, MvPolynomial.coeff_add] - split_ifs - · rw [map_add] - · rw [zero_add] - -#align mv_power_series.trunc MvPowerSeries.trunc - -variable {R} - -theorem coeff_trunc (m : σ →₀ ℕ) (φ : MvPowerSeries σ R) : - (trunc R n φ).coeff m = if m < n then coeff R m φ else 0 := by - classical simp [trunc, coeff_truncFun] -#align mv_power_series.coeff_trunc MvPowerSeries.coeff_trunc - -@[simp] -theorem trunc_one (n : σ →₀ ℕ) (hnn : n ≠ 0) : trunc R n 1 = 1 := - MvPolynomial.ext _ _ fun m => by - classical - rw [coeff_trunc, coeff_one] - split_ifs with H H' - · subst m - simp - · symm - rw [MvPolynomial.coeff_one] - exact if_neg (Ne.symm H') - · symm - rw [MvPolynomial.coeff_one] - refine' if_neg _ - rintro rfl - apply H - exact Ne.bot_lt hnn -#align mv_power_series.trunc_one MvPowerSeries.trunc_one - -@[simp] -theorem trunc_c (n : σ →₀ ℕ) (hnn : n ≠ 0) (a : R) : trunc R n (C σ R a) = MvPolynomial.C a := - MvPolynomial.ext _ _ fun m => by - classical - rw [coeff_trunc, coeff_C, MvPolynomial.coeff_C] - split_ifs with H <;> first |rfl|try simp_all - exfalso; apply H; subst m; exact Ne.bot_lt hnn -set_option linter.uppercaseLean3 false in -#align mv_power_series.trunc_C MvPowerSeries.trunc_c - -end Trunc - -section Semiring - -variable [Semiring R] - -theorem X_pow_dvd_iff {s : σ} {n : ℕ} {φ : MvPowerSeries σ R} : - (X s : MvPowerSeries σ R) ^ n ∣ φ ↔ ∀ m : σ →₀ ℕ, m s < n → coeff R m φ = 0 := by - classical - constructor - · rintro ⟨φ, rfl⟩ m h - rw [coeff_mul, Finset.sum_eq_zero] - rintro ⟨i, j⟩ hij - rw [coeff_X_pow, if_neg, zero_mul] - contrapose! h - dsimp at h - subst i - rw [mem_antidiagonal] at hij - rw [← hij, Finsupp.add_apply, Finsupp.single_eq_same] - exact Nat.le_add_right n _ - · intro h - refine' ⟨fun m => coeff R (m + single s n) φ, _⟩ - ext m - by_cases H : m - single s n + single s n = m - · rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)] - · rw [coeff_X_pow, if_pos rfl, one_mul] - simpa using congr_arg (fun m : σ →₀ ℕ => coeff R m φ) H.symm - · rintro ⟨i, j⟩ hij hne - rw [mem_antidiagonal] at hij - rw [coeff_X_pow] - split_ifs with hi - · exfalso - apply hne - rw [← hij, ← hi, Prod.mk.inj_iff] - refine' ⟨rfl, _⟩ - ext t - simp only [add_tsub_cancel_left, Finsupp.add_apply, Finsupp.tsub_apply] - · exact zero_mul _ - · intro hni - exfalso - apply hni - rwa [mem_antidiagonal, add_comm] - · rw [h, coeff_mul, Finset.sum_eq_zero] - · rintro ⟨i, j⟩ hij - rw [mem_antidiagonal] at hij - rw [coeff_X_pow] - split_ifs with hi - · exfalso - apply H - rw [← hij, hi] - ext - rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm] - · exact zero_mul _ - · contrapose! H - ext t - by_cases hst : s = t - · subst t - simpa using tsub_add_cancel_of_le H - · simp [Finsupp.single_apply, hst] -set_option linter.uppercaseLean3 false in -#align mv_power_series.X_pow_dvd_iff MvPowerSeries.X_pow_dvd_iff - -theorem X_dvd_iff {s : σ} {φ : MvPowerSeries σ R} : - (X s : MvPowerSeries σ R) ∣ φ ↔ ∀ m : σ →₀ ℕ, m s = 0 → coeff R m φ = 0 := by - rw [← pow_one (X s : MvPowerSeries σ R), X_pow_dvd_iff] - constructor <;> intro h m hm - · exact h m (hm.symm ▸ zero_lt_one) - · exact h m (Nat.eq_zero_of_le_zero <| Nat.le_of_succ_le_succ hm) -set_option linter.uppercaseLean3 false in -#align mv_power_series.X_dvd_iff MvPowerSeries.X_dvd_iff - -end Semiring - -section CommSemiring - -open Finset.HasAntidiagonal Finset - -variable {R : Type*} [CommSemiring R] {ι : Type*} [DecidableEq ι] - -/-- Coefficients of a product of power series -/ -theorem coeff_prod [DecidableEq σ] - (f : ι → MvPowerSeries σ R) (d : σ →₀ ℕ) (s : Finset ι) : - coeff R d (∏ j in s, f j) = - ∑ l in piAntidiagonal s d, - ∏ i in s, coeff R (l i) (f i) := by - induction s using Finset.induction_on generalizing d with - | empty => - simp only [prod_empty, sum_const, nsmul_eq_mul, mul_one, coeff_one, piAntidiagonal_empty] - split_ifs - · simp only [card_singleton, Nat.cast_one] - · simp only [card_empty, Nat.cast_zero] - | @insert a s ha ih => - rw [piAntidiagonal_insert ha, prod_insert ha, coeff_mul, sum_biUnion] - · apply Finset.sum_congr rfl - · simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall] - rintro u v rfl - rw [ih, Finset.mul_sum, ← Finset.sum_attach] - apply Finset.sum_congr rfl - simp only [mem_attach, Finset.prod_insert ha, Function.update_same, forall_true_left, - Subtype.forall] - rintro x - - rw [Finset.prod_congr rfl] - intro i hi - rw [Function.update_noteq] - exact ne_of_mem_of_not_mem hi ha - · simp only [Set.PairwiseDisjoint, Set.Pairwise, mem_coe, mem_antidiagonal, ne_eq, - disjoint_left, mem_map, mem_attach, Function.Embedding.coeFn_mk, true_and, Subtype.exists, - exists_prop, not_exists, not_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, - Prod.forall, Prod.mk.injEq] - rintro u v rfl u' v' huv h k - l - hkl - obtain rfl : u' = u := by - simpa only [Finsupp.coe_update, Function.update_same] using DFunLike.congr_fun hkl a - simp only [add_right_inj] at huv - exact h rfl huv.symm - -end CommSemiring - -section Ring - -variable [Ring R] - -/- -The inverse of a multivariate formal power series is defined by -well-founded recursion on the coefficients of the inverse. --/ -/-- Auxiliary definition that unifies - the totalised inverse formal power series `(_)⁻¹` and - the inverse formal power series that depends on - an inverse of the constant coefficient `invOfUnit`.-/ -protected noncomputable def inv.aux (a : R) (φ : MvPowerSeries σ R) : MvPowerSeries σ R - | n => - letI := Classical.decEq σ - if n = 0 then a - else - -a * - ∑ x in antidiagonal n, if _ : x.2 < n then coeff R x.1 φ * inv.aux a φ x.2 else 0 -termination_by n => n -#align mv_power_series.inv.aux MvPowerSeries.inv.aux - -theorem coeff_inv_aux [DecidableEq σ] (n : σ →₀ ℕ) (a : R) (φ : MvPowerSeries σ R) : - coeff R n (inv.aux a φ) = - if n = 0 then a - else - -a * - ∑ x in antidiagonal n, if x.2 < n then coeff R x.1 φ * coeff R x.2 (inv.aux a φ) else 0 := - show inv.aux a φ n = _ by - cases Subsingleton.elim ‹DecidableEq σ› (Classical.decEq σ) - rw [inv.aux] - rfl -#align mv_power_series.coeff_inv_aux MvPowerSeries.coeff_inv_aux - -/-- A multivariate formal power series is invertible if the constant coefficient is invertible.-/ -def invOfUnit (φ : MvPowerSeries σ R) (u : Rˣ) : MvPowerSeries σ R := - inv.aux (↑u⁻¹) φ -#align mv_power_series.inv_of_unit MvPowerSeries.invOfUnit - -theorem coeff_invOfUnit [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (u : Rˣ) : - coeff R n (invOfUnit φ u) = - if n = 0 then ↑u⁻¹ - else - -↑u⁻¹ * - ∑ x in antidiagonal n, - if x.2 < n then coeff R x.1 φ * coeff R x.2 (invOfUnit φ u) else 0 := by - convert coeff_inv_aux n (↑u⁻¹) φ -#align mv_power_series.coeff_inv_of_unit MvPowerSeries.coeff_invOfUnit - -@[simp] -theorem constantCoeff_invOfUnit (φ : MvPowerSeries σ R) (u : Rˣ) : - constantCoeff σ R (invOfUnit φ u) = ↑u⁻¹ := by - classical - rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl] -#align mv_power_series.constant_coeff_inv_of_unit MvPowerSeries.constantCoeff_invOfUnit - -theorem mul_invOfUnit (φ : MvPowerSeries σ R) (u : Rˣ) (h : constantCoeff σ R φ = u) : - φ * invOfUnit φ u = 1 := - ext fun n => - letI := Classical.decEq (σ →₀ ℕ) - if H : n = 0 then by - rw [H] - simp [coeff_mul, support_single_ne_zero, h] - else by - classical - have : ((0 : σ →₀ ℕ), n) ∈ antidiagonal n := by rw [mem_antidiagonal, zero_add] - rw [coeff_one, if_neg H, coeff_mul, ← Finset.insert_erase this, - Finset.sum_insert (Finset.not_mem_erase _ _), coeff_zero_eq_constantCoeff_apply, h, - coeff_invOfUnit, if_neg H, neg_mul, mul_neg, Units.mul_inv_cancel_left, ← - Finset.insert_erase this, Finset.sum_insert (Finset.not_mem_erase _ _), - Finset.insert_erase this, if_neg (not_lt_of_ge <| le_rfl), zero_add, add_comm, ← - sub_eq_add_neg, sub_eq_zero, Finset.sum_congr rfl] - rintro ⟨i, j⟩ hij - rw [Finset.mem_erase, mem_antidiagonal] at hij - cases' hij with h₁ h₂ - subst n - rw [if_pos] - suffices (0 : _) + j < i + j by simpa - apply add_lt_add_right - constructor - · intro s - exact Nat.zero_le _ - · intro H - apply h₁ - suffices i = 0 by simp [this] - ext1 s - exact Nat.eq_zero_of_le_zero (H s) -#align mv_power_series.mul_inv_of_unit MvPowerSeries.mul_invOfUnit - -end Ring - -section CommRing - -variable [CommRing R] - -/-- Multivariate formal power series over a local ring form a local ring. -/ -instance [LocalRing R] : LocalRing (MvPowerSeries σ R) := - LocalRing.of_isUnit_or_isUnit_one_sub_self <| by - intro φ - rcases LocalRing.isUnit_or_isUnit_one_sub_self (constantCoeff σ R φ) with (⟨u, h⟩ | ⟨u, h⟩) <;> - [left; right] <;> - · refine' isUnit_of_mul_eq_one _ _ (mul_invOfUnit _ u _) - simpa using h.symm - --- TODO(jmc): once adic topology lands, show that this is complete -end CommRing +Formal power series in one variable are defined from multivariate +power series as `PowerSeries R := MvPowerSeries Unit R`. -section LocalRing +The file sets up the (semi)ring structure on univariate power series. -variable {S : Type*} [CommRing R] [CommRing S] (f : R →+* S) [IsLocalRingHom f] - --- Thanks to the linter for informing us that this instance does --- not actually need R and S to be local rings! -/-- The map `A[[X]] → B[[X]]` induced by a local ring hom `A → B` is local -/ -instance map.isLocalRingHom : IsLocalRingHom (map σ f) := - ⟨by - rintro φ ⟨ψ, h⟩ - replace h := congr_arg (constantCoeff σ S) h - rw [constantCoeff_map] at h - have : IsUnit (constantCoeff σ S ↑ψ) := isUnit_constantCoeff (↑ψ) ψ.isUnit - rw [h] at this - rcases isUnit_of_map_unit f _ this with ⟨c, hc⟩ - exact isUnit_of_mul_eq_one φ (invOfUnit φ c) (mul_invOfUnit φ c hc.symm)⟩ -#align mv_power_series.map.is_local_ring_hom MvPowerSeries.map.isLocalRingHom - -end LocalRing - -section Field - -variable {k : Type*} [Field k] - -/-- The inverse `1/f` of a multivariable power series `f` over a field -/ -protected def inv (φ : MvPowerSeries σ k) : MvPowerSeries σ k := - inv.aux (constantCoeff σ k φ)⁻¹ φ -#align mv_power_series.inv MvPowerSeries.inv - -instance : Inv (MvPowerSeries σ k) := - ⟨MvPowerSeries.inv⟩ - -theorem coeff_inv [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ k) : - coeff k n φ⁻¹ = - if n = 0 then (constantCoeff σ k φ)⁻¹ - else - -(constantCoeff σ k φ)⁻¹ * - ∑ x in antidiagonal n, if x.2 < n then coeff k x.1 φ * coeff k x.2 φ⁻¹ else 0 := - coeff_inv_aux n _ φ -#align mv_power_series.coeff_inv MvPowerSeries.coeff_inv - -@[simp] -theorem constantCoeff_inv (φ : MvPowerSeries σ k) : - constantCoeff σ k φ⁻¹ = (constantCoeff σ k φ)⁻¹ := by - classical - rw [← coeff_zero_eq_constantCoeff_apply, coeff_inv, if_pos rfl] -#align mv_power_series.constant_coeff_inv MvPowerSeries.constantCoeff_inv - -theorem inv_eq_zero {φ : MvPowerSeries σ k} : φ⁻¹ = 0 ↔ constantCoeff σ k φ = 0 := - ⟨fun h => by simpa using congr_arg (constantCoeff σ k) h, fun h => - ext fun n => by - classical - rw [coeff_inv] - split_ifs <;> - simp only [h, map_zero, zero_mul, inv_zero, neg_zero]⟩ -#align mv_power_series.inv_eq_zero MvPowerSeries.inv_eq_zero - -@[simp] -theorem zero_inv : (0 : MvPowerSeries σ k)⁻¹ = 0 := by - rw [inv_eq_zero, constantCoeff_zero] -#align mv_power_series.zero_inv MvPowerSeries.zero_inv - --- Porting note (#10618): simp can prove this. --- @[simp] -theorem invOfUnit_eq (φ : MvPowerSeries σ k) (h : constantCoeff σ k φ ≠ 0) : - invOfUnit φ (Units.mk0 _ h) = φ⁻¹ := - rfl -#align mv_power_series.inv_of_unit_eq MvPowerSeries.invOfUnit_eq - -@[simp] -theorem invOfUnit_eq' (φ : MvPowerSeries σ k) (u : Units k) (h : constantCoeff σ k φ = u) : - invOfUnit φ u = φ⁻¹ := by - rw [← invOfUnit_eq φ (h.symm ▸ u.ne_zero)] - apply congrArg (invOfUnit φ) - rw [Units.ext_iff] - exact h.symm -#align mv_power_series.inv_of_unit_eq' MvPowerSeries.invOfUnit_eq' - -@[simp] -protected theorem mul_inv_cancel (φ : MvPowerSeries σ k) (h : constantCoeff σ k φ ≠ 0) : - φ * φ⁻¹ = 1 := by rw [← invOfUnit_eq φ h, mul_invOfUnit φ (Units.mk0 _ h) rfl] -#align mv_power_series.mul_inv_cancel MvPowerSeries.mul_inv_cancel - -@[simp] -protected theorem inv_mul_cancel (φ : MvPowerSeries σ k) (h : constantCoeff σ k φ ≠ 0) : - φ⁻¹ * φ = 1 := by rw [mul_comm, φ.mul_inv_cancel h] -#align mv_power_series.inv_mul_cancel MvPowerSeries.inv_mul_cancel - -protected theorem eq_mul_inv_iff_mul_eq {φ₁ φ₂ φ₃ : MvPowerSeries σ k} - (h : constantCoeff σ k φ₃ ≠ 0) : φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂ := - ⟨fun k => by simp [k, mul_assoc, MvPowerSeries.inv_mul_cancel _ h], fun k => by - simp [← k, mul_assoc, MvPowerSeries.mul_inv_cancel _ h]⟩ -#align mv_power_series.eq_mul_inv_iff_mul_eq MvPowerSeries.eq_mul_inv_iff_mul_eq - -protected theorem eq_inv_iff_mul_eq_one {φ ψ : MvPowerSeries σ k} (h : constantCoeff σ k ψ ≠ 0) : - φ = ψ⁻¹ ↔ φ * ψ = 1 := by rw [← MvPowerSeries.eq_mul_inv_iff_mul_eq h, one_mul] -#align mv_power_series.eq_inv_iff_mul_eq_one MvPowerSeries.eq_inv_iff_mul_eq_one - -protected theorem inv_eq_iff_mul_eq_one {φ ψ : MvPowerSeries σ k} (h : constantCoeff σ k ψ ≠ 0) : - ψ⁻¹ = φ ↔ φ * ψ = 1 := by rw [eq_comm, MvPowerSeries.eq_inv_iff_mul_eq_one h] -#align mv_power_series.inv_eq_iff_mul_eq_one MvPowerSeries.inv_eq_iff_mul_eq_one - -@[simp] -protected theorem mul_inv_rev (φ ψ : MvPowerSeries σ k) : - (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹ := by - by_cases h : constantCoeff σ k (φ * ψ) = 0 - · rw [inv_eq_zero.mpr h] - simp only [map_mul, mul_eq_zero] at h - -- we don't have `NoZeroDivisors (MvPowerSeries σ k)` yet, - cases' h with h h <;> simp [inv_eq_zero.mpr h] - · rw [MvPowerSeries.inv_eq_iff_mul_eq_one h] - simp only [not_or, map_mul, mul_eq_zero] at h - rw [← mul_assoc, mul_assoc _⁻¹, MvPowerSeries.inv_mul_cancel _ h.left, mul_one, - MvPowerSeries.inv_mul_cancel _ h.right] -#align mv_power_series.mul_inv_rev MvPowerSeries.mul_inv_rev - -instance : InvOneClass (MvPowerSeries σ k) := - { inferInstanceAs (One (MvPowerSeries σ k)), - inferInstanceAs (Inv (MvPowerSeries σ k)) with - inv_one := by - rw [MvPowerSeries.inv_eq_iff_mul_eq_one, mul_one] - simp } - -@[simp] -theorem C_inv (r : k) : (C σ k r)⁻¹ = C σ k r⁻¹ := by - rcases eq_or_ne r 0 with (rfl | hr) - · simp - rw [MvPowerSeries.inv_eq_iff_mul_eq_one, ← map_mul, inv_mul_cancel hr, map_one] - simpa using hr -set_option linter.uppercaseLean3 false in -#align mv_power_series.C_inv MvPowerSeries.C_inv - -@[simp] -theorem X_inv (s : σ) : (X s : MvPowerSeries σ k)⁻¹ = 0 := by - rw [inv_eq_zero, constantCoeff_X] -set_option linter.uppercaseLean3 false in -#align mv_power_series.X_inv MvPowerSeries.X_inv - -@[simp] -theorem smul_inv (r : k) (φ : MvPowerSeries σ k) : (r • φ)⁻¹ = r⁻¹ • φ⁻¹ := by - simp [smul_eq_C_mul, mul_comm] -#align mv_power_series.smul_inv MvPowerSeries.smul_inv - -end Field - -end MvPowerSeries - -namespace MvPolynomial - -open Finsupp - -variable {σ : Type*} {R : Type*} [CommSemiring R] (φ ψ : MvPolynomial σ R) - --- Porting note: added so we can add the `@[coe]` attribute -/-- The natural inclusion from multivariate polynomials into multivariate formal power series.-/ -@[coe] -def toMvPowerSeries : MvPolynomial σ R → MvPowerSeries σ R := - fun φ n => coeff n φ - -/-- The natural inclusion from multivariate polynomials into multivariate formal power series.-/ -instance coeToMvPowerSeries : Coe (MvPolynomial σ R) (MvPowerSeries σ R) := - ⟨toMvPowerSeries⟩ -#align mv_polynomial.coe_to_mv_power_series MvPolynomial.coeToMvPowerSeries - -theorem coe_def : (φ : MvPowerSeries σ R) = fun n => coeff n φ := - rfl -#align mv_polynomial.coe_def MvPolynomial.coe_def - -@[simp, norm_cast] -theorem coeff_coe (n : σ →₀ ℕ) : MvPowerSeries.coeff R n ↑φ = coeff n φ := - rfl -#align mv_polynomial.coeff_coe MvPolynomial.coeff_coe - -@[simp, norm_cast] -theorem coe_monomial (n : σ →₀ ℕ) (a : R) : - (monomial n a : MvPowerSeries σ R) = MvPowerSeries.monomial R n a := - MvPowerSeries.ext fun m => by - classical - rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial] - split_ifs with h₁ h₂ <;> first |rfl|subst m; contradiction -#align mv_polynomial.coe_monomial MvPolynomial.coe_monomial - -@[simp, norm_cast] -theorem coe_zero : ((0 : MvPolynomial σ R) : MvPowerSeries σ R) = 0 := - rfl -#align mv_polynomial.coe_zero MvPolynomial.coe_zero - -@[simp, norm_cast] -theorem coe_one : ((1 : MvPolynomial σ R) : MvPowerSeries σ R) = 1 := - coe_monomial _ _ -#align mv_polynomial.coe_one MvPolynomial.coe_one - -@[simp, norm_cast] -theorem coe_add : ((φ + ψ : MvPolynomial σ R) : MvPowerSeries σ R) = φ + ψ := - rfl -#align mv_polynomial.coe_add MvPolynomial.coe_add - -@[simp, norm_cast] -theorem coe_mul : ((φ * ψ : MvPolynomial σ R) : MvPowerSeries σ R) = φ * ψ := - MvPowerSeries.ext fun n => by - classical - simp only [coeff_coe, MvPowerSeries.coeff_mul, coeff_mul] -#align mv_polynomial.coe_mul MvPolynomial.coe_mul - -@[simp, norm_cast] -theorem coe_C (a : R) : ((C a : MvPolynomial σ R) : MvPowerSeries σ R) = MvPowerSeries.C σ R a := - coe_monomial _ _ -set_option linter.uppercaseLean3 false in -#align mv_polynomial.coe_C MvPolynomial.coe_C - -set_option linter.deprecated false in -@[simp, norm_cast] -theorem coe_bit0 : - ((bit0 φ : MvPolynomial σ R) : MvPowerSeries σ R) = bit0 (φ : MvPowerSeries σ R) := - coe_add _ _ -#align mv_polynomial.coe_bit0 MvPolynomial.coe_bit0 - -set_option linter.deprecated false in -@[simp, norm_cast] -theorem coe_bit1 : - ((bit1 φ : MvPolynomial σ R) : MvPowerSeries σ R) = bit1 (φ : MvPowerSeries σ R) := by - rw [bit1, bit1, coe_add, coe_one, coe_bit0] -#align mv_polynomial.coe_bit1 MvPolynomial.coe_bit1 - -@[simp, norm_cast] -theorem coe_X (s : σ) : ((X s : MvPolynomial σ R) : MvPowerSeries σ R) = MvPowerSeries.X s := - coe_monomial _ _ -set_option linter.uppercaseLean3 false in -#align mv_polynomial.coe_X MvPolynomial.coe_X - -variable (σ R) - -theorem coe_injective : Function.Injective (Coe.coe : MvPolynomial σ R → MvPowerSeries σ R) := - fun x y h => by - ext - simp_rw [← coeff_coe] - congr -#align mv_polynomial.coe_injective MvPolynomial.coe_injective - -variable {σ R φ ψ} - -@[simp, norm_cast] -theorem coe_inj : (φ : MvPowerSeries σ R) = ψ ↔ φ = ψ := - (coe_injective σ R).eq_iff -#align mv_polynomial.coe_inj MvPolynomial.coe_inj - -@[simp] -theorem coe_eq_zero_iff : (φ : MvPowerSeries σ R) = 0 ↔ φ = 0 := by rw [← coe_zero, coe_inj] -#align mv_polynomial.coe_eq_zero_iff MvPolynomial.coe_eq_zero_iff - -@[simp] -theorem coe_eq_one_iff : (φ : MvPowerSeries σ R) = 1 ↔ φ = 1 := by rw [← coe_one, coe_inj] -#align mv_polynomial.coe_eq_one_iff MvPolynomial.coe_eq_one_iff - -/-- The coercion from multivariable polynomials to multivariable power series -as a ring homomorphism. --/ -def coeToMvPowerSeries.ringHom : MvPolynomial σ R →+* MvPowerSeries σ R where - toFun := (Coe.coe : MvPolynomial σ R → MvPowerSeries σ R) - map_zero' := coe_zero - map_one' := coe_one - map_add' := coe_add - map_mul' := coe_mul -#align mv_polynomial.coe_to_mv_power_series.ring_hom MvPolynomial.coeToMvPowerSeries.ringHom - -@[simp, norm_cast] -theorem coe_pow (n : ℕ) : - ((φ ^ n : MvPolynomial σ R) : MvPowerSeries σ R) = (φ : MvPowerSeries σ R) ^ n := - coeToMvPowerSeries.ringHom.map_pow _ _ -#align mv_polynomial.coe_pow MvPolynomial.coe_pow - -variable (φ ψ) +We provide the natural inclusion from polynomials to formal power series. -@[simp] -theorem coeToMvPowerSeries.ringHom_apply : coeToMvPowerSeries.ringHom φ = φ := - rfl -#align mv_polynomial.coe_to_mv_power_series.ring_hom_apply MvPolynomial.coeToMvPowerSeries.ringHom_apply +Additional results can be found in: +* `Mathlib.RingTheory.PowerSeries.Trunc`, truncation of power series; +* `Mathlib.RingTheory.PowerSeries.Inverse`, about inverses of power series, +and the fact that power series over a local ring form a local ring; +* `Mathlib.RingTheory.PowerSeries.Order`, the order of a power series at 0, +and application to the fact that power series over an integral domain +form an integral domain. -section Algebra +## Implementation notes -variable (A : Type*) [CommSemiring A] [Algebra R A] +Because of its definition, + `PowerSeries R := MvPowerSeries Unit R`. +a lot of proofs and properties from the multivariate case +can be ported to the single variable case. +However, it means that formal power series are indexed by `Unit →₀ ℕ`, +which is of course canonically isomorphic to `ℕ`. +We then build some glue to treat formal power series as if they were indexed by `ℕ`. +Occasionally this leads to proofs that are uglier than expected. -/-- The coercion from multivariable polynomials to multivariable power series -as an algebra homomorphism. -/ -def coeToMvPowerSeries.algHom : MvPolynomial σ R →ₐ[R] MvPowerSeries σ A := - { (MvPowerSeries.map σ (algebraMap R A)).comp coeToMvPowerSeries.ringHom with - commutes' := fun r => by simp [algebraMap_apply, MvPowerSeries.algebraMap_apply] } -#align mv_polynomial.coe_to_mv_power_series.alg_hom MvPolynomial.coeToMvPowerSeries.algHom - -@[simp] -theorem coeToMvPowerSeries.algHom_apply : - coeToMvPowerSeries.algHom A φ = MvPowerSeries.map σ (algebraMap R A) ↑φ := - rfl -#align mv_polynomial.coe_to_mv_power_series.alg_hom_apply MvPolynomial.coeToMvPowerSeries.algHom_apply -end Algebra - -end MvPolynomial - -namespace MvPowerSeries - -variable {σ R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A] (f : MvPowerSeries σ R) - -instance algebraMvPolynomial : Algebra (MvPolynomial σ R) (MvPowerSeries σ A) := - RingHom.toAlgebra (MvPolynomial.coeToMvPowerSeries.algHom A).toRingHom -#align mv_power_series.algebra_mv_polynomial MvPowerSeries.algebraMvPolynomial - -instance algebraMvPowerSeries : Algebra (MvPowerSeries σ R) (MvPowerSeries σ A) := - (map σ (algebraMap R A)).toAlgebra -#align mv_power_series.algebra_mv_power_series MvPowerSeries.algebraMvPowerSeries - -variable (A) - -theorem algebraMap_apply' (p : MvPolynomial σ R) : - algebraMap (MvPolynomial σ R) (MvPowerSeries σ A) p = map σ (algebraMap R A) p := - rfl -#align mv_power_series.algebra_map_apply' MvPowerSeries.algebraMap_apply' +noncomputable section -theorem algebraMap_apply'' : - algebraMap (MvPowerSeries σ R) (MvPowerSeries σ A) f = map σ (algebraMap R A) f := - rfl -#align mv_power_series.algebra_map_apply'' MvPowerSeries.algebraMap_apply'' +open BigOperators -end MvPowerSeries +open Finset (antidiagonal mem_antidiagonal) -/-- Formal power series over the coefficient ring `R`.-/ +/-- Formal power series over a coefficient type `R` -/ def PowerSeries (R : Type*) := MvPowerSeries Unit R #align power_series PowerSeries @@ -1869,196 +630,6 @@ theorem rescale_mul (a b : R) : rescale (a * b) = (rescale b).comp (rescale a) : end CommSemiring -section Trunc -variable [Semiring R] -open Finset Nat - -/-- The `n`th truncation of a formal power series to a polynomial -/ -def trunc (n : ℕ) (φ : R⟦X⟧) : R[X] := - ∑ m in Ico 0 n, Polynomial.monomial m (coeff R m φ) -#align power_series.trunc PowerSeries.trunc - -theorem coeff_trunc (m) (n) (φ : R⟦X⟧) : - (trunc n φ).coeff m = if m < n then coeff R m φ else 0 := by - simp [trunc, Polynomial.coeff_sum, Polynomial.coeff_monomial, Nat.lt_succ_iff] -#align power_series.coeff_trunc PowerSeries.coeff_trunc - -@[simp] -theorem trunc_zero (n) : trunc n (0 : R⟦X⟧) = 0 := - Polynomial.ext fun m => by - rw [coeff_trunc, LinearMap.map_zero, Polynomial.coeff_zero] - split_ifs <;> rfl -#align power_series.trunc_zero PowerSeries.trunc_zero - -@[simp] -theorem trunc_one (n) : trunc (n + 1) (1 : R⟦X⟧) = 1 := - Polynomial.ext fun m => by - rw [coeff_trunc, coeff_one, Polynomial.coeff_one] - split_ifs with h _ h' - · rfl - · rfl - · subst h'; simp at h - · rfl -#align power_series.trunc_one PowerSeries.trunc_one - -@[simp] -theorem trunc_C (n) (a : R) : trunc (n + 1) (C R a) = Polynomial.C a := - Polynomial.ext fun m => by - rw [coeff_trunc, coeff_C, Polynomial.coeff_C] - split_ifs with H <;> first |rfl|try simp_all -set_option linter.uppercaseLean3 false in -#align power_series.trunc_C PowerSeries.trunc_C - -@[simp] -theorem trunc_add (n) (φ ψ : R⟦X⟧) : trunc n (φ + ψ) = trunc n φ + trunc n ψ := - Polynomial.ext fun m => by - simp only [coeff_trunc, AddMonoidHom.map_add, Polynomial.coeff_add] - split_ifs with H - · rfl - · rw [zero_add] -#align power_series.trunc_add PowerSeries.trunc_add - -theorem trunc_succ (f : R⟦X⟧) (n : ℕ) : - trunc n.succ f = trunc n f + Polynomial.monomial n (coeff R n f) := by - rw [trunc, Ico_zero_eq_range, sum_range_succ, trunc, Ico_zero_eq_range] - -theorem natDegree_trunc_lt (f : R⟦X⟧) (n) : (trunc (n + 1) f).natDegree < n + 1 := by - rw [Nat.lt_succ_iff, natDegree_le_iff_coeff_eq_zero] - intros - rw [coeff_trunc] - split_ifs with h - · rw [lt_succ, ← not_lt] at h - contradiction - · rfl - -@[simp] lemma trunc_zero' {f : R⟦X⟧} : trunc 0 f = 0 := rfl - -theorem degree_trunc_lt (f : R⟦X⟧) (n) : (trunc n f).degree < n := by - rw [degree_lt_iff_coeff_zero] - intros - rw [coeff_trunc] - split_ifs with h - · rw [← not_le] at h - contradiction - · rfl - -theorem eval₂_trunc_eq_sum_range {S : Type*} [Semiring S] (s : S) (G : R →+* S) (n) (f : R⟦X⟧) : - (trunc n f).eval₂ G s = ∑ i in range n, G (coeff R i f) * s ^ i := by - cases n with - | zero => - rw [trunc_zero', range_zero, sum_empty, eval₂_zero] - | succ n => - have := natDegree_trunc_lt f n - rw [eval₂_eq_sum_range' (hn := this)] - apply sum_congr rfl - intro _ h - rw [mem_range] at h - congr - rw [coeff_trunc, if_pos h] - -@[simp] theorem trunc_X (n) : trunc (n + 2) X = (Polynomial.X : R[X]) := by - ext d - rw [coeff_trunc, coeff_X] - split_ifs with h₁ h₂ - · rw [h₂, coeff_X_one] - · rw [coeff_X_of_ne_one h₂] - · rw [coeff_X_of_ne_one] - intro hd - apply h₁ - rw [hd] - exact n.one_lt_succ_succ - -lemma trunc_X_of {n : ℕ} (hn : 2 ≤ n) : trunc n X = (Polynomial.X : R[X]) := by - cases n with - | zero => contradiction - | succ n => - cases n with - | zero => contradiction - | succ n => exact trunc_X n - -end Trunc - - -section Ring - -variable [Ring R] - -/-- Auxiliary function used for computing inverse of a power series -/ -protected def inv.aux : R → R⟦X⟧ → R⟦X⟧ := - MvPowerSeries.inv.aux -#align power_series.inv.aux PowerSeries.inv.aux - -theorem coeff_inv_aux (n : ℕ) (a : R) (φ : R⟦X⟧) : - coeff R n (inv.aux a φ) = - if n = 0 then a - else - -a * - ∑ x in antidiagonal n, - if x.2 < n then coeff R x.1 φ * coeff R x.2 (inv.aux a φ) else 0 := by - -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [coeff, inv.aux, MvPowerSeries.coeff_inv_aux] - simp only [Finsupp.single_eq_zero] - split_ifs; · rfl - congr 1 - symm - apply Finset.sum_nbij' (fun (a, b) ↦ (single () a, single () b)) - fun (f, g) ↦ (f (), g ()) - · aesop - · aesop - · aesop - · aesop - · rintro ⟨i, j⟩ _hij - obtain H | H := le_or_lt n j - · aesop - rw [if_pos H, if_pos] - · rfl - refine ⟨?_, fun hh ↦ H.not_le ?_⟩ - · rintro ⟨⟩ - simpa [Finsupp.single_eq_same] using le_of_lt H - · simpa [Finsupp.single_eq_same] using hh () -#align power_series.coeff_inv_aux PowerSeries.coeff_inv_aux - -/-- A formal power series is invertible if the constant coefficient is invertible.-/ -def invOfUnit (φ : R⟦X⟧) (u : Rˣ) : R⟦X⟧ := - MvPowerSeries.invOfUnit φ u -#align power_series.inv_of_unit PowerSeries.invOfUnit - -theorem coeff_invOfUnit (n : ℕ) (φ : R⟦X⟧) (u : Rˣ) : - coeff R n (invOfUnit φ u) = - if n = 0 then ↑u⁻¹ - else - -↑u⁻¹ * - ∑ x in antidiagonal n, - if x.2 < n then coeff R x.1 φ * coeff R x.2 (invOfUnit φ u) else 0 := - coeff_inv_aux n (↑u⁻¹ : R) φ -#align power_series.coeff_inv_of_unit PowerSeries.coeff_invOfUnit - -@[simp] -theorem constantCoeff_invOfUnit (φ : R⟦X⟧) (u : Rˣ) : - constantCoeff R (invOfUnit φ u) = ↑u⁻¹ := by - rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl] -#align power_series.constant_coeff_inv_of_unit PowerSeries.constantCoeff_invOfUnit - -theorem mul_invOfUnit (φ : R⟦X⟧) (u : Rˣ) (h : constantCoeff R φ = u) : - φ * invOfUnit φ u = 1 := - MvPowerSeries.mul_invOfUnit φ u <| h -#align power_series.mul_inv_of_unit PowerSeries.mul_invOfUnit - -/-- Two ways of removing the constant coefficient of a power series are the same. -/ -theorem sub_const_eq_shift_mul_X (φ : R⟦X⟧) : - φ - C R (constantCoeff R φ) = (PowerSeries.mk fun p => coeff R (p + 1) φ) * X := - sub_eq_iff_eq_add.mpr (eq_shift_mul_X_add_const φ) -set_option linter.uppercaseLean3 false in -#align power_series.sub_const_eq_shift_mul_X PowerSeries.sub_const_eq_shift_mul_X - -theorem sub_const_eq_X_mul_shift (φ : R⟦X⟧) : - φ - C R (constantCoeff R φ) = X * PowerSeries.mk fun p => coeff R (p + 1) φ := - sub_eq_iff_eq_add.mpr (eq_X_mul_shift_add_const φ) -set_option linter.uppercaseLean3 false in -#align power_series.sub_const_eq_X_mul_shift PowerSeries.sub_const_eq_X_mul_shift - -end Ring - section CommSemiring open Finset.HasAntidiagonal Finset @@ -2201,22 +772,6 @@ theorem rescale_injective {a : R} (ha : a ≠ 0) : Function.Injective (rescale a end IsDomain -section LocalRing - -variable {S : Type*} [CommRing R] [CommRing S] (f : R →+* S) [IsLocalRingHom f] - -instance map.isLocalRingHom : IsLocalRingHom (map f) := - MvPowerSeries.map.isLocalRingHom f -#align power_series.map.is_local_ring_hom PowerSeries.map.isLocalRingHom - -variable [LocalRing R] [LocalRing S] - -instance : LocalRing R⟦X⟧ := - { inferInstanceAs <| LocalRing <| MvPowerSeries Unit R with } - - -end LocalRing - section Algebra variable {A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] @@ -2235,434 +790,11 @@ instance [Nontrivial R] : Nontrivial (Subalgebra R R⟦X⟧) := end Algebra -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 := - MvPowerSeries.inv -#align power_series.inv PowerSeries.inv - -instance : Inv (PowerSeries k) := - ⟨PowerSeries.inv⟩ - -theorem inv_eq_inv_aux (φ : PowerSeries k) : φ⁻¹ = inv.aux (constantCoeff k φ)⁻¹ φ := - rfl -#align power_series.inv_eq_inv_aux PowerSeries.inv_eq_inv_aux - -theorem coeff_inv (n) (φ : PowerSeries k) : - coeff k n φ⁻¹ = - if n = 0 then (constantCoeff k φ)⁻¹ - else - -(constantCoeff k φ)⁻¹ * - ∑ x in antidiagonal n, - if x.2 < n then coeff k x.1 φ * coeff k x.2 φ⁻¹ else 0 := - by rw [inv_eq_inv_aux, coeff_inv_aux n (constantCoeff k φ)⁻¹ φ] -#align power_series.coeff_inv PowerSeries.coeff_inv - -@[simp] -theorem constantCoeff_inv (φ : PowerSeries k) : 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 := - MvPowerSeries.inv_eq_zero -#align power_series.inv_eq_zero PowerSeries.inv_eq_zero - -@[simp] -theorem zero_inv : (0 : PowerSeries k)⁻¹ = 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) : - 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) : - 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 := - 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 := - 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) : - φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂ := - 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) : - φ = ψ⁻¹ ↔ φ * ψ = 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) : - ψ⁻¹ = φ ↔ φ * ψ = 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) : (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹ := - MvPowerSeries.mul_inv_rev _ _ -#align power_series.mul_inv_rev PowerSeries.mul_inv_rev - -instance : InvOneClass (PowerSeries k) := - { inferInstanceAs <| InvOneClass <| MvPowerSeries Unit k with } - -@[simp] -theorem C_inv (r : k) : (C k r)⁻¹ = C k r⁻¹ := - MvPowerSeries.C_inv _ -set_option linter.uppercaseLean3 false in -#align power_series.C_inv PowerSeries.C_inv - -@[simp] -theorem X_inv : (X : PowerSeries k)⁻¹ = 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⁻¹ • φ⁻¹ := - MvPowerSeries.smul_inv _ _ -#align power_series.smul_inv PowerSeries.smul_inv - -end Field - -end PowerSeries - -namespace PowerSeries - -variable {R : Type*} - -section OrderBasic - -open multiplicity - -variable [Semiring R] {φ : R⟦X⟧} - -theorem exists_coeff_ne_zero_iff_ne_zero : (∃ n : ℕ, coeff R n φ ≠ 0) ↔ φ ≠ 0 := by - refine' not_iff_not.mp _ - push_neg - -- FIXME: the `FunLike.coe` doesn't seem to be picked up in the expression after #8386? - simp [PowerSeries.ext_iff, (coeff R _).map_zero] -#align power_series.exists_coeff_ne_zero_iff_ne_zero PowerSeries.exists_coeff_ne_zero_iff_ne_zero - -/-- The order of a formal power series `φ` is the greatest `n : PartENat` -such that `X^n` divides `φ`. The order is `⊤` if and only if `φ = 0`. -/ -def order (φ : R⟦X⟧) : PartENat := - letI := Classical.decEq R - letI := Classical.decEq R⟦X⟧ - if h : φ = 0 then ⊤ else Nat.find (exists_coeff_ne_zero_iff_ne_zero.mpr h) -#align power_series.order PowerSeries.order - -/-- The order of the `0` power series is infinite.-/ -@[simp] -theorem order_zero : order (0 : R⟦X⟧) = ⊤ := - dif_pos rfl -#align power_series.order_zero PowerSeries.order_zero - -theorem order_finite_iff_ne_zero : (order φ).Dom ↔ φ ≠ 0 := by - simp only [order] - constructor - · split_ifs with h <;> intro H - · contrapose! H - simp only [← Part.eq_none_iff'] - rfl - · exact h - · intro h - simp [h] -#align power_series.order_finite_iff_ne_zero PowerSeries.order_finite_iff_ne_zero - -/-- If the order of a formal power series is finite, -then the coefficient indexed by the order is nonzero.-/ -theorem coeff_order (h : (order φ).Dom) : coeff R (φ.order.get h) φ ≠ 0 := by - classical - simp only [order, order_finite_iff_ne_zero.mp h, not_false_iff, dif_neg, PartENat.get_natCast'] - generalize_proofs h - exact Nat.find_spec h -#align power_series.coeff_order PowerSeries.coeff_order - -/-- If the `n`th coefficient of a formal power series is nonzero, -then the order of the power series is less than or equal to `n`.-/ -theorem order_le (n : ℕ) (h : coeff R n φ ≠ 0) : order φ ≤ n := by - classical - rw [order, dif_neg] - · simp only [PartENat.coe_le_coe] - exact Nat.find_le h - · exact exists_coeff_ne_zero_iff_ne_zero.mp ⟨n, h⟩ -#align power_series.order_le PowerSeries.order_le - -/-- The `n`th coefficient of a formal power series is `0` if `n` is strictly -smaller than the order of the power series.-/ -theorem coeff_of_lt_order (n : ℕ) (h : ↑n < order φ) : coeff R n φ = 0 := by - contrapose! h - exact order_le _ h -#align power_series.coeff_of_lt_order PowerSeries.coeff_of_lt_order - -/-- The `0` power series is the unique power series with infinite order.-/ -@[simp] -theorem order_eq_top {φ : R⟦X⟧} : φ.order = ⊤ ↔ φ = 0 := by - constructor - · intro h - ext n - rw [(coeff R n).map_zero, coeff_of_lt_order] - simp [h] - · rintro rfl - exact order_zero -#align power_series.order_eq_top PowerSeries.order_eq_top - -/-- The order of a formal power series is at least `n` if -the `i`th coefficient is `0` for all `i < n`.-/ -theorem nat_le_order (φ : R⟦X⟧) (n : ℕ) (h : ∀ i < n, coeff R i φ = 0) : ↑n ≤ order φ := by - by_contra H; rw [not_le] at H - have : (order φ).Dom := PartENat.dom_of_le_natCast H.le - rw [← PartENat.natCast_get this, PartENat.coe_lt_coe] at H - exact coeff_order this (h _ H) -#align power_series.nat_le_order PowerSeries.nat_le_order - -/-- The order of a formal power series is at least `n` if -the `i`th coefficient is `0` for all `i < n`.-/ -theorem le_order (φ : R⟦X⟧) (n : PartENat) (h : ∀ i : ℕ, ↑i < n → coeff R i φ = 0) : - n ≤ order φ := by - induction n using PartENat.casesOn - · show _ ≤ _ - rw [top_le_iff, order_eq_top] - ext i - exact h _ (PartENat.natCast_lt_top i) - · apply nat_le_order - simpa only [PartENat.coe_lt_coe] using h -#align power_series.le_order PowerSeries.le_order - -/-- The order of a formal power series is exactly `n` if the `n`th coefficient is nonzero, -and the `i`th coefficient is `0` for all `i < n`.-/ -theorem order_eq_nat {φ : R⟦X⟧} {n : ℕ} : - order φ = n ↔ coeff R n φ ≠ 0 ∧ ∀ i, i < n → coeff R i φ = 0 := by - classical - rcases eq_or_ne φ 0 with (rfl | hφ) - · simpa [(coeff R _).map_zero] using (PartENat.natCast_ne_top _).symm - simp [order, dif_neg hφ, Nat.find_eq_iff] -#align power_series.order_eq_nat PowerSeries.order_eq_nat - -/-- The order of a formal power series is exactly `n` if the `n`th coefficient is nonzero, -and the `i`th coefficient is `0` for all `i < n`.-/ -theorem order_eq {φ : R⟦X⟧} {n : PartENat} : - order φ = n ↔ (∀ i : ℕ, ↑i = n → coeff R i φ ≠ 0) ∧ ∀ i : ℕ, ↑i < n → coeff R i φ = 0 := by - induction n using PartENat.casesOn - · rw [order_eq_top] - constructor - · rintro rfl - constructor <;> intros - · exfalso - exact PartENat.natCast_ne_top ‹_› ‹_› - · exact (coeff _ _).map_zero - · rintro ⟨_h₁, h₂⟩ - ext i - exact h₂ i (PartENat.natCast_lt_top i) - · simpa [PartENat.natCast_inj] using order_eq_nat -#align power_series.order_eq PowerSeries.order_eq - -/-- The order of the sum of two formal power series - is at least the minimum of their orders.-/ -theorem le_order_add (φ ψ : R⟦X⟧) : min (order φ) (order ψ) ≤ order (φ + ψ) := by - refine' le_order _ _ _ - simp (config := { contextual := true }) [coeff_of_lt_order] -#align power_series.le_order_add PowerSeries.le_order_add - -private theorem order_add_of_order_eq.aux (φ ψ : R⟦X⟧) (_h : order φ ≠ order ψ) - (H : order φ < order ψ) : order (φ + ψ) ≤ order φ ⊓ order ψ := by - suffices order (φ + ψ) = order φ by - rw [le_inf_iff, this] - exact ⟨le_rfl, le_of_lt H⟩ - · rw [order_eq] - constructor - · intro i hi - rw [← hi] at H - rw [(coeff _ _).map_add, coeff_of_lt_order i H, add_zero] - exact (order_eq_nat.1 hi.symm).1 - · intro i hi - rw [(coeff _ _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H), - zero_add] --- #align power_series.order_add_of_order_eq.aux power_series.order_add_of_order_eq.aux - -/-- The order of the sum of two formal power series - is the minimum of their orders if their orders differ.-/ -theorem order_add_of_order_eq (φ ψ : R⟦X⟧) (h : order φ ≠ order ψ) : - order (φ + ψ) = order φ ⊓ order ψ := by - refine' le_antisymm _ (le_order_add _ _) - by_cases H₁ : order φ < order ψ - · apply order_add_of_order_eq.aux _ _ h H₁ - by_cases H₂ : order ψ < order φ - · simpa only [add_comm, inf_comm] using order_add_of_order_eq.aux _ _ h.symm H₂ - exfalso; exact h (le_antisymm (not_lt.1 H₂) (not_lt.1 H₁)) -#align power_series.order_add_of_order_eq PowerSeries.order_add_of_order_eq - -/-- The order of the product of two formal power series - is at least the sum of their orders.-/ -theorem order_mul_ge (φ ψ : R⟦X⟧) : order φ + order ψ ≤ order (φ * ψ) := by - apply le_order - intro n hn; rw [coeff_mul, Finset.sum_eq_zero] - rintro ⟨i, j⟩ hij - by_cases hi : ↑i < order φ - · rw [coeff_of_lt_order i hi, zero_mul] - by_cases hj : ↑j < order ψ - · rw [coeff_of_lt_order j hj, mul_zero] - rw [not_lt] at hi hj; rw [mem_antidiagonal] at hij - exfalso - apply ne_of_lt (lt_of_lt_of_le hn <| add_le_add hi hj) - rw [← Nat.cast_add, hij] -#align power_series.order_mul_ge PowerSeries.order_mul_ge - -/-- The order of the monomial `a*X^n` is infinite if `a = 0` and `n` otherwise.-/ -theorem order_monomial (n : ℕ) (a : R) [Decidable (a = 0)] : - order (monomial R n a) = if a = 0 then (⊤ : PartENat) else n := by - split_ifs with h - · rw [h, order_eq_top, LinearMap.map_zero] - · rw [order_eq] - constructor <;> intro i hi - · rw [PartENat.natCast_inj] at hi - rwa [hi, coeff_monomial_same] - · rw [PartENat.coe_lt_coe] at hi - rw [coeff_monomial, if_neg] - exact ne_of_lt hi -#align power_series.order_monomial PowerSeries.order_monomial - -/-- The order of the monomial `a*X^n` is `n` if `a ≠ 0`.-/ -theorem order_monomial_of_ne_zero (n : ℕ) (a : R) (h : a ≠ 0) : order (monomial R n a) = n := by - classical - rw [order_monomial, if_neg h] -#align power_series.order_monomial_of_ne_zero PowerSeries.order_monomial_of_ne_zero - -/-- If `n` is strictly smaller than the order of `ψ`, then the `n`th coefficient of its product -with any other power series is `0`. -/ -theorem coeff_mul_of_lt_order {φ ψ : R⟦X⟧} {n : ℕ} (h : ↑n < ψ.order) : - coeff R n (φ * ψ) = 0 := by - suffices coeff R n (φ * ψ) = ∑ p in antidiagonal n, 0 by rw [this, Finset.sum_const_zero] - rw [coeff_mul] - apply Finset.sum_congr rfl - intro x hx - refine' mul_eq_zero_of_right (coeff R x.fst φ) (coeff_of_lt_order x.snd (lt_of_le_of_lt _ h)) - rw [mem_antidiagonal] at hx - norm_cast - linarith -#align power_series.coeff_mul_of_lt_order PowerSeries.coeff_mul_of_lt_order - -theorem coeff_mul_one_sub_of_lt_order {R : Type*} [CommRing R] {φ ψ : R⟦X⟧} (n : ℕ) - (h : ↑n < ψ.order) : coeff R n (φ * (1 - ψ)) = coeff R n φ := by - simp [coeff_mul_of_lt_order h, mul_sub] -#align power_series.coeff_mul_one_sub_of_lt_order PowerSeries.coeff_mul_one_sub_of_lt_order - -theorem coeff_mul_prod_one_sub_of_lt_order {R ι : Type*} [CommRing R] (k : ℕ) (s : Finset ι) - (φ : R⟦X⟧) (f : ι → R⟦X⟧) : - (∀ i ∈ s, ↑k < (f i).order) → coeff R k (φ * ∏ i in s, (1 - f i)) = coeff R k φ := by - classical - induction' s using Finset.induction_on with a s ha ih t - · simp - · intro t - simp only [Finset.mem_insert, forall_eq_or_imp] at t - rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm, coeff_mul_one_sub_of_lt_order _ t.1] - exact ih t.2 -#align power_series.coeff_mul_prod_one_sub_of_lt_order PowerSeries.coeff_mul_prod_one_sub_of_lt_order - --- TODO: link with `X_pow_dvd_iff` -theorem X_pow_order_dvd (h : (order φ).Dom) : X ^ (order φ).get h ∣ φ := by - refine' ⟨PowerSeries.mk fun n => coeff R (n + (order φ).get h) φ, _⟩ - ext n - simp only [coeff_mul, coeff_X_pow, coeff_mk, boole_mul, Finset.sum_ite, - Finset.sum_const_zero, add_zero] - rw [Finset.filter_fst_eq_antidiagonal n (Part.get (order φ) h)] - split_ifs with hn - · simp [tsub_add_cancel_of_le hn] - · simp only [Finset.sum_empty] - refine' coeff_of_lt_order _ _ - simpa [PartENat.coe_lt_iff] using fun _ => hn -set_option linter.uppercaseLean3 false in -#align power_series.X_pow_order_dvd PowerSeries.X_pow_order_dvd - -theorem order_eq_multiplicity_X {R : Type*} [Semiring R] [@DecidableRel R⟦X⟧ (· ∣ ·)] (φ : R⟦X⟧) : - order φ = multiplicity X φ := by - classical - rcases eq_or_ne φ 0 with (rfl | hφ) - · simp - induction' ho : order φ using PartENat.casesOn with n - · simp [hφ] at ho - have hn : φ.order.get (order_finite_iff_ne_zero.mpr hφ) = n := by simp [ho] - rw [← hn] - refine' - le_antisymm (le_multiplicity_of_pow_dvd <| X_pow_order_dvd (order_finite_iff_ne_zero.mpr hφ)) - (PartENat.find_le _ _ _) - rintro ⟨ψ, H⟩ - have := congr_arg (coeff R n) H - rw [← (ψ.commute_X.pow_right _).eq, coeff_mul_of_lt_order, ← hn] at this - · exact coeff_order _ this - · rw [X_pow_eq, order_monomial] - split_ifs - · exact PartENat.natCast_lt_top _ - · rw [← hn, PartENat.coe_lt_coe] - exact Nat.lt_succ_self _ -set_option linter.uppercaseLean3 false in -#align power_series.order_eq_multiplicity_X PowerSeries.order_eq_multiplicity_X - -end OrderBasic - -section OrderZeroNeOne - -variable [Semiring R] [Nontrivial R] - -/-- The order of the formal power series `1` is `0`.-/ -@[simp] -theorem order_one : order (1 : R⟦X⟧) = 0 := by - simpa using order_monomial_of_ne_zero 0 (1 : R) one_ne_zero -#align power_series.order_one PowerSeries.order_one - -/-- The order of the formal power series `X` is `1`.-/ -@[simp] -theorem order_X : order (X : R⟦X⟧) = 1 := by - simpa only [Nat.cast_one] using order_monomial_of_ne_zero 1 (1 : R) one_ne_zero -set_option linter.uppercaseLean3 false in -#align power_series.order_X PowerSeries.order_X - -/-- The order of the formal power series `X^n` is `n`.-/ -@[simp] -theorem order_X_pow (n : ℕ) : order ((X : R⟦X⟧) ^ n) = n := by - rw [X_pow_eq, order_monomial_of_ne_zero] - exact one_ne_zero -set_option linter.uppercaseLean3 false in -#align power_series.order_X_pow PowerSeries.order_X_pow - -end OrderZeroNeOne - -section OrderIsDomain - --- TODO: generalize to `[Semiring R] [NoZeroDivisors R]` -variable [CommRing R] [IsDomain R] - -/-- The order of the product of two formal power series over an integral domain - is the sum of their orders.-/ -theorem order_mul (φ ψ : R⟦X⟧) : order (φ * ψ) = order φ + order ψ := by - classical - simp_rw [order_eq_multiplicity_X] - exact multiplicity.mul X_prime -#align power_series.order_mul PowerSeries.order_mul - -end OrderIsDomain - end PowerSeries namespace Polynomial -open Finsupp +open Finsupp Polynomial variable {σ : Type*} {R : Type*} [CommSemiring R] (φ ψ : R[X]) @@ -2822,6 +954,8 @@ namespace PowerSeries section Algebra +open Polynomial + variable {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A] (f : R⟦X⟧) instance algebraPolynomial : Algebra R[X] A⟦X⟧ := @@ -2851,82 +985,6 @@ theorem algebraMap_apply'' : end Algebra -section Trunc -/- -Lemmas in this section involve the coercion `R[X] → R⟦X⟧`, so they may only be stated in the case -`R` is commutative. This is because the coercion is an `R`-algebra map. --/ -variable {R : Type*} [CommSemiring R] - -open Nat hiding pow_succ pow_zero -open Polynomial BigOperators Finset Finset.Nat - -theorem trunc_trunc_of_le {n m} (f : R⟦X⟧) (hnm : n ≤ m := by rfl) : - trunc n ↑(trunc m f) = trunc n f := by - ext d - rw [coeff_trunc, coeff_trunc, coeff_coe] - split_ifs with h - · rw [coeff_trunc, if_pos <| lt_of_lt_of_le h hnm] - · rfl - -@[simp] theorem trunc_trunc {n} (f : R⟦X⟧) : trunc n ↑(trunc n f) = trunc n f := - trunc_trunc_of_le f - -@[simp] theorem trunc_trunc_mul {n} (f g : R ⟦X⟧) : - trunc n ((trunc n f) * g : R⟦X⟧) = trunc n (f * g) := by - ext m - rw [coeff_trunc, coeff_trunc] - split_ifs with h - · rw [coeff_mul, coeff_mul, sum_congr rfl] - intro _ hab - have ha := lt_of_le_of_lt (antidiagonal.fst_le hab) h - rw [coeff_coe, coeff_trunc, if_pos ha] - · rfl - -@[simp] theorem trunc_mul_trunc {n} (f g : R ⟦X⟧) : - trunc n (f * (trunc n g) : R⟦X⟧) = trunc n (f * g) := by - rw [mul_comm, trunc_trunc_mul, mul_comm] - -theorem trunc_trunc_mul_trunc {n} (f g : R⟦X⟧) : - trunc n (trunc n f * trunc n g : R⟦X⟧) = trunc n (f * g) := by - rw [trunc_trunc_mul, trunc_mul_trunc] - -@[simp] theorem trunc_trunc_pow (f : R⟦X⟧) (n a : ℕ) : - trunc n ((trunc n f : R⟦X⟧) ^ a) = trunc n (f ^ a) := by - induction a with - | zero => - rw [pow_zero, pow_zero] - | succ a ih => - rw [pow_succ, pow_succ, trunc_trunc_mul, ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc] - -theorem trunc_coe_eq_self {n} {f : R[X]} (hn : natDegree f < n) : trunc n (f : R⟦X⟧) = f := by - rw [← Polynomial.coe_inj] - ext m - rw [coeff_coe, coeff_trunc] - split - case inl h => rfl - case inr h => - rw [not_lt] at h - rw [coeff_coe]; symm - exact coeff_eq_zero_of_natDegree_lt <| lt_of_lt_of_le hn h - -/-- The function `coeff n : R⟦X⟧ → R` is continuous. I.e. `coeff n f` depends only on a sufficiently -long truncation of the power series `f`.-/ -theorem coeff_coe_trunc_of_lt {n m} {f : R⟦X⟧} (h : n < m) : - coeff R n (trunc m f) = coeff R n f := by - rwa [coeff_coe, coeff_trunc, if_pos] - -/-- The `n`-th coefficient of `f*g` may be calculated -from the truncations of `f` and `g`.-/ -theorem coeff_mul_eq_coeff_trunc_mul_trunc₂ {n a b} (f g) (ha : n < a) (hb : n < b) : - coeff R n (f * g) = coeff R n (trunc a f * trunc b g) := by - symm - rw [← coeff_coe_trunc_of_lt n.lt_succ_self, ← trunc_trunc_mul_trunc, trunc_trunc_of_le f ha, - trunc_trunc_of_le g hb, trunc_trunc_mul_trunc, coeff_coe_trunc_of_lt n.lt_succ_self] - -theorem coeff_mul_eq_coeff_trunc_mul_trunc {d n} (f g) (h : d < n) : - coeff R d (f * g) = coeff R d (trunc n f * trunc n g) := - coeff_mul_eq_coeff_trunc_mul_trunc₂ f g h h - -end Trunc end PowerSeries + +end diff --git a/Mathlib/RingTheory/PowerSeries/Derivative.lean b/Mathlib/RingTheory/PowerSeries/Derivative.lean index 6ba52e30cb2dc..eec79ddb70651 100644 --- a/Mathlib/RingTheory/PowerSeries/Derivative.lean +++ b/Mathlib/RingTheory/PowerSeries/Derivative.lean @@ -3,7 +3,8 @@ Copyright (c) 2023 Richard M. Hill. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Richard M. Hill -/ -import Mathlib.RingTheory.PowerSeries.Basic +import Mathlib.RingTheory.PowerSeries.Trunc +import Mathlib.RingTheory.PowerSeries.Inverse import Mathlib.RingTheory.Derivation.Basic /-! diff --git a/Mathlib/RingTheory/PowerSeries/Inverse.lean b/Mathlib/RingTheory/PowerSeries/Inverse.lean new file mode 100644 index 0000000000000..4a4459c14b7d2 --- /dev/null +++ b/Mathlib/RingTheory/PowerSeries/Inverse.lean @@ -0,0 +1,242 @@ +/- +Copyright (c) 2019 Johan Commelin. All rights reserved. +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.MvPowerSeries.Inverse + +#align_import ring_theory.power_series.basic from "leanprover-community/mathlib"@"2d5739b61641ee4e7e53eca5688a08f66f2e6a60" + +/-! # Formal power series - Inverses + +If the constant coefficient of a formal (univariate) power series is invertible, +then this formal power series is invertible. +(See the discussion in `Mathlib.RingTheory.MvPowerSeries.Inverse` for +the construction.) + +Formal (univariate) power series over a local ring form a local ring. + + +-/ + + +noncomputable section + +open BigOperators Polynomial + +open Finset (antidiagonal mem_antidiagonal) + +namespace PowerSeries + +open Finsupp (single) + +variable {R : Type*} + + +section Ring + +variable [Ring R] + +/-- Auxiliary function used for computing inverse of a power series -/ +protected def inv.aux : R → R⟦X⟧ → R⟦X⟧ := + MvPowerSeries.inv.aux +#align power_series.inv.aux PowerSeries.inv.aux + +theorem coeff_inv_aux (n : ℕ) (a : R) (φ : R⟦X⟧) : + coeff R n (inv.aux a φ) = + if n = 0 then a + else + -a * + ∑ x in antidiagonal n, + if x.2 < n then coeff R x.1 φ * coeff R x.2 (inv.aux a φ) else 0 := by + -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 + erw [coeff, inv.aux, MvPowerSeries.coeff_inv_aux] + simp only [Finsupp.single_eq_zero] + split_ifs; · rfl + congr 1 + symm + apply Finset.sum_nbij' (fun (a, b) ↦ (single () a, single () b)) + fun (f, g) ↦ (f (), g ()) + · aesop + · aesop + · aesop + · aesop + · rintro ⟨i, j⟩ _hij + obtain H | H := le_or_lt n j + · aesop + rw [if_pos H, if_pos] + · rfl + refine ⟨?_, fun hh ↦ H.not_le ?_⟩ + · rintro ⟨⟩ + simpa [Finsupp.single_eq_same] using le_of_lt H + · simpa [Finsupp.single_eq_same] using hh () +#align power_series.coeff_inv_aux PowerSeries.coeff_inv_aux + +/-- A formal power series is invertible if the constant coefficient is invertible.-/ +def invOfUnit (φ : R⟦X⟧) (u : Rˣ) : R⟦X⟧ := + MvPowerSeries.invOfUnit φ u +#align power_series.inv_of_unit PowerSeries.invOfUnit + +theorem coeff_invOfUnit (n : ℕ) (φ : R⟦X⟧) (u : Rˣ) : + coeff R n (invOfUnit φ u) = + if n = 0 then ↑u⁻¹ + else + -↑u⁻¹ * + ∑ x in antidiagonal n, + if x.2 < n then coeff R x.1 φ * coeff R x.2 (invOfUnit φ u) else 0 := + coeff_inv_aux n (↑u⁻¹ : R) φ +#align power_series.coeff_inv_of_unit PowerSeries.coeff_invOfUnit + +@[simp] +theorem constantCoeff_invOfUnit (φ : R⟦X⟧) (u : Rˣ) : + constantCoeff R (invOfUnit φ u) = ↑u⁻¹ := by + rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl] +#align power_series.constant_coeff_inv_of_unit PowerSeries.constantCoeff_invOfUnit + +theorem mul_invOfUnit (φ : R⟦X⟧) (u : Rˣ) (h : constantCoeff R φ = u) : + φ * invOfUnit φ u = 1 := + MvPowerSeries.mul_invOfUnit φ u <| h +#align power_series.mul_inv_of_unit PowerSeries.mul_invOfUnit + +/-- Two ways of removing the constant coefficient of a power series are the same. -/ +theorem sub_const_eq_shift_mul_X (φ : R⟦X⟧) : + φ - C R (constantCoeff R φ) = (PowerSeries.mk fun p => coeff R (p + 1) φ) * X := + sub_eq_iff_eq_add.mpr (eq_shift_mul_X_add_const φ) +set_option linter.uppercaseLean3 false in +#align power_series.sub_const_eq_shift_mul_X PowerSeries.sub_const_eq_shift_mul_X + +theorem sub_const_eq_X_mul_shift (φ : R⟦X⟧) : + φ - C R (constantCoeff R φ) = X * PowerSeries.mk fun p => coeff R (p + 1) φ := + sub_eq_iff_eq_add.mpr (eq_X_mul_shift_add_const φ) +set_option linter.uppercaseLean3 false in +#align power_series.sub_const_eq_X_mul_shift PowerSeries.sub_const_eq_X_mul_shift + +end Ring + +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 := + MvPowerSeries.inv +#align power_series.inv PowerSeries.inv + +instance : Inv (PowerSeries k) := + ⟨PowerSeries.inv⟩ + +theorem inv_eq_inv_aux (φ : PowerSeries k) : φ⁻¹ = inv.aux (constantCoeff k φ)⁻¹ φ := + rfl +#align power_series.inv_eq_inv_aux PowerSeries.inv_eq_inv_aux + +theorem coeff_inv (n) (φ : PowerSeries k) : + coeff k n φ⁻¹ = + if n = 0 then (constantCoeff k φ)⁻¹ + else + -(constantCoeff k φ)⁻¹ * + ∑ x in antidiagonal n, + if x.2 < n then coeff k x.1 φ * coeff k x.2 φ⁻¹ else 0 := + by rw [inv_eq_inv_aux, coeff_inv_aux n (constantCoeff k φ)⁻¹ φ] +#align power_series.coeff_inv PowerSeries.coeff_inv + +@[simp] +theorem constantCoeff_inv (φ : PowerSeries k) : 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 := + MvPowerSeries.inv_eq_zero +#align power_series.inv_eq_zero PowerSeries.inv_eq_zero + +@[simp] +theorem zero_inv : (0 : PowerSeries k)⁻¹ = 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) : + 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) : + 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 := + 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 := + 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) : + φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂ := + 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) : + φ = ψ⁻¹ ↔ φ * ψ = 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) : + ψ⁻¹ = φ ↔ φ * ψ = 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) : (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹ := + MvPowerSeries.mul_inv_rev _ _ +#align power_series.mul_inv_rev PowerSeries.mul_inv_rev + +instance : InvOneClass (PowerSeries k) := + { inferInstanceAs <| InvOneClass <| MvPowerSeries Unit k with } + +@[simp] +theorem C_inv (r : k) : (C k r)⁻¹ = C k r⁻¹ := + MvPowerSeries.C_inv _ +set_option linter.uppercaseLean3 false in +#align power_series.C_inv PowerSeries.C_inv + +@[simp] +theorem X_inv : (X : PowerSeries k)⁻¹ = 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⁻¹ • φ⁻¹ := + MvPowerSeries.smul_inv _ _ +#align power_series.smul_inv PowerSeries.smul_inv + +end Field + +section LocalRing + +variable {S : Type*} [CommRing R] [CommRing S] (f : R →+* S) [IsLocalRingHom f] + +instance map.isLocalRingHom : IsLocalRingHom (map f) := + MvPowerSeries.map.isLocalRingHom f +#align power_series.map.is_local_ring_hom PowerSeries.map.isLocalRingHom + +variable [LocalRing R] [LocalRing S] + +instance : LocalRing R⟦X⟧ := + { inferInstanceAs <| LocalRing <| MvPowerSeries Unit R with } + + +end LocalRing + + +end PowerSeries + +end diff --git a/Mathlib/RingTheory/PowerSeries/Order.lean b/Mathlib/RingTheory/PowerSeries/Order.lean new file mode 100644 index 0000000000000..484d508c33fd2 --- /dev/null +++ b/Mathlib/RingTheory/PowerSeries/Order.lean @@ -0,0 +1,350 @@ +/- +Copyright (c) 2019 Johan Commelin. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johan Commelin, Kenny Lau +-/ + +import Mathlib.RingTheory.PowerSeries.Basic +import Mathlib.Algebra.CharP.Basic + +#align_import ring_theory.power_series.basic from "leanprover-community/mathlib"@"2d5739b61641ee4e7e53eca5688a08f66f2e6a60" + +/-! # Formal power series (in one variable) - Order + +The `PowerSeries.order` of a formal power series `φ` is the multiplicity of the variable `X` in `φ`. + +If the coefficients form an integral domain, then `PowerSeries.order` is an +additive valuation (`PowerSeries.order_mul`, `PowerSeries.le_order_add`). + +We prove that if the commutative ring `R` of coefficients is an integral domain, +then the ring `R⟦X⟧` of formal power series in one variable over `R` +is an integral domain. + +-/ +noncomputable section + +open BigOperators Polynomial + +open Finset (antidiagonal mem_antidiagonal) + +namespace PowerSeries + +open Finsupp (single) + +variable {R : Type*} + +section OrderBasic + +open multiplicity + +variable [Semiring R] {φ : R⟦X⟧} + +theorem exists_coeff_ne_zero_iff_ne_zero : (∃ n : ℕ, coeff R n φ ≠ 0) ↔ φ ≠ 0 := by + refine' not_iff_not.mp _ + push_neg + -- FIXME: the `FunLike.coe` doesn't seem to be picked up in the expression after #8386? + simp [PowerSeries.ext_iff, (coeff R _).map_zero] +#align power_series.exists_coeff_ne_zero_iff_ne_zero PowerSeries.exists_coeff_ne_zero_iff_ne_zero + +/-- The order of a formal power series `φ` is the greatest `n : PartENat` +such that `X^n` divides `φ`. The order is `⊤` if and only if `φ = 0`. -/ +def order (φ : R⟦X⟧) : PartENat := + letI := Classical.decEq R + letI := Classical.decEq R⟦X⟧ + if h : φ = 0 then ⊤ else Nat.find (exists_coeff_ne_zero_iff_ne_zero.mpr h) +#align power_series.order PowerSeries.order + +/-- The order of the `0` power series is infinite.-/ +@[simp] +theorem order_zero : order (0 : R⟦X⟧) = ⊤ := + dif_pos rfl +#align power_series.order_zero PowerSeries.order_zero + +theorem order_finite_iff_ne_zero : (order φ).Dom ↔ φ ≠ 0 := by + simp only [order] + constructor + · split_ifs with h <;> intro H + · contrapose! H + simp only [← Part.eq_none_iff'] + rfl + · exact h + · intro h + simp [h] +#align power_series.order_finite_iff_ne_zero PowerSeries.order_finite_iff_ne_zero + +/-- If the order of a formal power series is finite, +then the coefficient indexed by the order is nonzero.-/ +theorem coeff_order (h : (order φ).Dom) : coeff R (φ.order.get h) φ ≠ 0 := by + classical + simp only [order, order_finite_iff_ne_zero.mp h, not_false_iff, dif_neg, PartENat.get_natCast'] + generalize_proofs h + exact Nat.find_spec h +#align power_series.coeff_order PowerSeries.coeff_order + +/-- If the `n`th coefficient of a formal power series is nonzero, +then the order of the power series is less than or equal to `n`.-/ +theorem order_le (n : ℕ) (h : coeff R n φ ≠ 0) : order φ ≤ n := by + classical + rw [order, dif_neg] + · simp only [PartENat.coe_le_coe] + exact Nat.find_le h + · exact exists_coeff_ne_zero_iff_ne_zero.mp ⟨n, h⟩ +#align power_series.order_le PowerSeries.order_le + +/-- The `n`th coefficient of a formal power series is `0` if `n` is strictly +smaller than the order of the power series.-/ +theorem coeff_of_lt_order (n : ℕ) (h : ↑n < order φ) : coeff R n φ = 0 := by + contrapose! h + exact order_le _ h +#align power_series.coeff_of_lt_order PowerSeries.coeff_of_lt_order + +/-- The `0` power series is the unique power series with infinite order.-/ +@[simp] +theorem order_eq_top {φ : R⟦X⟧} : φ.order = ⊤ ↔ φ = 0 := by + constructor + · intro h + ext n + rw [(coeff R n).map_zero, coeff_of_lt_order] + simp [h] + · rintro rfl + exact order_zero +#align power_series.order_eq_top PowerSeries.order_eq_top + +/-- The order of a formal power series is at least `n` if +the `i`th coefficient is `0` for all `i < n`.-/ +theorem nat_le_order (φ : R⟦X⟧) (n : ℕ) (h : ∀ i < n, coeff R i φ = 0) : ↑n ≤ order φ := by + by_contra H; rw [not_le] at H + have : (order φ).Dom := PartENat.dom_of_le_natCast H.le + rw [← PartENat.natCast_get this, PartENat.coe_lt_coe] at H + exact coeff_order this (h _ H) +#align power_series.nat_le_order PowerSeries.nat_le_order + +/-- The order of a formal power series is at least `n` if +the `i`th coefficient is `0` for all `i < n`.-/ +theorem le_order (φ : R⟦X⟧) (n : PartENat) (h : ∀ i : ℕ, ↑i < n → coeff R i φ = 0) : + n ≤ order φ := by + induction n using PartENat.casesOn + · show _ ≤ _ + rw [top_le_iff, order_eq_top] + ext i + exact h _ (PartENat.natCast_lt_top i) + · apply nat_le_order + simpa only [PartENat.coe_lt_coe] using h +#align power_series.le_order PowerSeries.le_order + +/-- The order of a formal power series is exactly `n` if the `n`th coefficient is nonzero, +and the `i`th coefficient is `0` for all `i < n`.-/ +theorem order_eq_nat {φ : R⟦X⟧} {n : ℕ} : + order φ = n ↔ coeff R n φ ≠ 0 ∧ ∀ i, i < n → coeff R i φ = 0 := by + classical + rcases eq_or_ne φ 0 with (rfl | hφ) + · simpa [(coeff R _).map_zero] using (PartENat.natCast_ne_top _).symm + simp [order, dif_neg hφ, Nat.find_eq_iff] +#align power_series.order_eq_nat PowerSeries.order_eq_nat + +/-- The order of a formal power series is exactly `n` if the `n`th coefficient is nonzero, +and the `i`th coefficient is `0` for all `i < n`.-/ +theorem order_eq {φ : R⟦X⟧} {n : PartENat} : + order φ = n ↔ (∀ i : ℕ, ↑i = n → coeff R i φ ≠ 0) ∧ ∀ i : ℕ, ↑i < n → coeff R i φ = 0 := by + induction n using PartENat.casesOn + · rw [order_eq_top] + constructor + · rintro rfl + constructor <;> intros + · exfalso + exact PartENat.natCast_ne_top ‹_› ‹_› + · exact (coeff _ _).map_zero + · rintro ⟨_h₁, h₂⟩ + ext i + exact h₂ i (PartENat.natCast_lt_top i) + · simpa [PartENat.natCast_inj] using order_eq_nat +#align power_series.order_eq PowerSeries.order_eq + +/-- The order of the sum of two formal power series + is at least the minimum of their orders.-/ +theorem le_order_add (φ ψ : R⟦X⟧) : min (order φ) (order ψ) ≤ order (φ + ψ) := by + refine' le_order _ _ _ + simp (config := { contextual := true }) [coeff_of_lt_order] +#align power_series.le_order_add PowerSeries.le_order_add + +private theorem order_add_of_order_eq.aux (φ ψ : R⟦X⟧) (_h : order φ ≠ order ψ) + (H : order φ < order ψ) : order (φ + ψ) ≤ order φ ⊓ order ψ := by + suffices order (φ + ψ) = order φ by + rw [le_inf_iff, this] + exact ⟨le_rfl, le_of_lt H⟩ + · rw [order_eq] + constructor + · intro i hi + rw [← hi] at H + rw [(coeff _ _).map_add, coeff_of_lt_order i H, add_zero] + exact (order_eq_nat.1 hi.symm).1 + · intro i hi + rw [(coeff _ _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H), + zero_add] +-- #align power_series.order_add_of_order_eq.aux power_series.order_add_of_order_eq.aux + +/-- The order of the sum of two formal power series + is the minimum of their orders if their orders differ.-/ +theorem order_add_of_order_eq (φ ψ : R⟦X⟧) (h : order φ ≠ order ψ) : + order (φ + ψ) = order φ ⊓ order ψ := by + refine' le_antisymm _ (le_order_add _ _) + by_cases H₁ : order φ < order ψ + · apply order_add_of_order_eq.aux _ _ h H₁ + by_cases H₂ : order ψ < order φ + · simpa only [add_comm, inf_comm] using order_add_of_order_eq.aux _ _ h.symm H₂ + exfalso; exact h (le_antisymm (not_lt.1 H₂) (not_lt.1 H₁)) +#align power_series.order_add_of_order_eq PowerSeries.order_add_of_order_eq + +/-- The order of the product of two formal power series + is at least the sum of their orders.-/ +theorem order_mul_ge (φ ψ : R⟦X⟧) : order φ + order ψ ≤ order (φ * ψ) := by + apply le_order + intro n hn; rw [coeff_mul, Finset.sum_eq_zero] + rintro ⟨i, j⟩ hij + by_cases hi : ↑i < order φ + · rw [coeff_of_lt_order i hi, zero_mul] + by_cases hj : ↑j < order ψ + · rw [coeff_of_lt_order j hj, mul_zero] + rw [not_lt] at hi hj; rw [mem_antidiagonal] at hij + exfalso + apply ne_of_lt (lt_of_lt_of_le hn <| add_le_add hi hj) + rw [← Nat.cast_add, hij] +#align power_series.order_mul_ge PowerSeries.order_mul_ge + +/-- The order of the monomial `a*X^n` is infinite if `a = 0` and `n` otherwise.-/ +theorem order_monomial (n : ℕ) (a : R) [Decidable (a = 0)] : + order (monomial R n a) = if a = 0 then (⊤ : PartENat) else n := by + split_ifs with h + · rw [h, order_eq_top, LinearMap.map_zero] + · rw [order_eq] + constructor <;> intro i hi + · rw [PartENat.natCast_inj] at hi + rwa [hi, coeff_monomial_same] + · rw [PartENat.coe_lt_coe] at hi + rw [coeff_monomial, if_neg] + exact ne_of_lt hi +#align power_series.order_monomial PowerSeries.order_monomial + +/-- The order of the monomial `a*X^n` is `n` if `a ≠ 0`.-/ +theorem order_monomial_of_ne_zero (n : ℕ) (a : R) (h : a ≠ 0) : order (monomial R n a) = n := by + classical + rw [order_monomial, if_neg h] +#align power_series.order_monomial_of_ne_zero PowerSeries.order_monomial_of_ne_zero + +/-- If `n` is strictly smaller than the order of `ψ`, then the `n`th coefficient of its product +with any other power series is `0`. -/ +theorem coeff_mul_of_lt_order {φ ψ : R⟦X⟧} {n : ℕ} (h : ↑n < ψ.order) : + coeff R n (φ * ψ) = 0 := by + suffices coeff R n (φ * ψ) = ∑ p in antidiagonal n, 0 by rw [this, Finset.sum_const_zero] + rw [coeff_mul] + apply Finset.sum_congr rfl + intro x hx + refine' mul_eq_zero_of_right (coeff R x.fst φ) (coeff_of_lt_order x.snd (lt_of_le_of_lt _ h)) + rw [mem_antidiagonal] at hx + norm_cast + linarith +#align power_series.coeff_mul_of_lt_order PowerSeries.coeff_mul_of_lt_order + +theorem coeff_mul_one_sub_of_lt_order {R : Type*} [CommRing R] {φ ψ : R⟦X⟧} (n : ℕ) + (h : ↑n < ψ.order) : coeff R n (φ * (1 - ψ)) = coeff R n φ := by + simp [coeff_mul_of_lt_order h, mul_sub] +#align power_series.coeff_mul_one_sub_of_lt_order PowerSeries.coeff_mul_one_sub_of_lt_order + +theorem coeff_mul_prod_one_sub_of_lt_order {R ι : Type*} [CommRing R] (k : ℕ) (s : Finset ι) + (φ : R⟦X⟧) (f : ι → R⟦X⟧) : + (∀ i ∈ s, ↑k < (f i).order) → coeff R k (φ * ∏ i in s, (1 - f i)) = coeff R k φ := by + classical + induction' s using Finset.induction_on with a s ha ih t + · simp + · intro t + simp only [Finset.mem_insert, forall_eq_or_imp] at t + rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm, coeff_mul_one_sub_of_lt_order _ t.1] + exact ih t.2 +#align power_series.coeff_mul_prod_one_sub_of_lt_order PowerSeries.coeff_mul_prod_one_sub_of_lt_order + +-- TODO: link with `X_pow_dvd_iff` +theorem X_pow_order_dvd (h : (order φ).Dom) : X ^ (order φ).get h ∣ φ := by + refine' ⟨PowerSeries.mk fun n => coeff R (n + (order φ).get h) φ, _⟩ + ext n + simp only [coeff_mul, coeff_X_pow, coeff_mk, boole_mul, Finset.sum_ite, + Finset.sum_const_zero, add_zero] + rw [Finset.filter_fst_eq_antidiagonal n (Part.get (order φ) h)] + split_ifs with hn + · simp [tsub_add_cancel_of_le hn] + · simp only [Finset.sum_empty] + refine' coeff_of_lt_order _ _ + simpa [PartENat.coe_lt_iff] using fun _ => hn +set_option linter.uppercaseLean3 false in +#align power_series.X_pow_order_dvd PowerSeries.X_pow_order_dvd + +theorem order_eq_multiplicity_X {R : Type*} [Semiring R] [@DecidableRel R⟦X⟧ (· ∣ ·)] (φ : R⟦X⟧) : + order φ = multiplicity X φ := by + classical + rcases eq_or_ne φ 0 with (rfl | hφ) + · simp + induction' ho : order φ using PartENat.casesOn with n + · simp [hφ] at ho + have hn : φ.order.get (order_finite_iff_ne_zero.mpr hφ) = n := by simp [ho] + rw [← hn] + refine' + le_antisymm (le_multiplicity_of_pow_dvd <| X_pow_order_dvd (order_finite_iff_ne_zero.mpr hφ)) + (PartENat.find_le _ _ _) + rintro ⟨ψ, H⟩ + have := congr_arg (coeff R n) H + rw [← (ψ.commute_X.pow_right _).eq, coeff_mul_of_lt_order, ← hn] at this + · exact coeff_order _ this + · rw [X_pow_eq, order_monomial] + split_ifs + · exact PartENat.natCast_lt_top _ + · rw [← hn, PartENat.coe_lt_coe] + exact Nat.lt_succ_self _ +set_option linter.uppercaseLean3 false in +#align power_series.order_eq_multiplicity_X PowerSeries.order_eq_multiplicity_X + +end OrderBasic + +section OrderZeroNeOne + +variable [Semiring R] [Nontrivial R] + +/-- The order of the formal power series `1` is `0`.-/ +@[simp] +theorem order_one : order (1 : R⟦X⟧) = 0 := by + simpa using order_monomial_of_ne_zero 0 (1 : R) one_ne_zero +#align power_series.order_one PowerSeries.order_one + +/-- The order of the formal power series `X` is `1`.-/ +@[simp] +theorem order_X : order (X : R⟦X⟧) = 1 := by + simpa only [Nat.cast_one] using order_monomial_of_ne_zero 1 (1 : R) one_ne_zero +set_option linter.uppercaseLean3 false in +#align power_series.order_X PowerSeries.order_X + +/-- The order of the formal power series `X^n` is `n`.-/ +@[simp] +theorem order_X_pow (n : ℕ) : order ((X : R⟦X⟧) ^ n) = n := by + rw [X_pow_eq, order_monomial_of_ne_zero] + exact one_ne_zero +set_option linter.uppercaseLean3 false in +#align power_series.order_X_pow PowerSeries.order_X_pow + +end OrderZeroNeOne + +section OrderIsDomain + +-- TODO: generalize to `[Semiring R] [NoZeroDivisors R]` +variable [CommRing R] [IsDomain R] + +/-- The order of the product of two formal power series over an integral domain + is the sum of their orders.-/ +theorem order_mul (φ ψ : R⟦X⟧) : order (φ * ψ) = order φ + order ψ := by + classical + simp_rw [order_eq_multiplicity_X] + exact multiplicity.mul X_prime +#align power_series.order_mul PowerSeries.order_mul + +end OrderIsDomain + +end PowerSeries + +end diff --git a/Mathlib/RingTheory/PowerSeries/Trunc.lean b/Mathlib/RingTheory/PowerSeries/Trunc.lean new file mode 100644 index 0000000000000..3e4592cb526fa --- /dev/null +++ b/Mathlib/RingTheory/PowerSeries/Trunc.lean @@ -0,0 +1,226 @@ +/- +Copyright (c) 2019 Johan Commelin. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johan Commelin, Kenny Lau +-/ + +import Mathlib.RingTheory.PowerSeries.Basic +import Mathlib.Data.Polynomial.Coeff +import Mathlib.Data.Polynomial.Degree.Lemmas + +#align_import ring_theory.power_series.basic from "leanprover-community/mathlib"@"2d5739b61641ee4e7e53eca5688a08f66f2e6a60" + + +/-! + +# Formal power series in one variable - Truncation + +`PowerSeries.trunc n φ` truncates a (univariate) formal power series +to the polynomial that has the same coefficients as `φ`, for all `m < n`, +and `0` otherwise. + +-/ + +noncomputable section + +open BigOperators Polynomial + +open Finset (antidiagonal mem_antidiagonal) + +namespace PowerSeries + +open Finsupp (single) + +variable {R : Type*} + +section Trunc +variable [Semiring R] +open Finset Nat + +/-- The `n`th truncation of a formal power series to a polynomial -/ +def trunc (n : ℕ) (φ : R⟦X⟧) : R[X] := + ∑ m in Ico 0 n, Polynomial.monomial m (coeff R m φ) +#align power_series.trunc PowerSeries.trunc + +theorem coeff_trunc (m) (n) (φ : R⟦X⟧) : + (trunc n φ).coeff m = if m < n then coeff R m φ else 0 := by + simp [trunc, Polynomial.coeff_sum, Polynomial.coeff_monomial, Nat.lt_succ_iff] +#align power_series.coeff_trunc PowerSeries.coeff_trunc + +@[simp] +theorem trunc_zero (n) : trunc n (0 : R⟦X⟧) = 0 := + Polynomial.ext fun m => by + rw [coeff_trunc, LinearMap.map_zero, Polynomial.coeff_zero] + split_ifs <;> rfl +#align power_series.trunc_zero PowerSeries.trunc_zero + +@[simp] +theorem trunc_one (n) : trunc (n + 1) (1 : R⟦X⟧) = 1 := + Polynomial.ext fun m => by + rw [coeff_trunc, coeff_one, Polynomial.coeff_one] + split_ifs with h _ h' + · rfl + · rfl + · subst h'; simp at h + · rfl +#align power_series.trunc_one PowerSeries.trunc_one + +@[simp] +theorem trunc_C (n) (a : R) : trunc (n + 1) (C R a) = Polynomial.C a := + Polynomial.ext fun m => by + rw [coeff_trunc, coeff_C, Polynomial.coeff_C] + split_ifs with H <;> first |rfl|try simp_all +set_option linter.uppercaseLean3 false in +#align power_series.trunc_C PowerSeries.trunc_C + +@[simp] +theorem trunc_add (n) (φ ψ : R⟦X⟧) : trunc n (φ + ψ) = trunc n φ + trunc n ψ := + Polynomial.ext fun m => by + simp only [coeff_trunc, AddMonoidHom.map_add, Polynomial.coeff_add] + split_ifs with H + · rfl + · rw [zero_add] +#align power_series.trunc_add PowerSeries.trunc_add + +theorem trunc_succ (f : R⟦X⟧) (n : ℕ) : + trunc n.succ f = trunc n f + Polynomial.monomial n (coeff R n f) := by + rw [trunc, Ico_zero_eq_range, sum_range_succ, trunc, Ico_zero_eq_range] + +theorem natDegree_trunc_lt (f : R⟦X⟧) (n) : (trunc (n + 1) f).natDegree < n + 1 := by + rw [Nat.lt_succ_iff, natDegree_le_iff_coeff_eq_zero] + intros + rw [coeff_trunc] + split_ifs with h + · rw [lt_succ, ← not_lt] at h + contradiction + · rfl + +@[simp] lemma trunc_zero' {f : R⟦X⟧} : trunc 0 f = 0 := rfl + +theorem degree_trunc_lt (f : R⟦X⟧) (n) : (trunc n f).degree < n := by + rw [degree_lt_iff_coeff_zero] + intros + rw [coeff_trunc] + split_ifs with h + · rw [← not_le] at h + contradiction + · rfl + +theorem eval₂_trunc_eq_sum_range {S : Type*} [Semiring S] (s : S) (G : R →+* S) (n) (f : R⟦X⟧) : + (trunc n f).eval₂ G s = ∑ i in range n, G (coeff R i f) * s ^ i := by + cases n with + | zero => + rw [trunc_zero', range_zero, sum_empty, eval₂_zero] + | succ n => + have := natDegree_trunc_lt f n + rw [eval₂_eq_sum_range' (hn := this)] + apply sum_congr rfl + intro _ h + rw [mem_range] at h + congr + rw [coeff_trunc, if_pos h] + +@[simp] theorem trunc_X (n) : trunc (n + 2) X = (Polynomial.X : R[X]) := by + ext d + rw [coeff_trunc, coeff_X] + split_ifs with h₁ h₂ + · rw [h₂, coeff_X_one] + · rw [coeff_X_of_ne_one h₂] + · rw [coeff_X_of_ne_one] + intro hd + apply h₁ + rw [hd] + exact n.one_lt_succ_succ + +lemma trunc_X_of {n : ℕ} (hn : 2 ≤ n) : trunc n X = (Polynomial.X : R[X]) := by + cases n with + | zero => contradiction + | succ n => + cases n with + | zero => contradiction + | succ n => exact trunc_X n + +end Trunc + +section Trunc +/- +Lemmas in this section involve the coercion `R[X] → R⟦X⟧`, so they may only be stated in the case +`R` is commutative. This is because the coercion is an `R`-algebra map. +-/ +variable {R : Type*} [CommSemiring R] + +open Nat hiding pow_succ pow_zero +open Polynomial BigOperators Finset Finset.Nat + +theorem trunc_trunc_of_le {n m} (f : R⟦X⟧) (hnm : n ≤ m := by rfl) : + trunc n ↑(trunc m f) = trunc n f := by + ext d + rw [coeff_trunc, coeff_trunc, coeff_coe] + split_ifs with h + · rw [coeff_trunc, if_pos <| lt_of_lt_of_le h hnm] + · rfl + +@[simp] theorem trunc_trunc {n} (f : R⟦X⟧) : trunc n ↑(trunc n f) = trunc n f := + trunc_trunc_of_le f + +@[simp] theorem trunc_trunc_mul {n} (f g : R ⟦X⟧) : + trunc n ((trunc n f) * g : R⟦X⟧) = trunc n (f * g) := by + ext m + rw [coeff_trunc, coeff_trunc] + split_ifs with h + · rw [coeff_mul, coeff_mul, sum_congr rfl] + intro _ hab + have ha := lt_of_le_of_lt (antidiagonal.fst_le hab) h + rw [coeff_coe, coeff_trunc, if_pos ha] + · rfl + +@[simp] theorem trunc_mul_trunc {n} (f g : R ⟦X⟧) : + trunc n (f * (trunc n g) : R⟦X⟧) = trunc n (f * g) := by + rw [mul_comm, trunc_trunc_mul, mul_comm] + +theorem trunc_trunc_mul_trunc {n} (f g : R⟦X⟧) : + trunc n (trunc n f * trunc n g : R⟦X⟧) = trunc n (f * g) := by + rw [trunc_trunc_mul, trunc_mul_trunc] + +@[simp] theorem trunc_trunc_pow (f : R⟦X⟧) (n a : ℕ) : + trunc n ((trunc n f : R⟦X⟧) ^ a) = trunc n (f ^ a) := by + induction a with + | zero => + rw [pow_zero, pow_zero] + | succ a ih => + rw [pow_succ, pow_succ, trunc_trunc_mul, ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc] + +theorem trunc_coe_eq_self {n} {f : R[X]} (hn : natDegree f < n) : trunc n (f : R⟦X⟧) = f := by + rw [← Polynomial.coe_inj] + ext m + rw [coeff_coe, coeff_trunc] + split + case inl h => rfl + case inr h => + rw [not_lt] at h + rw [coeff_coe]; symm + exact coeff_eq_zero_of_natDegree_lt <| lt_of_lt_of_le hn h + +/-- The function `coeff n : R⟦X⟧ → R` is continuous. I.e. `coeff n f` depends only on a sufficiently +long truncation of the power series `f`.-/ +theorem coeff_coe_trunc_of_lt {n m} {f : R⟦X⟧} (h : n < m) : + coeff R n (trunc m f) = coeff R n f := by + rwa [coeff_coe, coeff_trunc, if_pos] + +/-- The `n`-th coefficient of `f*g` may be calculated +from the truncations of `f` and `g`.-/ +theorem coeff_mul_eq_coeff_trunc_mul_trunc₂ {n a b} (f g) (ha : n < a) (hb : n < b) : + coeff R n (f * g) = coeff R n (trunc a f * trunc b g) := by + symm + rw [← coeff_coe_trunc_of_lt n.lt_succ_self, ← trunc_trunc_mul_trunc, trunc_trunc_of_le f ha, + trunc_trunc_of_le g hb, trunc_trunc_mul_trunc, coeff_coe_trunc_of_lt n.lt_succ_self] + +theorem coeff_mul_eq_coeff_trunc_mul_trunc {d n} (f g) (h : d < n) : + coeff R d (f * g) = coeff R d (trunc n f * trunc n g) := + coeff_mul_eq_coeff_trunc_mul_trunc₂ f g h h + +end Trunc + +end PowerSeries + +end