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 (TODO) 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.

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₂.

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)