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 one maximal ideal, and hence it is a complete local ring.

Main definitions

• PowerSeries.IsWeierstrassDivisionAt f g q r I: let f and g be power series over A, I be an ideal of A, this 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).

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

• PowerSeries.IsWeierstrassDivisorAt g I: let g be a power series over A, I be an ideal of A, this 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 A 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: for a power series g over A and an ideal I of A, this is a Prop which asserts that f is a distinguished polynomial at I, h is a formal power series over A that is a unit and such that 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 ([Was97], 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, PowerSeries.IsWeierstrassDivision.unique: q and r in the Weierstrass division are unique.

• PowerSeries.exists_isWeierstrassFactorization: Weierstrass preparation theorem ([Was97], 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, PowerSeries.IsWeierstrassFactorization.unique: f and h in Weierstrass preparation theorem are unique.

References

• Washington, Lawrence C. Introduction to cyclotomic fields.

Weierstrass division

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

Let f, g be power series over A, I be an ideal of A, 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).

• degree_lt : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
• eq_mul_add : f = g * q + ↑r

theorem PowerSeries.isWeierstrassDivisionAt_iff {A : Type u_1} [CommRing A] (f g q : PowerSeries A) (r : Polynomial A) (I : Ideal A) : f.IsWeierstrassDivisionAt g q r I ↔ r.degree < ↑((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 : ℕ} (hi : 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 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 : ℕ} (hi : 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.

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

Weierstrass division ([Was97], 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] (f g : PowerSeries A) [IsPrecomplete (IsLocalRing.maximalIdeal A) A] : PowerSeries A

The quotient q in Weierstrass 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 PowerSeries.IsWeierstrassDivisorAt.div ⋯ f else 0

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

The remainder r in Weierstrass 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 PowerSeries.IsWeierstrassDivisorAt.mod ⋯ f else 0

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

The quotient q in Weierstrass 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 remainder r in Weierstrass 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] (f : PowerSeries A) [IsPrecomplete (IsLocalRing.maximalIdeal A) A] : f /ʷ 0 = 0

@[simp]

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

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

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

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

theorem PowerSeries.IsWeierstrassDivision.elim {A : Type u_1} [CommRing A] [IsLocalRing A] {f g : PowerSeries A} (hg : (map (IsLocalRing.residue A)) g ≠ 0) [IsHausdorff (IsLocalRing.maximalIdeal A) A] {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 quotient q and the remainder r in the Weierstrass division are unique.

This result is stated using two PowerSeries.IsWeierstrassDivision assertions, and only requires the ring being Hausdorff with respect to the maximal ideal. If you want q and r equal to f /ʷ g and f %ʷ g, use PowerSeries.IsWeierstrassDivision.unique instead, which requires the ring being complete with respect to the maximal ideal.

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

If q and r are quotient and remainder in the Weierstrass division 0 / g, then they are equal to 0.

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

If q and r are quotient and remainder in the Weierstrass division f / g, then they are 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_coe_lift_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.lift ⋯)

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_coe_lift_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.lift ⋯)

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 ([Was97], 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 the Weierstrass preparation theorem.

Equations

• PowerSeries.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 the Weierstrass preparation theorem.

Equations

• PowerSeries.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 (weierstrassDistinguished hg) (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) : (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 (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 = ↑(weierstrassDistinguished hg) * 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 the Weierstrass preparation theorem are unique.

This result is stated using two PowerSeries.IsWeierstrassFactorization assertions, and only requires the ring being Hausdorff with respect to the maximal ideal. If you want f and h equal to PowerSeries.weierstrassDistinguished and PowerSeries.weierstrassUnit, use PowerSeries.IsWeierstrassFactorization.unique instead, which requires the ring being complete with respect to the maximal ideal.

theorem PowerSeries.IsWeierstrassFactorization.unique {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 = weierstrassDistinguished hg ∧ h = weierstrassUnit hg

The f and h in Weierstrass preparation theorem are equal to PowerSeries.weierstrassDistinguished and PowerSeries.weierstrassUnit.