An Artinian submodule meets a filtered intersection at a finite stage

Let F be a downward-directed family of submodules of a module M — a filtration F 0 ≥ F 1 ≥ ⋯ is the typical case — and let W be a submodule of M that is Artinian, for instance a finite-dimensional subspace of an infinite-dimensional vector space. The traces W ⊓ F i are again downward directed, and they live in the Artinian lattice of submodules of W, so they cannot descend forever: one of them already equals the trace W ⊓ ⨅ j, F j of the whole intersection. In particular, if the family intersects in ⊥, then W ⊓ F i = ⊥ for some single i.

Nothing is assumed about M itself; that is the point. Mathlib's stabilization results for descending chains — IsArtinian.monotone_stabilizes and Module.End.eventually_iInf_range_pow_eq — all require the ambient module to be Artinian, which fails in the intended applications, where M is an infinite-dimensional algebra and only the subspace being separated is finite-dimensional.

The lattice-theoretic core is Directed.exists_eq_iInf in TauCeti/Order/Directed.lean; everything here is its transport along Submodule.comap W.subtype, which turns the traces on W into honest submodules of W and so makes IsArtinian R W applicable.

Main results

• Submodule.exists_inf_eq_inf_iInf_of_directed: the trace of a downward-directed family of submodules on an Artinian submodule W attains the trace of the infimum, with no hypothesis on the ambient module.
• Submodule.exists_disjoint_of_directed: consequently W is disjoint from a single member of the family as soon as it is disjoint from their infimum.
• Submodule.exists_forall_inf_eq_inf_iInf_of_antitone and Submodule.exists_forall_inf_eq_bot_of_antitone: for an antitone filtration indexed by a directed order the trace is eventually constant, not merely constant at one index.
• LinearMap.exists_mkQ_comp_injective_of_directed: the form the applications use — an embedding of an Artinian module into M stays injective after passing to the quotient by a single member of a family whose infimum is ⊥.
• Ideal.exists_forall_inf_restrictScalars_pow_eq_bot: the specialization to the powers of a (one- or two-sided) ideal of an algebra, viewed as submodules over the base ring.

theorem Submodule.exists_inf_eq_inf_iInf_of_directed {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_1} [Nonempty ι] (W : Submodule R M) [IsArtinian R ↥W] (F : ι → Submodule R M) (hF : Directed (fun (x1 x2 : Submodule R M) => x1 ≥ x2) F) : ∃ (i : ι), W ⊓ F i = W ⊓ ⨅ (j : ι), F j

The trace of a downward-directed family of submodules on an Artinian submodule attains the trace of the infimum.

The ambient module M is arbitrary; only W is Artinian. This is the statement wanted when M is an infinite-dimensional algebra and W is a finite-dimensional subspace of it, where applying Directed.exists_eq_iInf to the lattice Submodule R M itself is not possible.

theorem Submodule.exists_disjoint_of_directed {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_1} [Nonempty ι] (W : Submodule R M) [IsArtinian R ↥W] (F : ι → Submodule R M) (hF : Directed (fun (x1 x2 : Submodule R M) => x1 ≥ x2) F) (hW : Disjoint W (⨅ (j : ι), F j)) : ∃ (i : ι), Disjoint W (F i)

An Artinian submodule disjoint from a filtered intersection is already disjoint from one member of the family.

theorem Submodule.exists_forall_inf_eq_inf_iInf_of_antitone {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type w} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι] (W : Submodule R M) [IsArtinian R ↥W] (F : ι → Submodule R M) (hF : Antitone F) : ∃ (i : ι), ∀ (j : ι), i ≤ j → W ⊓ F j = W ⊓ ⨅ (k : ι), F k

The trace of an antitone filtration on an Artinian submodule is eventually the trace of the intersection.

Unlike Submodule.exists_inf_eq_inf_iInf_of_directed, which produces one index, monotonicity makes the conclusion hold from that index onwards.

theorem Submodule.exists_forall_inf_eq_bot_of_antitone {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type w} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι] (W : Submodule R M) [IsArtinian R ↥W] (F : ι → Submodule R M) (hF : Antitone F) (h : ⨅ (k : ι), F k = ⊥) : ∃ (i : ι), ∀ (j : ι), i ≤ j → W ⊓ F j = ⊥

An antitone filtration with zero intersection eventually misses an Artinian submodule.

This is the separation step in the form its consumers use: W is a finite-dimensional subspace, F is a filtration of the ambient module by submodules with ⨅ k, F k = ⊥, and the conclusion exhibits a stage at which W is separated.

theorem LinearMap.exists_mkQ_comp_injective_of_directed {R : Type u} {M : Type v} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {ι : Sort u_1} [Nonempty ι] [IsArtinian R N] (f : N →ₗ[R] M) (hf : Function.Injective ⇑f) (F : ι → Submodule R M) (hF : Directed (fun (x1 x2 : Submodule R M) => x1 ≥ x2) F) (h : ⨅ (j : ι), F j = ⊥) : ∃ (i : ι), Function.Injective ⇑((F i).mkQ ∘ₗ f)

An embedding of an Artinian module survives the quotient by a single member of a family whose intersection is zero.

Applied to the canonical embedding of a finite-dimensional Lie algebra into its universal enveloping algebra, this is the statement that the algebra is separated by one finite stage of a filtration, which is how a faithful representation on a quotient is obtained.

theorem Ideal.exists_forall_inf_restrictScalars_pow_eq_bot {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (I : Ideal A) (W : Submodule R A) [IsArtinian R ↥W] (h : ⨅ (n : ℕ), I ^ n = ⊥) : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → W ⊓ Submodule.restrictScalars R (I ^ m) = ⊥

The powers of an ideal whose intersection is zero are eventually disjoint from an Artinian submodule of the algebra.

No commutativity of A and no two-sidedness of I is needed: the powers of a left ideal are antitone, and the statement concerns their underlying R-submodules. This is the shape taken by the separation of a finite-dimensional Lie algebra from the powers of the central ideal of its universal enveloping algebra.