Weierstrass preparation theorem for power series over a complete local ring

In this file we define Weierstrass division, Weierstrass factorization, and prove Weierstrass preparation theorem.

We assume that a ring is adic complete with respect to some ideal. If such ideal is a maximal ideal, then by isLocalRing_of_isAdicComplete_maximal, such ring has only on maximal ideal, and hence such ring is a complete local ring.

Main definitions

• PowerSeries.IsWeierstrassDivisionAt f g q r I: a Prop which asserts that a power series q and a polynomial r of degree < n satisfy f = g * q + r, where n is the order of the image of g in (A / I)⟦X⟧ (defined to be zero if such image is zero, in which case it's mathematically not considered).

• PowerSeries.IsWeierstrassDivision: version of PowerSeries.IsWeierstrassDivisionAt for local rings with respect to its maximal ideal.

• PowerSeries.IsWeierstrassDivisorAt g I: a Prop which asserts that the n-th coefficient of g is a unit, where n is the order of the image of g in (A / I)⟦X⟧ (defined to be zero if such image is zero, in which case it's mathematically not considered).

  This property guarantees that if the ring is I-adic complete, then g can be used as a divisor in Weierstrass division (PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod).

• PowerSeries.IsWeierstrassDivisor: version of PowerSeries.IsWeierstrassDivisorAt for local rings with respect to its maximal ideal.

• PowerSeries.IsWeierstrassFactorizationAt g f h I: a Prop which asserts that f is a distingushed polynomial at I, h is a formal power series over A which a unit, such that the formal power series g satisfies g = f * h.

• PowerSeries.IsWeierstrassFactorization: version of PowerSeries.IsWeierstrassFactorizationAt for local rings with respect to its maximal ideal.

Main results

• PowerSeries.exists_isWeierstrassDivision: Weierstrass division ([washington_cyclotomic], Proposition 7.2): let f, g be power series over a complete local ring, such that the image of g in the residue field is not zero. Let n be the order of the image of g in the residue field. Then there exists a power series q and a polynomial r of degree < n, such that f = g * q + r.

• PowerSeries.IsWeierstrassDivision.elim: The q and r in the Weierstrass division is unique.

• PowerSeries.exists_isWeierstrassFactorization: Weierstrass preparation theorem ([washington_cyclotomic], Theorem 7.3): let g be a power series over a complete local ring, such that the image of g in the residue field is not zero. Then there exists a distinguished polynomial f and a power series h which is a unit, such that g = f * h.

• PowerSeries.IsWeierstrassFactorization.elim: The f and h in Werierstrass preparation theorem is unique.

• Polynomial.IsDistinguishedAt.algEquivQuotient: a distinguished polynomial g induces a natural isomorphism A[X] / (g) ≃ A⟦X⟧ / (g).

References

• [Washington, Lawrence C. Introduction to cyclotomic fields.][washington_cyclotomic]

Results should be added to mathlib

theorem ENat.lift_eq_toNat_of_lt_top {x : ℕ∞} (hx : x < ⊤) : x.lift hx = x.toNat

theorem PowerSeries.eq_shift_mul_X_pow_add_trunc {A : Type u_1} [Semiring A] (n : ℕ) (f : PowerSeries A) : f = (mk fun (i : ℕ) => (coeff A (i + n)) f) * X ^ n + ↑(trunc n f)

theorem PowerSeries.eq_X_pow_mul_shift_add_trunc {A : Type u_1} [Semiring A] (n : ℕ) (f : PowerSeries A) : f = (X ^ n * mk fun (i : ℕ) => (coeff A (i + n)) f) + ↑(trunc n f)

theorem PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal {A : Type u_1} [Semiring A] {I J : Ideal A} {f g : PowerSeries A} (n : ℕ) (hf : ∀ i ≤ n, (coeff A i) f ∈ I) (hg : ∀ i ≤ n, (coeff A i) g ∈ J) (i : ℕ) : i ≤ n → (coeff A i) (f * g) ∈ I * J

theorem PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' {A : Type u_1} [Semiring A] {I J : Ideal A} {f g : PowerSeries A} (hf : ∀ (i : ℕ), (coeff A i) f ∈ I) (hg : ∀ (i : ℕ), (coeff A i) g ∈ J) (i : ℕ) : (coeff A i) (f * g) ∈ I * J

theorem PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal {A : Type u_1} [Semiring A] {I : Ideal A} {f g : PowerSeries A} (n : ℕ) (hg : ∀ i ≤ n, (coeff A i) g ∈ I) (i : ℕ) : i ≤ n → (coeff A i) (f * g) ∈ I

theorem PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal' {A : Type u_1} [Semiring A] {I : Ideal A} {f g : PowerSeries A} (hg : ∀ (i : ℕ), (coeff A i) g ∈ I) (i : ℕ) : (coeff A i) (f * g) ∈ I

theorem PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal {A : Type u_1} [Semiring A] {I : Ideal A} {f g : PowerSeries A} (n : ℕ) [I.IsTwoSided] (hf : ∀ i ≤ n, (coeff A i) f ∈ I) (i : ℕ) : i ≤ n → (coeff A i) (f * g) ∈ I

theorem PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal' {A : Type u_1} [Semiring A] {I : Ideal A} {f g : PowerSeries A} [I.IsTwoSided] (hf : ∀ (i : ℕ), (coeff A i) f ∈ I) (i : ℕ) : (coeff A i) (f * g) ∈ I

Weierstrass division

def PowerSeries.IsWeierstrassDivisionAt {A : Type u_1} [CommRing A] (f g q : PowerSeries A) (r : Polynomial A) (I : Ideal A) : Prop

PowerSeries.IsWeierstrassDivisionAt f g q r I is a Prop which asserts that a power series q and a polynomial r of degree < n satisfy f = g * q + r, where n is the order of the image of g in (A / I)⟦X⟧ (defined to be zero if such image is zero, in which case it's mathematically not considered).

Equations

• f.IsWeierstrassDivisionAt g q r I = (r.degree < ↑((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat ∧ f = g * q + ↑r)

@[reducible, inline]

abbrev PowerSeries.IsWeierstrassDivision {A : Type u_1} [CommRing A] (f g q : PowerSeries A) (r : Polynomial A) [IsLocalRing A] : Prop

Version of PowerSeries.IsWeierstrassDivisionAt for local rings with respect to its maximal ideal.

Equations

• f.IsWeierstrassDivision g q r = f.IsWeierstrassDivisionAt g q r (IsLocalRing.maximalIdeal A)

theorem PowerSeries.isWeierstrassDivisionAt_zero {A : Type u_1} [CommRing A] (g : PowerSeries A) (I : Ideal A) : IsWeierstrassDivisionAt 0 g 0 0 I

theorem PowerSeries.IsWeierstrassDivisionAt.coeff_f_sub_r_mem {A : Type u_1} [CommRing A] {f g q : PowerSeries A} {r : Polynomial A} {I : Ideal A} (H : f.IsWeierstrassDivisionAt g q r I) (i : ℕ) : i < ((map (Ideal.Quotient.mk I)) g).order.toNat → (coeff A i) (f - ↑r) ∈ I

def PowerSeries.IsWeierstrassDivisorAt {A : Type u_1} [CommRing A] (g : PowerSeries A) (I : Ideal A) : Prop

PowerSeries.IsWeierstrassDivisorAt g I is a Prop which asserts that the n-th coefficient of g is a unit, where n is the order of the image of g in (A / I)⟦X⟧ (defined to be zero if such image is zero, in which case it's mathematically not considered).

This property guarantees that if the ring is I-adic complete, then g can be used as a divisor in Weierstrass division (PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod).

Equations

• g.IsWeierstrassDivisorAt I = IsUnit ((PowerSeries.coeff A ((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat) g)

@[reducible, inline]

abbrev PowerSeries.IsWeierstrassDivisor {A : Type u_1} [CommRing A] (g : PowerSeries A) [IsLocalRing A] : Prop

Version of PowerSeries.IsWeierstrassDivisorAt for local rings with respect to its maximal ideal.

Equations

• g.IsWeierstrassDivisor = g.IsWeierstrassDivisorAt (IsLocalRing.maximalIdeal A)

theorem PowerSeries.IsWeierstrassDivisor.of_map_ne_zero {A : Type u_1} [CommRing A] (g : PowerSeries A) [IsLocalRing A] (hg : (map (IsLocalRing.residue A)) g ≠ 0) : g.IsWeierstrassDivisor

If g is a power series over a local ring such that its image in the residue field is not zero, then g can be used as a Weierstrass divisor.

theorem Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt {A : Type u_1} [CommRing A] {g : Polynomial A} {I : Ideal A} (H : g.IsDistinguishedAt I) (hI : I ≠ ⊤) : (↑g).IsWeierstrassDivisorAt I

theorem Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt' {A : Type u_1} [CommRing A] {g : Polynomial A} {I : Ideal A} (H : g.IsDistinguishedAt I) [IsHausdorff I A] : (↑g).IsWeierstrassDivisorAt I

theorem PowerSeries.IsWeierstrassDivisorAt.isUnit_shift {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) : IsUnit (mk fun (i : ℕ) => (coeff A (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g)

noncomputable def PowerSeries.IsWeierstrassDivisorAt.seq {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) (f : PowerSeries A) : ℕ → PowerSeries A

The inductively constructed sequence qₖ in the proof of Weierstrass division.

Equations

• H.seq f 0 = 0
• H.seq f k.succ = H.seq f k + (PowerSeries.mk fun (i : ℕ) => (PowerSeries.coeff A (i + ((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat)) (f - g * H.seq f k)) * ↑⋯.unit⁻¹

theorem PowerSeries.IsWeierstrassDivisorAt.coeff_seq_mem {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) {f : PowerSeries A} (k i : ℕ) : i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat → (coeff A i) (f - g * H.seq f k) ∈ I ^ k

theorem PowerSeries.IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) {f : PowerSeries A} (k i : ℕ) : (coeff A i) (H.seq f (k + 1) - H.seq f k) ∈ I ^ k

@[simp]

theorem PowerSeries.IsWeierstrassDivisorAt.seq_zero {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) {f : PowerSeries A} : H.seq f 0 = 0

theorem PowerSeries.IsWeierstrassDivisorAt.seq_one {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) {f : PowerSeries A} : H.seq f 1 = (mk fun (i : ℕ) => (coeff A (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) f) * ↑⋯.unit⁻¹

noncomputable def PowerSeries.IsWeierstrassDivisorAt.divCoeff {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) (f : PowerSeries A) [IsPrecomplete I A] (i : ℕ) : { x : A // ∀ (n : ℕ), (fun (k : ℕ) => (coeff A i) (H.seq f k)) n ≡ x [SMOD I ^ n • ⊤] }

The (bundled version of) coefficient of the limit q of the inductively constructed sequence qₖ in the proof of Weierstrass division.

Equations

• H.divCoeff f i = Classical.indefiniteDescription (fun (x : A) => ∀ (n : ℕ), (fun (k : ℕ) => (PowerSeries.coeff A i) (H.seq f k)) n ≡ x [SMOD I ^ n • ⊤]) ⋯

noncomputable def PowerSeries.IsWeierstrassDivisorAt.div {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) (f : PowerSeries A) [IsPrecomplete I A] : PowerSeries A

The limit q of the inductively constructed sequence qₖ in the proof of Weierstrass division.

Equations

• H.div f = PowerSeries.mk fun (i : ℕ) => ↑(H.divCoeff f i)

theorem PowerSeries.IsWeierstrassDivisorAt.coeff_div {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) {f : PowerSeries A} [IsPrecomplete I A] (i : ℕ) : (coeff A i) (H.div f) = ↑(H.divCoeff f i)

theorem PowerSeries.IsWeierstrassDivisorAt.coeff_div_sub_seq_mem {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) {f : PowerSeries A} [IsPrecomplete I A] (k i : ℕ) : (coeff A i) (H.div f - H.seq f k) ∈ I ^ k

noncomputable def PowerSeries.IsWeierstrassDivisorAt.mod {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) (f : PowerSeries A) [IsPrecomplete I A] : Polynomial A

The remainder r in the proof of Weierstrass division.

Equations

• H.mod f = PowerSeries.trunc ((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat (f - g * H.div f)

theorem PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) (f : PowerSeries A) [IsAdicComplete I A] : f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) I

If the ring is I-adic complete, then g can be used as a divisor in Weierstrass division.

theorem PowerSeries.IsWeierstrassDivisorAt.eq_zero_of_mul_eq {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) [IsHausdorff I A] {q : PowerSeries A} {r : Polynomial A} (hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat) (heq : g * q = ↑r) : q = 0 ∧ r = 0

If g * q = r for some power series q and some polynomial r whose degree is < n, then q and r are all zero. This implies the uniqueness of Weierstrass division.

theorem PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) [IsHausdorff I A] {q q' : PowerSeries A} {r r' : Polynomial A} (hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat) (hr' : r'.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat) (heq : g * q + ↑r = g * q' + ↑r') : q = q' ∧ r = r'

If g * q + r = g * q' + r' for some power series q, q' and some polynomials r, r' whose degrees are < n, then q = q' and r = r' are all zero. This implies the uniqueness of Weierstrass division.

@[simp]

theorem PowerSeries.IsWeierstrassDivisorAt.mod_add {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) [IsAdicComplete I A] {f f' : PowerSeries A} : H.mod (f + f') = H.mod f + H.mod f'

@[simp]

theorem PowerSeries.IsWeierstrassDivisorAt.mod_smul {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) [IsAdicComplete I A] {a : A} {f : PowerSeries A} : H.mod (a • f) = a • H.mod f

@[simp]

theorem PowerSeries.IsWeierstrassDivisorAt.mod_zero {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) [IsAdicComplete I A] : H.mod 0 = 0

noncomputable def PowerSeries.IsWeierstrassDivisorAt.mod' {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) [IsAdicComplete I A] : PowerSeries A ⧸ Ideal.span {g} →ₗ[A] Polynomial A

The remainder is invariant under multiples of g.

Equations

• H.mod' = { toFun := Quotient.lift (fun (f : PowerSeries A) => H.mod f) ⋯, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) [IsAdicComplete I A] {f : PowerSeries A} : H.mod' ((Ideal.Quotient.mk (Ideal.span {g})) f) = H.mod f

theorem PowerSeries.IsWeierstrassDivisorAt.mod_coe_eq_self {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) [IsAdicComplete I A] {r : Polynomial A} (hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat) : H.mod ↑r = r

@[simp]

theorem PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) [IsAdicComplete I A] {f : PowerSeries A ⧸ Ideal.span {g}} : (Ideal.Quotient.mk (Ideal.span {g})) ↑(H.mod' f) = f

noncomputable def Polynomial.IsDistinguishedAt.algEquivQuotient {A : Type u_1} [CommRing A] {g : Polynomial A} {I : Ideal A} (H : g.IsDistinguishedAt I) [IsAdicComplete I A] : (Polynomial A ⧸ Ideal.span {g}) ≃ₐ[A] PowerSeries A ⧸ Ideal.span {↑g}

A distinguished polynomial g induces a natural isomorphism A[X] / (g) ≃ A⟦X⟧ / (g).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Polynomial.IsDistinguishedAt.algEquivQuotient_apply {A : Type u_1} [CommRing A] {g : Polynomial A} {I : Ideal A} (H : g.IsDistinguishedAt I) [IsAdicComplete I A] (a✝ : Polynomial A ⧸ Ideal.span {g}) : H.algEquivQuotient a✝ = (Ideal.quotientMapₐ (Ideal.span {↑g}) (coeToPowerSeries.algHom A) ⋯) a✝

@[simp]

theorem Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply {A : Type u_1} [CommRing A] {g : Polynomial A} {I : Ideal A} (H : g.IsDistinguishedAt I) [IsAdicComplete I A] (a✝ : PowerSeries A ⧸ Ideal.span {↑g}) : H.algEquivQuotient.symm a✝ = (Ideal.Quotient.mk (Ideal.span {g})) (⋯.mod' a✝)

theorem Polynomial.IsDistinguishedAt.algEquivQuotient_mk {A : Type u_1} [CommRing A] {g : Polynomial A} {I : Ideal A} (H : g.IsDistinguishedAt I) [IsAdicComplete I A] (f : Polynomial A) : H.algEquivQuotient ((Ideal.Quotient.mk (Ideal.span {g})) f) = (Ideal.Quotient.mk (Ideal.span {↑g})) ↑f

theorem Polynomial.IsDistinguishedAt.algEquivQuotient_symm_mk {A : Type u_1} [CommRing A] {g : Polynomial A} {I : Ideal A} (H : g.IsDistinguishedAt I) [IsAdicComplete I A] (f : PowerSeries A) : H.algEquivQuotient.symm ((Ideal.Quotient.mk (Ideal.span {↑g})) f) = (Ideal.Quotient.mk (Ideal.span {g})) (⋯.mod f)

theorem PowerSeries.exists_isWeierstrassDivision {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (f g : PowerSeries A) (hg : (map (IsLocalRing.residue A)) g ≠ 0) : ∃ (q : PowerSeries A) (r : Polynomial A), f.IsWeierstrassDivision g q r

Weierstrass division ([washington_cyclotomic], Proposition 7.2): let f, g be power series over a complete local ring, such that the image of g in the residue field is not zero. Let n be the order of the image of g in the residue field. Then there exists a power series q and a polynomial r of degree < n, such that f = g * q + r.

noncomputable def PowerSeries.weierstrassDiv {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (f g : PowerSeries A) : PowerSeries A

The q in Werierstrass division, denoted by f /ʷ g. Note that when the image of g in the residue field is zero, this is defined to be zero.

Equations

• f /ʷ g = if hg : (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 then ⋯.choose else 0

noncomputable def PowerSeries.weierstrassMod {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (f g : PowerSeries A) : Polynomial A

The r in Werierstrass division, denoted by f %ʷ g. Note that when the image of g in the residue field is zero, this is defined to be zero.

Equations

• f %ʷ g = if hg : (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 then ⋯.choose else 0

def PowerSeries.«term_/ʷ_» : Lean.TrailingParserDescr

The q in Werierstrass division, denoted by f /ʷ g. Note that when the image of g in the residue field is zero, this is defined to be zero.

Equations

• PowerSeries.«term_/ʷ_» = Lean.ParserDescr.trailingNode `PowerSeries.«term_/ʷ_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " /ʷ ") (Lean.ParserDescr.cat `term 71))

def PowerSeries.«term_%ʷ_» : Lean.TrailingParserDescr

The r in Werierstrass division, denoted by f %ʷ g. Note that when the image of g in the residue field is zero, this is defined to be zero.

Equations

• PowerSeries.«term_%ʷ_» = Lean.ParserDescr.trailingNode `PowerSeries.«term_%ʷ_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " %ʷ ") (Lean.ParserDescr.cat `term 71))

@[simp]

theorem PowerSeries.weierstrassDiv_zero_right {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (f : PowerSeries A) : f /ʷ 0 = 0

@[simp]

theorem PowerSeries.weierstrassMod_zero_right {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (f : PowerSeries A) : f %ʷ 0 = 0

theorem PowerSeries.degree_weierstrassMod_lt {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (f g : PowerSeries A) : (f %ʷ g).degree < ↑((map (IsLocalRing.residue A)) g).order.toNat

theorem PowerSeries.isWeierstrassDivision_weierstrassDiv_weierstrassMod {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (f g : PowerSeries A) (hg : (map (IsLocalRing.residue A)) g ≠ 0) : f.IsWeierstrassDivision g (f /ʷ g) (f %ʷ g)

theorem PowerSeries.eq_mul_weierstrassDiv_add_weierstrassMod {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (f g : PowerSeries A) (hg : (map (IsLocalRing.residue A)) g ≠ 0) : f = g * (f /ʷ g) + ↑(f %ʷ g)

theorem PowerSeries.eq_zero_of_weierstrass_division {A : Type u_1} [CommRing A] [IsLocalRing A] [IsHausdorff (IsLocalRing.maximalIdeal A) A] (g : PowerSeries A) (hg : (map (IsLocalRing.residue A)) g ≠ 0) {q : PowerSeries A} {r : Polynomial A} (hr : r.degree < ↑((map (IsLocalRing.residue A)) g).order.toNat) (heq : g * q = ↑r) : q = 0 ∧ r = 0

The q and r in the Weierstrass division for 0 is equal to 0.

theorem PowerSeries.eq_of_weierstrass_division {A : Type u_1} [CommRing A] [IsLocalRing A] [IsHausdorff (IsLocalRing.maximalIdeal A) A] (g : PowerSeries A) (hg : (map (IsLocalRing.residue A)) g ≠ 0) {q q' : PowerSeries A} {r r' : Polynomial A} (hr : r.degree < ↑((map (IsLocalRing.residue A)) g).order.toNat) (hr' : r'.degree < ↑((map (IsLocalRing.residue A)) g).order.toNat) (heq : g * q + ↑r = g * q' + ↑r') : q = q' ∧ r = r'

The q and r in the Weierstrass division is unique.

theorem PowerSeries.IsWeierstrassDivision.elim {A : Type u_1} [CommRing A] [IsLocalRing A] [IsHausdorff (IsLocalRing.maximalIdeal A) A] {f g : PowerSeries A} (hg : (map (IsLocalRing.residue A)) g ≠ 0) {q q' : PowerSeries A} {r r' : Polynomial A} (H : f.IsWeierstrassDivision g q r) (H2 : f.IsWeierstrassDivision g q' r') : q = q' ∧ r = r'

The q and r in the Weierstrass division is unique.

theorem PowerSeries.IsWeierstrassDivision.eq_zero {A : Type u_1} [CommRing A] [IsLocalRing A] [IsHausdorff (IsLocalRing.maximalIdeal A) A] {g : PowerSeries A} (hg : (map (IsLocalRing.residue A)) g ≠ 0) {q : PowerSeries A} {r : Polynomial A} (H : IsWeierstrassDivision 0 g q r) : q = 0 ∧ r = 0

The q and r in the Weierstrass division for 0 is equal to 0.

theorem PowerSeries.IsWeierstrassDivision.eq_weierstrassDiv_weierstrassMod {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] {f g : PowerSeries A} (hg : (map (IsLocalRing.residue A)) g ≠ 0) {q : PowerSeries A} {r : Polynomial A} (H : f.IsWeierstrassDivision g q r) : q = f /ʷ g ∧ r = f %ʷ g

The q and r in the Weierstrass division is equal to f /ʷ g and f %ʷ g.

@[simp]

theorem PowerSeries.weierstrassDiv_zero_left {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (g : PowerSeries A) : 0 /ʷ g = 0

@[simp]

theorem PowerSeries.weierstrassMod_zero_left {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (g : PowerSeries A) : 0 %ʷ g = 0

Weierstrass preparation theorem

structure PowerSeries.IsWeierstrassFactorizationAt {A : Type u_1} [CommRing A] (g : PowerSeries A) (f : Polynomial A) (h : PowerSeries A) (I : Ideal A) : Prop

If f is a polynomial over A, g and h are power series over A, then PowerSeries.IsWeierstrassFactorizationAt g f h I is a Prop which asserts that f is distingushed at I, h is a unit, such that g = f * h.

• isDistinguishedAt : f.IsDistinguishedAt I
• isUnit : IsUnit h
• eq_mul : g = ↑f * h

theorem PowerSeries.isWeierstrassFactorizationAt_iff {A : Type u_1} [CommRing A] (g : PowerSeries A) (f : Polynomial A) (h : PowerSeries A) (I : Ideal A) : g.IsWeierstrassFactorizationAt f h I ↔ f.IsDistinguishedAt I ∧ IsUnit h ∧ g = ↑f * h

@[reducible, inline]

abbrev PowerSeries.IsWeierstrassFactorization {A : Type u_1} [CommRing A] (g : PowerSeries A) (f : Polynomial A) (h : PowerSeries A) [IsLocalRing A] : Prop

Version of PowerSeries.IsWeierstrassFactorizationAt for local rings with respect to its maximal ideal.

Equations

• g.IsWeierstrassFactorization f h = g.IsWeierstrassFactorizationAt f h (IsLocalRing.maximalIdeal A)

theorem PowerSeries.IsWeierstrassFactorizationAt.map_ne_zero_of_ne_top {A : Type u_1} [CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassFactorizationAt f h I) (hI : I ≠ ⊤) : (map (Ideal.Quotient.mk I)) g ≠ 0

theorem PowerSeries.IsWeierstrassFactorizationAt.degree_eq_order_map_of_ne_top {A : Type u_1} [CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassFactorizationAt f h I) (hI : I ≠ ⊤) : f.degree = ((map (Ideal.Quotient.mk I)) g).order

theorem PowerSeries.IsWeierstrassFactorizationAt.natDegree_eq_toNat_order_map_of_ne_top {A : Type u_1} [CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassFactorizationAt f h I) (hI : I ≠ ⊤) : f.natDegree = ((map (Ideal.Quotient.mk I)) g).order.toNat

theorem PowerSeries.IsWeierstrassFactorization.map_ne_zero {A : Type u_1} [CommRing A] [IsLocalRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} (H : g.IsWeierstrassFactorization f h) : (map (IsLocalRing.residue A)) g ≠ 0

theorem PowerSeries.IsWeierstrassFactorization.degree_eq_order_map {A : Type u_1} [CommRing A] [IsLocalRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} (H : g.IsWeierstrassFactorization f h) : f.degree = ((map (IsLocalRing.residue A)) g).order

theorem PowerSeries.IsWeierstrassFactorization.natDegree_eq_toNat_order_map {A : Type u_1} [CommRing A] [IsLocalRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} (H : g.IsWeierstrassFactorization f h) : f.natDegree = ((map (IsLocalRing.residue A)) g).order.toNat

theorem PowerSeries.IsWeierstrassDivision.isUnit_of_map_ne_zero {A : Type u_1} [CommRing A] [IsLocalRing A] {g q : PowerSeries A} {r : Polynomial A} (hg : (map (IsLocalRing.residue A)) g ≠ 0) (H : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r) : IsUnit q

theorem PowerSeries.IsWeierstrassDivision.isWeierstrassFactorization {A : Type u_1} [CommRing A] [IsLocalRing A] {g q : PowerSeries A} {r : Polynomial A} (hg : (map (IsLocalRing.residue A)) g ≠ 0) (H : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r) : g.IsWeierstrassFactorization (Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - r) ↑⋯.unit⁻¹

theorem PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision {A : Type u_1} [CommRing A] [IsLocalRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} (H : g.IsWeierstrassFactorization f h) : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g (↑⋯.unit⁻¹) (Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f)

theorem PowerSeries.exists_isWeierstrassFactorization {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (g : PowerSeries A) (hg : (map (IsLocalRing.residue A)) g ≠ 0) : ∃ (f : Polynomial A) (h : PowerSeries A), g.IsWeierstrassFactorization f h

Weierstrass preparation theorem ([washington_cyclotomic], Theorem 7.3): let g be a power series over a complete local ring, such that the image of g in the residue field is not zero. Then there exists a distinguished polynomial f and a power series h which is a unit, such that g = f * h.

noncomputable def PowerSeries.weierstrassDistinguished {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (g : PowerSeries A) (hg : (map (IsLocalRing.residue A)) g ≠ 0) : Polynomial A

The f in Werierstrass preparation theorem.

Equations

• g.weierstrassDistinguished hg = ⋯.choose

noncomputable def PowerSeries.weierstrassUnit {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (g : PowerSeries A) (hg : (map (IsLocalRing.residue A)) g ≠ 0) : PowerSeries A

The h in Werierstrass preparation theorem.

Equations

• g.weierstrassUnit hg = ⋯.choose

theorem PowerSeries.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (g : PowerSeries A) (hg : (map (IsLocalRing.residue A)) g ≠ 0) : g.IsWeierstrassFactorization (g.weierstrassDistinguished hg) (g.weierstrassUnit hg)

theorem PowerSeries.isDistinguishedAt_weierstrassDistinguished {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (g : PowerSeries A) (hg : (map (IsLocalRing.residue A)) g ≠ 0) : (g.weierstrassDistinguished hg).IsDistinguishedAt (IsLocalRing.maximalIdeal A)

theorem PowerSeries.isUnit_weierstrassUnit {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (g : PowerSeries A) (hg : (map (IsLocalRing.residue A)) g ≠ 0) : IsUnit (g.weierstrassUnit hg)

theorem PowerSeries.eq_weierstrassDistinguished_mul_weierstrassUnit {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (g : PowerSeries A) (hg : (map (IsLocalRing.residue A)) g ≠ 0) : g = ↑(g.weierstrassDistinguished hg) * g.weierstrassUnit hg

theorem PowerSeries.IsWeierstrassFactorization.elim {A : Type u_1} [CommRing A] [IsLocalRing A] [IsHausdorff (IsLocalRing.maximalIdeal A) A] {g : PowerSeries A} {f f' : Polynomial A} {h h' : PowerSeries A} (H : g.IsWeierstrassFactorization f h) (H2 : g.IsWeierstrassFactorization f' h') : f = f' ∧ h = h'

The f and h in Werierstrass preparation theorem is unique.

theorem PowerSeries.IsWeierstrassFactorization.eq_weierstrassDistinguished_weierstrassUnit {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} (H : g.IsWeierstrassFactorization f h) (hg : (map (IsLocalRing.residue A)) g ≠ 0) : f = g.weierstrassDistinguished hg ∧ h = g.weierstrassUnit hg

The f and h in Werierstrass preparation theorem is unique.