Saturation with respect to an idempotent coordinate

For a left module M and an idempotent coordinate e, the largest submodule on which the entire left ideal generated by e acts trivially consists of the elements x satisfying (e * r) • x = 0 for every scalar r.

Applied to M / L, its inverse image in M is the source-literal maximal enlargement of L that is invisible to the projective coordinate R e. This is the elementary saturation operation used in Iyama's realization argument.

theorem MagnitudeConjecture.IdempotentSaturation.forall_linearMap_eq_zero_congr {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] {P Q : Type u} [AddCommGroup P] [Module R P] [AddCommGroup Q] [Module R Q] (E : P ≃ₗ[R] Q) : (∀ (f : P →ₗ[R] M), f = 0) ↔ ∀ (g : Q →ₗ[R] M), g = 0

Universal vanishing of linear maps is unchanged when the source is replaced by a linearly equivalent module.

def MagnitudeConjecture.IdempotentSaturation.rightMultiplication {R : Type u} [Ring R] (e : R) : R →ₗ[R] R

Right multiplication by e on the left regular module.

def MagnitudeConjecture.IdempotentSaturation.principalLeftIdeal {R : Type u} [Ring R] (e : R) : Submodule R R

The principal left ideal R e, regarded as a left R-module.

def MagnitudeConjecture.IdempotentSaturation.principalLeftIdealGenerator {R : Type u} [Ring R] (e : R) : ↥(principalLeftIdeal e)

The canonical generator e of the principal left ideal R e.

theorem MagnitudeConjecture.IdempotentSaturation.principalLeftIdeal_fixed {R : Type u} [Ring R] {e : R} (he : IsIdempotentElem e) (y : ↥(principalLeftIdeal e)) : ↑y * e = ↑y

Every element of R e is fixed by right multiplication by an idempotent e.

def MagnitudeConjecture.IdempotentSaturation.principalLeftIdealHomOf {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] (e : R) (x : M) : ↥(principalLeftIdeal e) →ₗ[R] M

Every module element defines a map R e → M by scalar multiplication.

@[simp]

theorem MagnitudeConjecture.IdempotentSaturation.principalLeftIdealHomOf_generator {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] (e : R) (x : M) : (principalLeftIdealHomOf e x) (principalLeftIdealGenerator e) = e • x

theorem MagnitudeConjecture.IdempotentSaturation.principalLeftIdeal_hom_eq_zero_of_smul_eq_zero {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] {e : R} (he : IsIdempotentElem e) (hzero : ∀ (x : M), e • x = 0) (f : ↥(principalLeftIdeal e) →ₗ[R] M) : f = 0

If e annihilates a module, every map from the principal left ideal R e to that module is zero.

theorem MagnitudeConjecture.IdempotentSaturation.principalLeftIdeal_hom_eq_zero_iff {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] {e : R} (he : IsIdempotentElem e) : (∀ (f : ↥(principalLeftIdeal e) →ₗ[R] M), f = 0) ↔ ∀ (x : M), e • x = 0

Vanishing of all maps from R e is exactly annihilation by e.

def MagnitudeConjecture.IdempotentSaturation.torsionSubmodule {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] (e : R) : Submodule R M

The largest submodule whose every scalar translate is annihilated by e. Equivalently, this is the largest submodule on which the left ideal R e has zero Hom coordinate.

@[simp]

theorem MagnitudeConjecture.IdempotentSaturation.mem_torsionSubmodule_iff {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] (e : R) (x : M) : x ∈ torsionSubmodule e ↔ ∀ (r : R), (e * r) • x = 0

theorem MagnitudeConjecture.IdempotentSaturation.smul_eq_zero_of_mem_torsionSubmodule {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] (e : R) {x : M} (hx : x ∈ torsionSubmodule e) : e • x = 0

In particular, e annihilates its torsion submodule.

theorem MagnitudeConjecture.IdempotentSaturation.le_torsionSubmodule {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] (e : R) (N : Submodule R M) (hN : ∀ x ∈ N, e • x = 0) : N ≤ torsionSubmodule e

Any submodule annihilated by e is contained in the torsion submodule. Closure under all scalars supplies the stronger defining condition.

def MagnitudeConjecture.IdempotentSaturation.saturation {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] (e : R) (L : Submodule R M) : Submodule R M

Enlarge L by the full idempotent-torsion submodule of M / L.

@[simp]

theorem MagnitudeConjecture.IdempotentSaturation.mem_saturation_iff {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] (e : R) (L : Submodule R M) (x : M) : x ∈ saturation e L ↔ ∀ (r : R), (e * r) • L.mkQ x = 0

theorem MagnitudeConjecture.IdempotentSaturation.le_saturation {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] (e : R) (L : Submodule R M) : L ≤ saturation e L

Saturation really enlarges the original submodule.

theorem MagnitudeConjecture.IdempotentSaturation.smul_mkQ_eq_zero_of_mem_saturation {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] (e : R) (L : Submodule R M) {x : M} (hx : x ∈ saturation e L) : e • L.mkQ x = 0

The quotient of the saturation by L is annihilated by e.

theorem MagnitudeConjecture.IdempotentSaturation.le_saturation_of_smul_mkQ_eq_zero {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] (e : R) (L N : Submodule R M) (hN : ∀ x ∈ N, e • L.mkQ x = 0) : N ≤ saturation e L

Maximality: every enlargement of L whose image in M / L is annihilated by e lies in the saturation.

theorem MagnitudeConjecture.IdempotentSaturation.torsionSubmodule_quotient_saturation_eq_bot {R M : Type u} [Ring R] [AddCommGroup M] [Module R M] {e : R} (he : IsIdempotentElem e) (L : Submodule R M) : torsionSubmodule e = ⊥

Saturating once removes all remaining idempotent torsion: the quotient by saturation e L has no nonzero submodule element whose scalar translates are all annihilated by e.