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 ([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, PowerSeries.IsWeierstrassDivision.unique: q and r in the Weierstrass division are 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 its image 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.

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

• PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient: a Weierstrass factorization g = f * h induces a natural isomorphism A[X] / (f) ≃ₐ[A] A⟦X⟧ / (g).

• PowerSeries.algEquivQuotientWeierstrassDistinguished: if g is a power series over a complete local ring, such that its image in the residue field is not zero, then there is a natural isomorphism A[X] / (f) ≃ₐ[A] A⟦X⟧ / (g) where f is PowerSeries.weierstrassDistinguished g.

References

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

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

theorem PowerSeries.IsWeierstrassDivisionAt.add {A : Type u_1} [CommRing A] {f g q : PowerSeries A} {r : Polynomial A} {I : Ideal A} {f' q' : PowerSeries A} {r' : Polynomial A} (H : f.IsWeierstrassDivisionAt g q r I) (H' : f'.IsWeierstrassDivisionAt g q' r' I) : (f + f').IsWeierstrassDivisionAt g (q + q') (r + r') I

theorem PowerSeries.IsWeierstrassDivisionAt.smul {A : Type u_1} [CommRing A] {f g q : PowerSeries A} {r : Polynomial A} {I : Ideal A} (H : f.IsWeierstrassDivisionAt g q r I) (a : A) : (a • f).IsWeierstrassDivisionAt g (a • q) (a • 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 : ℕ} (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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem PowerSeries.IsWeierstrassDivisorAt.mod_add {A : Type u_1} [CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) (f f' : PowerSeries A) [IsAdicComplete I 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) (a : A) (f : PowerSeries A) [IsAdicComplete I 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 map PowerSeries.IsWeierstrassDivisorAt.mod induces a linear map A⟦X⟧ / (g) →ₗ[A] A[X].

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.div_coe_eq_zero {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.div ↑r = 0

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] 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 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 ([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] (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

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

Alias of PowerSeries.weierstrassDiv_zero_right.

@[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.weierstrassMod_zero {A : Type u_1} [CommRing A] [IsLocalRing A] (f : PowerSeries A) [IsPrecomplete (IsLocalRing.maximalIdeal A) A] : f %ʷ 0 = 0

Alias of PowerSeries.weierstrassMod_zero_right.

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.add_weierstrassDiv {A : Type u_1} [CommRing A] [IsLocalRing A] (f f' g : PowerSeries A) [IsAdicComplete (IsLocalRing.maximalIdeal A) A] : (f + f') /ʷ g = f /ʷ g + f' /ʷ g

@[simp]

theorem PowerSeries.smul_weierstrassDiv {A : Type u_1} [CommRing A] [IsLocalRing A] (a : A) (f g : PowerSeries A) [IsAdicComplete (IsLocalRing.maximalIdeal A) A] : a • f /ʷ g = a • (f /ʷ g)

@[simp]

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

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

Alias of PowerSeries.weierstrassDiv_zero_left.

@[simp]

theorem PowerSeries.add_weierstrassMod {A : Type u_1} [CommRing A] [IsLocalRing A] (f f' g : PowerSeries A) [IsAdicComplete (IsLocalRing.maximalIdeal A) A] : (f + f') %ʷ g = f %ʷ g + f' %ʷ g

@[simp]

theorem PowerSeries.smul_weierstrassMod {A : Type u_1} [CommRing A] [IsLocalRing A] (a : A) (f g : PowerSeries A) [IsAdicComplete (IsLocalRing.maximalIdeal A) A] : a • f %ʷ g = a • (f %ʷ g)

@[simp]

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

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

Alias of PowerSeries.weierstrassMod_zero_left.

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 distinguished 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

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

If g = f * h is a Weierstrass factorization, then there is a natural isomorphism A[X] / (f) ≃ₐ[A] A⟦X⟧ / (g).

Equations

• H.algEquivQuotient = ⋯.algEquivQuotient.trans (Ideal.quotientEquivAlgOfEq A ⋯)

@[simp]

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

@[simp]

theorem PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply {A : Type u_1} [CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassFactorizationAt f h I) [IsAdicComplete I A] (x : PowerSeries A ⧸ Ideal.span {g}) : H.algEquivQuotient.symm x = (Ideal.Quotient.mk (Ideal.span {f})) (⋯.mod' ((Ideal.quotientEquivAlgOfEq A ⋯) x))

theorem PowerSeries.IsWeierstrassFactorizationAt.mul {A : Type u_1} [CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassFactorizationAt f h I) {g' : PowerSeries A} {f' : Polynomial A} {h' : PowerSeries A} (H' : g'.IsWeierstrassFactorizationAt f' h' I) : (g * g').IsWeierstrassFactorizationAt (f * f') (h * h') I

theorem PowerSeries.IsWeierstrassFactorizationAt.smul {A : Type u_1} [CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassFactorizationAt f h I) {a : A} (ha : IsUnit a) : (a • g).IsWeierstrassFactorizationAt f (a • h) I

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.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.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 its image 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

• 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 the Weierstrass 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)

@[reducible, inline]

noncomputable abbrev PowerSeries.algEquivQuotientWeierstrassDistinguished {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 ⧸ Ideal.span {g.weierstrassDistinguished hg}) ≃ₐ[A] PowerSeries A ⧸ Ideal.span {g}

If g is a power series over a complete local ring, such that its image in the residue field is not zero, then there is a natural isomorphism A[X] / (f) ≃ₐ[A] A⟦X⟧ / (g) where f is PowerSeries.weierstrassDistinguished g.

Equations

• PowerSeries.algEquivQuotientWeierstrassDistinguished hg = PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient ⋯

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.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 = g.weierstrassDistinguished hg ∧ h = g.weierstrassUnit hg

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

@[simp]

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

@[simp]

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

@[simp]

theorem PowerSeries.weierstrassDistinguished_smul {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] {a : A} {g : PowerSeries A} (hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0) : (a • g).weierstrassDistinguished hg = g.weierstrassDistinguished ⋯

@[simp]

theorem PowerSeries.weierstrassUnit_smul {A : Type u_1} [CommRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] {a : A} {g : PowerSeries A} (hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0) : (a • g).weierstrassUnit hg = a • g.weierstrassUnit ⋯