The kernel of the coefficientwise map of power series

For a ring homomorphism f : R →+* S with finitely generated kernel, the kernel of the induced map R⟦X⟧ →+* S⟦X⟧ is the extension of ker f along the constant embedding C. This is the one-variable form of MvPowerSeries.ker_map_of_fg.

Applied to the quotient map R → R ⧸ (r), whose kernel is principal, this identifies R⟦X⟧ ⧸ (r) with (R ⧸ (r))⟦X⟧. Hence a constant series C r is a prime element of R⟦X⟧ exactly when r is a prime element of R, as for polynomials (Polynomial.prime_C_iff). Over a local domain with a prime ϖ, a series with nonzero reduction modulo the maximal ideal is not divisible by C ϖ, so it acts injectively on R⟦X⟧ ⧸ (ϖ ^ m).

A series whose coefficients lie in an ideal J has square zero modulo any ideal containing J * J. For a finitely generated ideal I, the same kernel computation describes I.map C by its coefficients and shows that it is prime when I is.

Main results

• PowerSeries.ker_map_of_fg: ker (map f) = (ker f).map C when ker f is finitely generated.
• PowerSeries.mem_map_C_iff_of_fg, PowerSeries.isPrime_map_C_of_fg: for a finitely generated ideal I, the series in I.map C are those with all coefficients in I, and I.map C is prime when I is.
• PowerSeries.prime_C_iff: C r is prime in R⟦X⟧ if and only if r is prime in R.
• PowerSeries.torsionBy_quotient_span_C_pow_eq_bot: a series with nonzero reduction modulo the maximal ideal has no nonzero torsion on R⟦X⟧ ⧸ (ϖ ^ m) for a prime ϖ of a local domain.
• PowerSeries.sq_map_mk_eq_zero_of_coeff_mem: a series with coefficients in J squares to zero in (R ⧸ K)⟦X⟧ when J * J ≤ K.

theorem PowerSeries.ker_map_of_fg {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : (RingHom.ker f).FG) : RingHom.ker (map f) = Ideal.map C (RingHom.ker f)

If f : R →+* S has finitely generated kernel, the kernel of the coefficientwise map R⟦X⟧ →+* S⟦X⟧ is the extension of ker f along the constant embedding.

theorem PowerSeries.mem_map_C_iff_of_fg {R : Type u_1} [CommRing R] {I : Ideal R} (hI : I.FG) {f : PowerSeries R} : f ∈ Ideal.map C I ↔ ∀ (n : ℕ), (coeff n) f ∈ I

For a finitely generated ideal I, a power series lies in the extension I.map C iff all of its coefficients lie in I.

theorem PowerSeries.isPrime_map_C_of_fg {R : Type u_1} [CommRing R] {I : Ideal R} [I.IsPrime] (hI : I.FG) : (Ideal.map C I).IsPrime

The extension I.map C of a finitely generated prime ideal I of R is a prime ideal of R⟦X⟧: it is the kernel of R⟦X⟧ → (R ⧸ I)⟦X⟧, whose target is a domain.

theorem PowerSeries.prime_C_iff {R : Type u_1} [CommRing R] {r : R} : Prime (C r) ↔ Prime r

A constant power series C r is a prime element of R⟦X⟧ if and only if r is a prime element of R.

theorem PowerSeries.torsionBy_quotient_span_C_pow_eq_bot {R : Type u_1} [CommRing R] [IsDomain R] [IsLocalRing R] {ϖ : R} (hϖ : Prime ϖ) {g : PowerSeries R} (hg : (map (IsLocalRing.residue R)) g ≠ 0) (m : ℕ) : Submodule.torsionBy (PowerSeries R) (PowerSeries R ⧸ Ideal.span {C (ϖ ^ m)}) g = ⊥

Over a local domain R with a prime ϖ, a power series g with nonzero reduction modulo the maximal ideal acts injectively on R⟦X⟧ ⧸ (ϖ ^ m). In Iwasawa theory these are the vertical blocks of an elementary module.

theorem PowerSeries.sq_map_mk_eq_zero_of_coeff_mem {R : Type u_1} [CommRing R] {J K : Ideal R} (hJK : J * J ≤ K) {f : PowerSeries R} (hf : ∀ (n : ℕ), (coeff n) f ∈ J) : (map (Ideal.Quotient.mk K)) f ^ 2 = 0

A series whose coefficients lie in an ideal J squares to zero in (R ⧸ K)⟦X⟧ for any ideal K containing J * J.