I-Primary Components of modules

Let A be a commutative ring and I, an ideal of A. Given an A-Module M it's I-primary component is defined as $$M(I) := \bigcup_{i : \mathbb{N}} \text{torsionBySet A M } I ^ i.$$

For P : HeightOneSpectrum A, the main result of this file is that $$M \cong \bigoplus_{P} M(P).$$

Main definitions

• Ideal.primaryComponent : The I-primary component of an A-module M.

def Ideal.primaryComponent {A : Type u_1} (M : Type u_2) [CommRing A] (I : Ideal A) [AddCommMonoid M] [Module A M] : Submodule A M

The I-primaryComponent component of a module M where I is an ideal of A.

Equations

• Ideal.primaryComponent M I = ⨆ (i : ℕ), Submodule.torsionBySet A M ↑(I ^ i)

theorem Ideal.primaryComponent_mem {A : Type u_1} (M : Type u_2) [CommRing A] (I : Ideal A) [AddCommMonoid M] [Module A M] (x : M) : x ∈ primaryComponent M I ↔ ∃ (n : ℕ), x ∈ Submodule.torsionBySet A M ↑(I ^ n)

theorem Ideal.primaryComponent_map_mem {A : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing A] (I : Ideal A) [AddCommMonoid M₁] [AddCommMonoid M₂] [Module A M₁] [Module A M₂] (φ : M₁ →ₗ[A] M₂) (c : ↥(primaryComponent M₁ I)) : φ ↑c ∈ primaryComponent M₂ I

def Ideal.primaryComponent.map {A : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing A] (I : Ideal A) [AddCommMonoid M₁] [AddCommMonoid M₂] [Module A M₁] [Module A M₂] (φ : M₁ →ₗ[A] M₂) : ↥(primaryComponent M₁ I) →ₗ[A] ↥(primaryComponent M₂ I)

Given an A-linear map between M₁ and M₂, primaryComponent.map is the restriction to the I-primaryComponent components of M₁ and M₂.

Equations

• Ideal.primaryComponent.map I φ = LinearMap.codRestrict (Ideal.primaryComponent M₂ I) (φ.domRestrict (Ideal.primaryComponent M₁ I)) ⋯

@[simp]

theorem Ideal.primaryComponent.map_apply_coe {A : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing A] (I : Ideal A) [AddCommMonoid M₁] [AddCommMonoid M₂] [Module A M₁] [Module A M₂] (φ : M₁ →ₗ[A] M₂) (c : ↥(primaryComponent M₁ I)) : ↑((map I φ) c) = φ ↑c

theorem Ideal.primaryComponent.map_ker_eq {A : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing A] (I : Ideal A) [AddCommMonoid M₁] [AddCommMonoid M₂] [Module A M₁] [Module A M₂] (φ : M₁ →ₗ[A] M₂) : Submodule.map (primaryComponent M₁ I).subtype (map I φ).ker = Submodule.map φ.ker.subtype (primaryComponent (↥φ.ker) I)

theorem Ideal.primaryComponent_torsionBySet_eq_inf {A : Type u_1} (M : Type u_2) [CommRing A] [AddCommMonoid M] [Module A M] (I : Ideal A) : Submodule.map (Submodule.torsionBySet A M ↑I).subtype (primaryComponent (↥(Submodule.torsionBySet A M ↑I)) I) = primaryComponent M I ⊓ Submodule.torsionBySet A M ↑I

theorem Ideal.primaryComponent_torsionBySet_of_isCoprime {A : Type u_1} (M : Type u_2) [CommRing A] (I : Ideal A) [AddCommMonoid M] [Module A M] (J : Ideal A) (hD : IsCoprime I J) : primaryComponent (↥(Submodule.torsionBySet A M ↑J)) I = ⊥

theorem Ideal.primaryComponent_sup {A : Type u_1} {M : Type u_2} [CommRing A] (I : Ideal A) [AddCommGroup M] [Module A M] (N₁ N₂ : Submodule A M) (hD : Disjoint N₁ N₂) : Submodule.map (N₁ ⊔ N₂).subtype (primaryComponent (↥(N₁ ⊔ N₂)) I) = Submodule.map N₁.subtype (primaryComponent (↥N₁) I) ⊔ Submodule.map N₂.subtype (primaryComponent (↥N₂) I)

theorem Ideal.iSup_primaryComponent_eq_top {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] [IsDedekindDomain A] (h : Module.IsTorsion A M) : ⨆ (P : IsDedekindDomain.HeightOneSpectrum A), primaryComponent M P.asIdeal = ⊤

theorem Ideal.iSupIndep_primaryComponent (A : Type u_1) (M : Type u_2) [CommRing A] [AddCommGroup M] [Module A M] [IsDedekindDomain A] : iSupIndep fun (P : IsDedekindDomain.HeightOneSpectrum A) => primaryComponent M P.asIdeal

theorem Ideal.primaryComponent.map_surjective {A : Type u_1} [CommRing A] [IsDedekindDomain A] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (hM₁ : Module.IsTorsion A M₁) (P : IsDedekindDomain.HeightOneSpectrum A) (φ : M₁ →ₗ[A] M₂) (hf : Function.Surjective ⇑φ) : Function.Surjective ⇑(map P.asIdeal φ)