Projections onto the summands of an internal direct sum

Mathlib's Submodule.projectionOnto projects a module onto one of two complementary submodules. A family Q of submodules that is iSupIndep and spans the whole module presents each Q i as complementary to the supremum of the other summands (iSupIndep.isCompl_biSup_ne), so each summand inherits such a projection.

This file records these projections, Ado.internalProjection. Their pointwise behaviour and kernel are Mathlib's lemmas about Submodule.projectionOnto, restated for the specialization. The one fact that goes beyond a single projection is that over a finite index type the projections sum to the identity, Ado.sum_coe_internalProjection.

Main definitions

• Ado.internalProjection: the projection of M onto the summand Q i of an internal direct sum decomposition, as a linear map M →ₗ[A] Q i.

Main results

• Ado.internalProjection_surjective: the projection onto Q i is surjective.
• Ado.ker_internalProjection: the kernel of the projection onto Q i is the supremum of the other summands.
• Ado.sum_coe_internalProjection: over a finite index type the projections onto the summands sum to the identity.
• DirectSum.IsInternal.coe_ofBijective_coeLinearMap_symm_apply_eq_internalProjection: the component supplied by the inverse direct-sum equivalence is the internal projection.

Implementation notes

The decomposition is spelled as iSupIndep Q together with ⨆ i, Q i = ⊤ rather than as DirectSum.IsInternal, which carries a DecidableEq hypothesis on the index type that nothing here needs; DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top converts between the two.

noncomputable def Ado.internalProjection {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] {ι : Type w} {Q : ι → Submodule A M} (hQi : iSupIndep Q) (hQt : ⨆ (i : ι), Q i = ⊤) (i : ι) : M →ₗ[A] ↥(Q i)

The projection of M onto the summand Q i of an internal direct sum decomposition, along the supremum of the other summands.

Equations

• Ado.internalProjection hQi hQt i = (Q i).projectionOnto (⨆ (j : ι), ⨆ (_ : j ≠ i), Q j) ⋯

theorem Ado.internalProjection_apply_of_mem {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] {ι : Type w} {Q : ι → Submodule A M} (hQi : iSupIndep Q) (hQt : ⨆ (i : ι), Q i = ⊤) {i : ι} {x : M} (hx : x ∈ Q i) : (internalProjection hQi hQt i) x = ⟨x, hx⟩

The projection onto Q i fixes the elements of Q i.

@[simp]

theorem Ado.internalProjection_apply {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] {ι : Type w} {Q : ι → Submodule A M} (hQi : iSupIndep Q) (hQt : ⨆ (i : ι), Q i = ⊤) {i : ι} (x : ↥(Q i)) : (internalProjection hQi hQt i) ↑x = x

The projection onto Q i restricts to the identity on Q i.

theorem Ado.internalProjection_apply_eq_zero_of_mem_of_ne {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] {ι : Type w} {Q : ι → Submodule A M} (hQi : iSupIndep Q) (hQt : ⨆ (i : ι), Q i = ⊤) {i j : ι} (hij : i ≠ j) {x : M} (hx : x ∈ Q i) : (internalProjection hQi hQt j) x = 0

The projection onto Q j kills the elements of any other summand Q i.

@[simp]

theorem Ado.internalProjection_apply_of_ne {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] {ι : Type w} {Q : ι → Submodule A M} (hQi : iSupIndep Q) (hQt : ⨆ (i : ι), Q i = ⊤) {i j : ι} (hij : i ≠ j) (x : ↥(Q i)) : (internalProjection hQi hQt j) ↑x = 0

The projection onto Q j restricts to 0 on any other summand Q i.

This is the form simp can use: the summand index i is read off the type of x, whereas in Ado.internalProjection_apply_eq_zero_of_mem_of_ne it appears only in the hypotheses.

theorem Ado.internalProjection_surjective {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] {ι : Type w} {Q : ι → Submodule A M} (hQi : iSupIndep Q) (hQt : ⨆ (i : ι), Q i = ⊤) (i : ι) : Function.Surjective ⇑(internalProjection hQi hQt i)

The projection onto Q i is surjective, being the identity on Q i.

@[simp]

theorem Ado.ker_internalProjection {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] {ι : Type w} {Q : ι → Submodule A M} (hQi : iSupIndep Q) (hQt : ⨆ (i : ι), Q i = ⊤) (i : ι) : (internalProjection hQi hQt i).ker = ⨆ (j : ι), ⨆ (_ : j ≠ i), Q j

The kernel of the projection onto Q i is the supremum of the other summands.

theorem Ado.sum_coe_internalProjection {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] {ι : Type w} {Q : ι → Submodule A M} [Fintype ι] (hQi : iSupIndep Q) (hQt : ⨆ (i : ι), Q i = ⊤) (x : M) : ∑ i : ι, ↑((internalProjection hQi hQt i) x) = x

Over a finite index type the projections onto the summands sum to the identity.

The sum of the projections is a linear map agreeing with the identity on each summand, and the summands span M.

theorem DirectSum.IsInternal.coe_ofBijective_coeLinearMap_symm_apply_eq_internalProjection {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] {ι : Type w} [DecidableEq ι] {Q : ι → Submodule A M} (h : IsInternal Q) (i : ι) (x : M) : ↑(((LinearEquiv.ofBijective (coeLinearMap Q) h).symm x) i) = ↑((Ado.internalProjection ⋯ ⋯ i) x)

The component supplied by the inverse of the canonical internal-direct-sum equivalence is the projection onto that summand.