Essential submodules

A submodule N of M is essential (also called large) when it is indispensable for separating points of M: whenever N ⊓ K = ⊥ for a submodule K, already K = ⊥. Essential submodules are the notion dual to the superfluous submodules of TauCeti/Algebra/Module/Submodule/Superfluous.lean, and a monomorphism M ↪ Q is an injective envelope exactly when Q is injective and the image is essential in Q.

Mathlib has neither this predicate nor injective envelopes. This file supplies the predicate with its lattice API and identifies it, on the modules where the comparison is available, with containing every simple submodule.

The duality with superfluity is not formal — there is no order isomorphism between the submodule lattices of a module and of a dual object — so the statements are proved, not transported. Two of them are genuinely less symmetric than their superfluous counterparts: the image of an essential submodule is essential only along an embedding whose own image is essential (TauCeti.IsEssential.map, the analogue of TauCeti.IsSuperfluous.comap), while the preimage is essential along any linear map (TauCeti.IsEssential.comap, the analogue of TauCeti.IsSuperfluous.map).

Main definitions

• TauCeti.IsEssential: N ⊓ K = ⊥ forces K = ⊥.

Main results

• TauCeti.isEssential_iff: the definition, restated so that essentiality can be proved and used downstream.
• TauCeti.isEssential_top, TauCeti.IsEssential.mono, TauCeti.isEssential_inf_iff: the essential submodules of M are closed upwards and under binary infima, and contain ⊤.
• TauCeti.isEssential_bot_iff: ⊥ is essential exactly for the zero module.
• TauCeti.IsEssential.comap: the preimage of an essential submodule under any linear map is essential.
• TauCeti.IsEssential.map: the image of an essential submodule under an embedding whose range is itself essential is essential; TauCeti.isEssential_map_equiv_iff records that along an equivalence this is an equivalence. This is what makes injective envelopes compose.
• TauCeti.IsEssential.injective_of_injective_comp and TauCeti.isEssential_range_iff_forall_injective: an embedding has essential range exactly when it is an essential monomorphism, that is, when every map out of its target whose composite with it is injective is itself injective. This is the minimality that makes an injective envelope an injective envelope.
• TauCeti.IsEssential.atom_le and TauCeti.isEssential_iff_forall_atom_le: an essential submodule contains every atom of the submodule lattice — every simple submodule — and over an atomic submodule lattice that property characterizes essentiality.

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, Lectures on Modules and Rings, §3.

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

A submodule N of M is essential (or large) when it meets every nonzero submodule: any submodule K with N ⊓ K = ⊥ is already ⊥.

Equations

• TauCeti.IsEssential N = ∀ (K : Submodule R M), N ⊓ K = ⊥ → K = ⊥

theorem TauCeti.isEssential_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} : IsEssential N ↔ ∀ (K : Submodule R M), N ⊓ K = ⊥ → K = ⊥

Essentiality, restated. The body of TauCeti.IsEssential is not exposed outside this module, so this is the interface through which essentiality is both proved and used.

@[simp]

theorem TauCeti.isEssential_top {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : IsEssential ⊤

The whole module is essential in itself.

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

A submodule containing an essential submodule is essential.

theorem TauCeti.IsEssential.inf {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N N' : Submodule R M} (hN : IsEssential N) (hN' : IsEssential N') : IsEssential (N ⊓ N')

The infimum of two essential submodules is essential.

@[simp]

theorem TauCeti.isEssential_inf_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N N' : Submodule R M} : IsEssential (N ⊓ N') ↔ IsEssential N ∧ IsEssential N'

An infimum of two submodules is essential exactly when both of them are.

@[simp]

theorem TauCeti.isEssential_bot_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : IsEssential ⊥ ↔ Subsingleton M

The zero submodule is essential exactly in the zero module: essentiality of ⊥ says precisely that ⊤ = ⊥.

theorem TauCeti.not_isEssential_bot {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] : ¬IsEssential ⊥

The zero submodule is not essential in a nonzero module.

theorem TauCeti.IsEssential.ne_bot {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] {N : Submodule R M} (hN : IsEssential N) : N ≠ ⊥

An essential submodule of a nonzero module is nonzero.

theorem TauCeti.IsEssential.comap {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₂} (hN : IsEssential N) (f : M →ₗ[R] M₂) : IsEssential (Submodule.comap f N)

The preimage of an essential submodule under any linear map is essential.

theorem TauCeti.IsEssential.map {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} (hN : IsEssential N) {f : M →ₗ[R] M₂} (hf : Function.Injective ⇑f) (hrange : IsEssential f.range) : IsEssential (Submodule.map f N)

The image of an essential submodule under an embedding whose range is itself essential is essential. This is what makes injective envelopes compose; unlike the preimage (TauCeti.IsEssential.comap), the image needs both hypotheses on the map: the image of ⊤ under the inclusion of a non-essential submodule is that submodule, which is not essential.

@[simp]

theorem TauCeti.isEssential_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₂) : IsEssential (Submodule.map (↑e) N) ↔ IsEssential N

Transport along a linear equivalence both preserves and reflects essentiality.

theorem TauCeti.IsEssential.atom_le {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {N a : Submodule R M} (hN : IsEssential N) (ha : IsAtom a) : a ≤ N

An essential submodule contains every atom of the submodule lattice, that is, every simple submodule.

theorem TauCeti.isEssential_of_forall_atom_le {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [IsAtomic (Submodule R M)] {N : Submodule R M} (h : ∀ (a : Submodule R M), IsAtom a → a ≤ N) : IsEssential N

Conversely, when every nonzero submodule of M contains a simple one, a submodule containing every simple submodule is essential.

theorem TauCeti.isEssential_iff_forall_atom_le {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [IsAtomic (Submodule R M)] {N : Submodule R M} : IsEssential N ↔ ∀ (a : Submodule R M), IsAtom a → a ≤ N

Over a module with atomic submodule lattice — for instance an Artinian one — the essential submodules are exactly the submodules containing every simple submodule.

theorem TauCeti.IsEssential.injective_of_injective_comp {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommGroup M₂] [Module R M₂] {M₃ : Type u_1} [AddCommMonoid M₃] [Module R M₃] {f : M →ₗ[R] M₂} (hf : IsEssential f.range) {h : M₂ →ₗ[R] M₃} (hhf : Function.Injective ⇑(h ∘ₗ f)) : Function.Injective ⇑h

An essential range is a minimality condition. If f : M →ₗ[R] M₂ has essential range and h : M₂ →ₗ[R] M₃ is such that h ∘ₗ f is injective, then h is already injective. This is what makes an injective envelope minimal.

theorem TauCeti.isEssential_range_iff_forall_injective {R : Type u} {M : Type v} {M₂ : Type w} [Ring R] [AddCommMonoid M] [Module R M] [AddCommGroup M₂] [Module R M₂] {f : M →ₗ[R] M₂} (hf : Function.Injective ⇑f) : IsEssential f.range ↔ ∀ {M₃ : Type w} [inst : AddCommMonoid M₃] [inst_1 : Module R M₃] (h : M₂ →ₗ[R] M₃), Function.Injective ⇑(h ∘ₗ f) → Function.Injective ⇑h

Essential ranges are exactly the essential monomorphisms. An embedding f : M →ₗ[R] M₂ has essential range precisely when no map out of M₂ can precompose to an embedding without already being one. It suffices to quantify over targets in the universe of M₂; for arbitrary targets the forward implication is TauCeti.IsEssential.injective_of_injective_comp.