Internal direct sums from explicit equivalences

This file provides reusable infrastructure for direct sums of submodules. The generic DirectSum.piInclusion, DirectSum.piSubmodule, and DirectSum.piSubmoduleEquiv declarations describe their componentwise inclusion and range, while DirectSum.isInternal_of_lof gives a criterion for proving that a family of submodules is an internal direct sum by identifying its summands with the components of a linear equivalence.

A second group of declarations restricts a decomposition along a linear map. DirectSum.map_decompose_shift says that a map carrying each summand of one decomposition into a summand of another, along an injective reindexing of the degrees, commutes with the homogeneous projections, while DirectSum.isInternal_comap and DirectSum.Decomposition.restrict transport a decomposition backwards along an injective linear map whose range contains the homogeneous projections of its elements, with DirectSum.map_decompose_restrict computing the projections of the restricted decomposition.

A third group is about maps compatible with a decomposition: if a linear map carries each summand of a spanning family into the corresponding member of an independent family, then its kernel is spanned by its homogeneous parts, LinearMap.ker_eq_iSup_inf_of_map_le.

The file also specializes the compactness bound Ado.finite_ne_bot_of_iSupIndep_of_isCompactElement to submodules, Ado.Submodule.finite_ne_bot_of_iSupIndep_of_fg.

Finally, DirectSum.IsInternal.iSup_inf_eq_of_component_mem restricts an internal decomposition to any submodule that contains the canonical components of each of its elements.

def Ado.DirectSum.piInclusion {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : (i : ι) → Submodule R (M i)) : (DirectSum ι fun (i : ι) => ↥(N i)) →ₗ[R] DirectSum ι fun (i : ι) => M i

The canonical inclusion of a direct sum of submodules into the direct sum of their ambient modules.

Equations

• Ado.DirectSum.piInclusion N = DirectSum.lmap fun (i : ι) => (N i).subtype

def Ado.DirectSum.piSubmodule {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : (i : ι) → Submodule R (M i)) : Submodule R (DirectSum ι fun (i : ι) => M i)

The submodule of the direct sum consisting of elements whose components lie in the given submodules.

Equations

• Ado.DirectSum.piSubmodule N = (Ado.DirectSum.piInclusion N).range

@[simp]

theorem Ado.DirectSum.piInclusion_apply {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : (i : ι) → Submodule R (M i)) (x : DirectSum ι fun (i : ι) => ↥(N i)) (i : ι) : ((piInclusion N) x) i = ↑(x i)

The componentwise formula for the inclusion of a direct sum of submodules.

@[simp]

theorem Ado.DirectSum.piInclusion_lof {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : (i : ι) → Submodule R (M i)) (i : ι) (x : ↥(N i)) [DecidableEq ι] : (piInclusion N) ((DirectSum.lof R ι (fun (i : ι) => ↥(N i)) i) x) = (DirectSum.lof R ι (fun (i : ι) => M i) i) ↑x

The inclusion of a generator of a direct sum of submodules.

noncomputable def Ado.DirectSum.piSubmoduleEquiv {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : (i : ι) → Submodule R (M i)) : (DirectSum ι fun (i : ι) => ↥(N i)) ≃ₗ[R] ↥(piSubmodule N)

The linear equivalence from the direct sum of submodules to piSubmodule N.

Equations

• Ado.DirectSum.piSubmoduleEquiv N = LinearEquiv.ofInjective (Ado.DirectSum.piInclusion N) ⋯

@[simp]

theorem Ado.DirectSum.piSubmoduleEquiv_apply {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : (i : ι) → Submodule R (M i)) (x : DirectSum ι fun (i : ι) => ↥(N i)) : ↑((piSubmoduleEquiv N) x) = (piInclusion N) x

The underlying map of piSubmoduleEquiv is the canonical inclusion.

@[simp]

theorem Ado.DirectSum.piSubmoduleEquiv_symm_apply {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : (i : ι) → Submodule R (M i)) (y : ↥(piSubmodule N)) (i : ι) : ↑(((piSubmoduleEquiv N).symm y) i) = ↑y i

The inverse of piSubmoduleEquiv has the expected componentwise values.

@[simp]

theorem Ado.DirectSum.mem_piSubmodule_iff {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : (i : ι) → Submodule R (M i)) (x : DirectSum ι fun (i : ι) => M i) : x ∈ piSubmodule N ↔ ∀ (i : ι), x i ∈ N i

Membership in the direct sum of a family of submodules is componentwise.

theorem Ado.DirectSum.lof_mem_piSubmodule {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : (i : ι) → Submodule R (M i)) (i : ι) (x : ↥(N i)) [DecidableEq ι] : (DirectSum.lof R ι M i) ↑x ∈ piSubmodule N

An included summand belongs to the direct sum of a family of submodules.

theorem Ado.DirectSum.isInternal_comap {R : Type u_1} {ι : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [DecidableEq ι] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (ℳ : ι → Submodule R M) [DirectSum.Decomposition ℳ] (𝓝 : ι → Submodule R N) (f : N →ₗ[R] M) (hf : Function.Injective ⇑f) (hmem : ∀ (i : ι) (x : N), x ∈ 𝓝 i ↔ f x ∈ ℳ i) (hproj : ∀ (i : ι) (x : N), ↑(((DirectSum.decompose ℳ) (f x)) i) ∈ f.range) : DirectSum.IsInternal 𝓝

Restrict an internal direct sum decomposition along an injective linear map f which detects membership in the summands and whose range contains every homogeneous projection of each of its elements: the summands 𝓝 pulled back from ℳ are again an internal direct sum.

@[instance_reducible]

noncomputable def Ado.DirectSum.Decomposition.restrict {R : Type u_1} {ι : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [DecidableEq ι] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (ℳ : ι → Submodule R M) [DirectSum.Decomposition ℳ] (𝓝 : ι → Submodule R N) (f : N →ₗ[R] M) (hf : Function.Injective ⇑f) (hmem : ∀ (i : ι) (x : N), x ∈ 𝓝 i ↔ f x ∈ ℳ i) (hproj : ∀ (i : ι) (x : N), ↑(((DirectSum.decompose ℳ) (f x)) i) ∈ f.range) : DirectSum.Decomposition 𝓝

Restrict an internal decomposition along an injective linear map whose range contains every homogeneous projection of each of its elements.

Equations

• Ado.DirectSum.Decomposition.restrict ℳ 𝓝 f hf hmem hproj = DirectSum.IsInternal.chooseDecomposition 𝓝 ⋯

theorem Ado.DirectSum.map_decompose_shift {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {M : Type u_4} {N : Type u_5} [Semiring R] [DecidableEq ι] [DecidableEq κ] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (ℳ : ι → Submodule R M) [DirectSum.Decomposition ℳ] (𝓝 : κ → Submodule R N) [DirectSum.Decomposition 𝓝] (f : M →ₗ[R] N) (σ : ι → κ) (hσ : Function.Injective σ) (hf : ∀ (i : ι), ∀ x ∈ ℳ i, f x ∈ 𝓝 (σ i)) (i : ι) (x : M) : f ↑(((DirectSum.decompose ℳ) x) i) = ↑(((DirectSum.decompose 𝓝) (f x)) (σ i))

A linear map which carries the degree-i summand of one internal decomposition into the degree-σ i summand of another, along an injective reindexing σ of the degrees, commutes with the homogeneous projections.

@[simp]

theorem Ado.DirectSum.map_decompose_restrict {R : Type u_1} {ι : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [DecidableEq ι] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (ℳ : ι → Submodule R M) [DirectSum.Decomposition ℳ] (𝓝 : ι → Submodule R N) [DirectSum.Decomposition 𝓝] (f : N →ₗ[R] M) (hmem : ∀ (i : ι) (x : N), x ∈ 𝓝 i ↔ f x ∈ ℳ i) (i : ι) (x : N) : f ↑(((DirectSum.decompose 𝓝) x) i) = ↑(((DirectSum.decompose ℳ) (f x)) i)

Homogeneous projection in a restricted decomposition agrees with projection in the ambient module.

theorem Ado.DirectSum.isInternal_of_lof {R : Type u_1} {ι : Type u_2} {M : Type u_3} [Semiring R] [DecidableEq ι] [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} {N : ι → Type u_4} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (e : (i : ι) → N i ≃ₗ[R] ↥(A i)) (E : (DirectSum ι fun (i : ι) => N i) ≃ₗ[R] M) (hE : ∀ (i : ι) (x : N i), E ((DirectSum.lof R ι (fun (i : ι) => N i) i) x) = ↑((e i) x)) : DirectSum.IsInternal A

The canonical inclusions of a family of submodules form an internal direct sum when they are identified with the summands of an equivalence.

theorem Ado.Submodule.finite_ne_bot_of_iSupIndep_of_fg {R : Type u_1} {ι : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (hAi : iSupIndep A) (hAf : (⨆ (i : ι), A i).FG) : {i : ι | A i ≠ ⊥}.Finite

An independent family of submodules spanning a finitely generated submodule has only finitely many nonzero members.

theorem LinearMap.ker_eq_iSup_inf_of_map_le {R : Type u_1} {ι : Type u_2} {M : Type u_3} {N : Type u_4} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (g : M →ₗ[R] N) {A : ι → Submodule R M} {A' : ι → Submodule R N} (hA : ⨆ (i : ι), A i = ⊤) (hA' : iSupIndep A') (hg : ∀ (i : ι), Submodule.map g (A i) ≤ A' i) : g.ker = ⨆ (i : ι), g.ker ⊓ A i

The kernel of a map compatible with a decomposition is spanned by its homogeneous parts. If the submodules A i span the source, the submodules A' i are independent, and g carries A i into A' i, then the kernel of g is the supremum of its intersections with the A i.

The hypothesis on the source is only that its family spans; independence there is not used, and an internal direct sum supplies it through DirectSum.IsInternal.submodule_iSup_eq_top.

theorem Ado.iSupIndep_map_mkQ {R : Type u_1} {ι : Type u_2} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] {A : ι → Submodule R M} (hA : iSupIndep A) {U : Submodule R M} (hU : U ⊓ ⨆ (i : ι), A i ≤ ⨆ (i : ι), U ⊓ A i) : iSupIndep fun (i : ι) => Submodule.map U.mkQ (A i)

A homogeneous submodule can be quotiented componentwise. If A is an independent family and the part of U in the span of A is contained in the sum of its intersections with the members of A, then the members of A in M ⧸ U are again independent.

theorem DirectSum.IsInternal.iSup_inf_eq_of_component_mem {S : Type u_1} {V : Type u_2} {κ : Type u_3} [Semiring S] [AddCommMonoid V] [Module S V] [DecidableEq κ] {A : κ → Submodule S V} (h : IsInternal A) (p : Submodule S V) (hp : ∀ m ∈ p, ∀ (i : κ), ↑(((LinearEquiv.ofBijective (coeLinearMap A) h).symm m) i) ∈ p) : ⨆ (i : κ), p ⊓ A i = p

Restricting an internal decomposition to a component-stable subspace. If a subspace contains every canonical component of each of its elements, then it is the internal sum of its intersections with the original summands.