Superfluous submodules

A submodule N of M is superfluous (also called small) when it is dispensable for generating M: whenever N ⊔ K = ⊤ for a submodule K, already K = ⊤. Superfluous submodules are the dual notion to essential submodules, and an epimorphism P ↠ M is a projective cover exactly when P is projective and its kernel is superfluous in P.

Mathlib has neither this predicate nor projective covers. This file supplies the predicate with its lattice API and identifies it, on the modules where the comparison is available, with being contained in the radical Module.jacobson.

Main definitions

• TauCeti.IsSuperfluous: N ⊔ K = ⊤ forces K = ⊤.

Main results

• TauCeti.isSuperfluous_iff: the definition, restated so that superfluity can be proved downstream.
• TauCeti.isSuperfluous_bot, TauCeti.IsSuperfluous.mono, TauCeti.isSuperfluous_sup_iff: the superfluous submodules of M are closed downwards and under binary suprema, and contain ⊥.
• TauCeti.isSuperfluous_top_iff: ⊤ is superfluous exactly for the zero module.
• TauCeti.IsSuperfluous.map: the image of a superfluous submodule under any linear map is superfluous; TauCeti.isSuperfluous_map_equiv_iff records that along an equivalence this is an equivalence.
• TauCeti.IsSuperfluous.comap: the preimage of a superfluous submodule under a surjection whose kernel is superfluous is again superfluous. This is what makes projective covers compose.
• TauCeti.IsSuperfluous.surjective_of_surjective_comp and TauCeti.isSuperfluous_ker_iff_forall_surjective: a surjection has superfluous kernel exactly when it is an essential epimorphism, that is, when every map into its source whose composite with it is onto is itself onto. This is the minimality that makes a projective cover a projective cover. Both directions need differences, so they are stated for modules over a semiring that are additive groups.
• TauCeti.IsSuperfluous.le_coatom and TauCeti.IsSuperfluous.le_jacobson: a superfluous submodule lies in every coatom, hence in the radical Module.jacobson R M.
• TauCeti.isSuperfluous_iff_le_jacobson: over a module whose submodule lattice is coatomic — in particular over a finitely generated module — the converse holds, so the superfluous submodules are exactly the submodules of the radical, and TauCeti.isSuperfluous_jacobson records that the radical itself is then superfluous.
• TauCeti.isSuperfluous_smul_top_of_isNilpotent: the form of Nakayama's lemma that needs no hypothesis on the module at all — a nilpotent ideal times any module is superfluous in it.

References

See I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.4, and T. Y. Lam, A First Course in Noncommutative Rings, §24.

def TauCeti.IsSuperfluous {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) : Prop

A submodule N of M is superfluous (or small) when it is dispensable for generating M: any submodule K with N ⊔ K = ⊤ is already ⊤.

Equations

• TauCeti.IsSuperfluous N = ∀ (K : Submodule R M), N ⊔ K = ⊤ → K = ⊤

theorem TauCeti.isSuperfluous_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} : IsSuperfluous N ↔ ∀ (K : Submodule R M), N ⊔ K = ⊤ → K = ⊤

Superfluity, restated: this is the introduction rule for TauCeti.IsSuperfluous, whose body is not exposed outside this module.

theorem TauCeti.IsSuperfluous.eq_top_of_sup_eq_top {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N K : Submodule R M} (hN : IsSuperfluous N) (h : N ⊔ K = ⊤) : K = ⊤

The defining property of a superfluous submodule, in the shape it is consumed in.

theorem TauCeti.IsSuperfluous.eq_bot_of_isCompl {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N K : Submodule R M} (hN : IsSuperfluous N) (hNK : IsCompl N K) : N = ⊥

A superfluous direct summand is zero.

@[simp]

theorem TauCeti.isSuperfluous_bot {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : IsSuperfluous ⊥

The zero submodule is superfluous.

theorem TauCeti.IsSuperfluous.mono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N N' : Submodule R M} (hN' : IsSuperfluous N') (h : N ≤ N') : IsSuperfluous N

A submodule of a superfluous submodule is superfluous.

theorem TauCeti.IsSuperfluous.sup {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N N' : Submodule R M} (hN : IsSuperfluous N) (hN' : IsSuperfluous N') : IsSuperfluous (N ⊔ N')

The supremum of two superfluous submodules is superfluous.

@[simp]

theorem TauCeti.isSuperfluous_sup_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N N' : Submodule R M} : IsSuperfluous (N ⊔ N') ↔ IsSuperfluous N ∧ IsSuperfluous N'

A supremum of two submodules is superfluous exactly when both of them are.

@[simp]

theorem TauCeti.isSuperfluous_top_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : IsSuperfluous ⊤ ↔ Subsingleton M

The whole module is superfluous in itself exactly when it is zero: superfluity of ⊤ says precisely that ⊥ = ⊤.

theorem TauCeti.not_isSuperfluous_top {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] : ¬IsSuperfluous ⊤

The whole module is not superfluous in a nonzero module.

theorem TauCeti.IsSuperfluous.ne_top {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] {N : Submodule R M} (hN : IsSuperfluous N) : N ≠ ⊤

A superfluous submodule of a nonzero module is proper.

@[simp]

theorem TauCeti.isSuperfluous_map_equiv_iff {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {N : Submodule R M} (e : M ≃ₗ[R] M₂) : IsSuperfluous (Submodule.map (↑e) N) ↔ IsSuperfluous N

Transport along a linear equivalence both preserves and reflects superfluity.

theorem TauCeti.IsSuperfluous.le_coatom {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N m : Submodule R M} (hN : IsSuperfluous N) (hm : IsCoatom m) : N ≤ m

A superfluous submodule is contained in every maximal submodule.

theorem TauCeti.isSuperfluous_smul_top_of_isNilpotent {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} (hI : IsNilpotent I) : IsSuperfluous (I • ⊤)

Nakayama's lemma for a nilpotent ideal. If I is a nilpotent ideal then I • M is superfluous in M.

Unlike TauCeti.isSuperfluous_jacobson, which asks the submodule lattice of M to be coatomic (for instance M finitely generated) and takes the radical of M, nilpotence of I buys the conclusion for an arbitrary module: a submodule K with I • M ⊔ K = ⊤ absorbs I ^ k • M into I ^ (k + 1) • M for every k, and a power of I vanishes.

theorem TauCeti.IsSuperfluous.map {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] {N : Submodule R M} (hN : IsSuperfluous N) (f : M →ₗ[R] M₂) : IsSuperfluous (Submodule.map f N)

The image of a superfluous submodule under a linear map is superfluous.

theorem TauCeti.IsSuperfluous.comap {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] {K : Submodule R M₂} (hK : IsSuperfluous K) {f : M →ₗ[R] M₂} (hf : Function.Surjective ⇑f) (hker : IsSuperfluous f.ker) : IsSuperfluous (Submodule.comap f K)

The preimage of a superfluous submodule under a surjection whose kernel is itself superfluous is superfluous. This is what makes projective covers compose.

theorem TauCeti.IsSuperfluous.surjective_of_surjective_comp {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] {M₃ : Type u_1} [AddCommMonoid M₃] [Module R M₃] {f : M →ₗ[R] M₂} (hf : IsSuperfluous f.ker) {h : M₃ →ₗ[R] M} (hfh : Function.Surjective ⇑(f ∘ₗ h)) : Function.Surjective ⇑h

A superfluous kernel is a minimality condition. If f : M →ₗ[R] M₂ has superfluous kernel and h : M₃ →ₗ[R] M is such that f ∘ₗ h is onto, then h is already onto.

This is what makes a projective cover minimal; it is TauCeti.IsProjectiveCover's workhorse, and uses nothing about f beyond its kernel.

theorem TauCeti.isSuperfluous_ker_iff_forall_surjective {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] {f : M →ₗ[R] M₂} (hf : Function.Surjective ⇑f) : IsSuperfluous f.ker ↔ ∀ {M₃ : Type v} [inst : AddCommMonoid M₃] [inst_1 : Module R M₃] (h : M₃ →ₗ[R] M), Function.Surjective ⇑(f ∘ₗ h) → Function.Surjective ⇑h

Superfluous kernels are exactly the essential epimorphisms. A surjection f : M →ₗ[R] M₂ has superfluous kernel precisely when no map into M can compose onto M₂ without already being onto; the submodule inclusions of M witness the nontrivial direction, so it suffices to quantify over sources in the universe of M (over larger sources the implication is TauCeti.IsSuperfluous.surjective_of_surjective_comp).

theorem TauCeti.IsSuperfluous.le_jacobson {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} (hN : IsSuperfluous N) : N ≤ Module.jacobson R M

A superfluous submodule is contained in the radical.

theorem TauCeti.isSuperfluous_of_le_jacobson {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [IsCoatomic (Submodule R M)] {N : Submodule R M} (h : N ≤ Module.jacobson R M) : IsSuperfluous N

Conversely, when every proper submodule of M sits under a maximal one, every submodule of the radical is superfluous.

@[simp]

theorem TauCeti.isSuperfluous_iff_le_jacobson {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [IsCoatomic (Submodule R M)] {N : Submodule R M} : IsSuperfluous N ↔ N ≤ Module.jacobson R M

Over a module with coatomic submodule lattice — for instance a finitely generated one — the superfluous submodules are exactly the submodules of the radical.

This is the simp normal form of superfluity wherever the comparison is available, at low priority so that the shape-specific lemmas above (TauCeti.isSuperfluous_bot, TauCeti.isSuperfluous_sup_iff, TauCeti.isSuperfluous_top_iff, TauCeti.isSuperfluous_map_equiv_iff) still fire first on the submodules they match.

theorem TauCeti.isSuperfluous_jacobson {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [IsCoatomic (Submodule R M)] : IsSuperfluous (Module.jacobson R M)

The radical of a module with coatomic submodule lattice — for instance a finitely generated one — is superfluous; this is the form of Nakayama's lemma that the theory of projective covers runs on.