Lemmas about ideals of MvPowerSeries

Main results

• MvPowerSeries.mem_map_C_iff_of_FG
• MvPowerSeries.ker_map
• MvPowerSeries.ker_mapAlgHom

theorem MvPowerSeries.coeff_mem_of_mem_map_C {R : Type u_1} {σ : Type u_3} [CommRing R] {I : Ideal R} {p : MvPowerSeries σ R} (h : p ∈ Ideal.map C I) (m : σ →₀ ℕ) : (coeff m) p ∈ I

theorem MvPowerSeries.mem_map_C_of_forall_coeff_mem {R : Type u_1} {σ : Type u_3} [CommRing R] {I : Ideal R} {p : MvPowerSeries σ R} (hI : I.FG) (hf : ∀ (m : σ →₀ ℕ), (coeff m) p ∈ I) : p ∈ Ideal.map C I

If every coefficient of f lies in I, and I is finitely generated, then f ∈ I.map C.

theorem MvPowerSeries.mem_map_C_iff_of_fg {R : Type u_1} {σ : Type u_3} [CommRing R] {I : Ideal R} {p : MvPowerSeries σ R} (hI : I.FG) : p ∈ Ideal.map C I ↔ ∀ (m : σ →₀ ℕ), (coeff m) p ∈ I

Suppose that I is finitely generated, then the push-forward of an ideal I of R to MvPowerSeries σ R via inclusion is exactly the set of power series whose coefficients are in I.

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

theorem MvPowerSeries.ker_mapAlgHom_of_fg {R : Type u_1} {σ : Type u_3} [CommRing R] {S₁ : Type u_4} {S₂ : Type u_5} [CommRing S₁] [CommRing S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) (hf : (RingHom.ker f).FG) : RingHom.ker (mapAlgHom f) = Ideal.map C (RingHom.ker f)