Documentation

TauCeti.Algebra.Module.Torsion.PrimaryComponent

Primary components of modules #

The p-power torsion of a module over an arbitrary ring #

For a natural number p and a module M over an arbitrary, possibly noncommutative, semiring A, the elements of M killed by some power of p form an A-submodule: multiplication by p ^ n is additive, so it commutes with every scalar. As an additive submonoid it is Mathlib's p-primary component AddCommMonoid.primaryComponent M p.

Mathlib's Submodule.torsion' requires a commutative base ring. Here the ring is typically a group algebra ℤ_p[G] of a nonabelian group, whose modules — such as the p-completed units of a Galois extension of p-adic fields — have a p-power torsion that must be compared as ℤ_p[G]-modules (NSW (7.4.1)). An extension by a module without p-power torsion does not change the p-power torsion.

The primary component of an ideal #

For an ideal 𝔞 of a commutative ring R, Mathlib's Ideal.primaryComponent is the submodule Γ_𝔞(N) of elements of N killed by some power of 𝔞. This file adds two facts about it: a finitely generated submodule of Γ_𝔞(N) is killed by a single power of 𝔞, and, when 𝔞 is generated by a finite set G, an element lies in Γ_𝔞(N) exactly when each g ∈ G kills it after raising to some power.

Main definitions #

Main statements #

References #

source
def TauCeti.pPowerTorsion (p : ℕ) (A : Type u_1) [Semiring A] (M : Type u_2) [AddCommMonoid M] [Module A M] :
Submodule A M

The p-power torsion of an A-module M: the A-submodule of elements killed by some power of p. Its underlying additive submonoid is the p-primary component of M.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.mem_pPowerTorsion_iff {p : ℕ} {A : Type u_1} [Semiring A] {M : Type u_2} [AddCommMonoid M] [Module A M] {x : M} :
    x ∈ pPowerTorsion p A M ↔ ∃ (k : ℕ), p ^ k • x = 0

    An element lies in the p-power torsion exactly when some power of p kills it.

    source
    @[simp]
    theorem TauCeti.toAddSubmonoid_pPowerTorsion (p : ℕ) (A : Type u_1) [Semiring A] (M : Type u_2) [AddCommMonoid M] [Module A M] :
    (pPowerTorsion p A M).toAddSubmonoid = AddCommMonoid.primaryComponent M p

    The additive submonoid underlying the p-power torsion is the p-primary component.

    source
    theorem TauCeti.map_pPowerTorsion_of_exact {p : ℕ} {A : Type u_1} [Semiring A] {M : Type u_2} [AddCommMonoid M] [Module A M] {N : Type u_3} {P : Type u_4} [AddCommMonoid N] [Module A N] [AddCommMonoid P] [Module A P] {f : M →ₗ[A] N} {g : N →ₗ[A] P} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hP : pPowerTorsion p A P = ⊥) :
    Submodule.map f (pPowerTorsion p A M) = pPowerTorsion p A N

    In an exact sequence 0 → M → N → P whose last term has no p-power torsion, the p-power torsion of N is the image of that of M.

    source
    theorem Ideal.exists_le_torsionBySet_pow_of_le_primaryComponent {R : Type u_1} [CommRing R] {N : Type u_2} [AddCommMonoid N] [Module R N] (𝔞 : Ideal R) {P : Submodule R N} (hP : P.FG) (h : P ≤ primaryComponent N 𝔞) :
    ∃ (n : ℕ), P ≤ Submodule.torsionBySet R N ↑(𝔞 ^ n)

    A finitely generated submodule of the 𝔞-primary component is killed by a single power of 𝔞: the primary component is the directed union of the submodules killed by 𝔞ⁿ.

    source
    theorem Ideal.mem_primaryComponent_span_iff {R : Type u_1} [CommRing R] {N : Type u_2} [AddCommMonoid N] [Module R N] (G : Finset R) {y : N} :
    y ∈ primaryComponent N (span ↑G) ↔ ∀ g ∈ G, ∃ (n : ℕ), g ^ n • y = 0

    For an ideal generated by a finite set G, an element lies in the primary component exactly when each generator g ∈ G kills it after raising to some power.