Theorems for binary direct sum of modules

Stream: mathlib4

[Paul Schwahn]

Hi everyone,

in the course of a linear algebra heavy project we needed some definition/theorems about direct sums of modules. Back then I noticed that these existed for arbitrarily indexed direct sums ⨁ i, M i (although I can't find them anymore), but I think it would be really useful to have them for binary direct sums/products M₁ × M₂ as well.

I am thinking of creating PRs for the following two definitions:
1) The linear map from M₁ × M₂ to L defined by specifying maps from M₁ and M₂ to L
2) A linear equivalence from the product of two complementary submodules of L to L.

import Mathlib

variable {K L : Type*} [CommRing K] [AddCommGroup L] [Module K L] (p q : Submodule K L)

/-- The linear map from `M₁ × M₂` to `L` defined by specifying maps from `M₁` and `M₂` to `L`. -/
def LinearMap.ofProd {M₁ M₂ : Type*} [AddCommGroup M₁] [AddCommGroup M₂] [Module K M₁] [Module K M₂]
      (f : M₁ →ₗ[K] L) (g : M₂ →ₗ[K] L) :
    M₁ × M₂ →ₗ[K] L :=
  f ∘ₗLinearMap.fst K M₁ M₂ + g ∘ₗLinearMap.snd K M₁ M₂

@[simp]
theorem LinearMap.ofProd_apply {M₁ M₂ : Type*} [AddCommGroup M₁] [AddCommGroup M₂] [Module K M₁] [Module K M₂]
      (f : M₁ →ₗ[K] L) (g : M₂ →ₗ[K] L) (x : M₁ × M₂) :
    LinearMap.ofProd f g x = f x.1 + g x.2 := rfl

variable {p q}

/-- If two submodules are disjoint, then the canonical map from the product is injective. -/
theorem Submodule.prod_injective_of_disjoint (h : Disjoint p q) :
    Function.Injective (LinearMap.ofProd p.subtype q.subtype) := by
  rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff]
  intro x hx
  simp only [LinearMap.mem_ker, LinearMap.ofProd_apply, subtype_apply] at hx
  rw [add_eq_zero_iff_neg_eq'] at hx
  have x₁p : x.1.val ∈ p := x.1.prop
  have x₁q : x.1.val ∈ q := by
    rw [← hx, Submodule.neg_mem_iff]
    exact x.2.prop
  have x₁0 := Submodule.disjoint_def.mp h _ x₁p x₁q
  have x₂p : x.2.val ∈ p := by
    rw [← Submodule.neg_mem_iff, hx]
    exact x.1.prop
  have x₂q : x.2.val ∈ q := x.2.prop
  have x₂0 := Submodule.disjoint_def.mp h _ x₂p x₂q
  ext
  · rw [x₁0]
    rfl
  · rw [x₂0]
    rfl

/-- If two submodules are codisjoint, then the canonical map from the product is surjectve. -/
theorem Submodule.prod_surjective_of_codisjoint (h : Codisjoint p q) :
    Function.Surjective (LinearMap.ofProd p.subtype q.subtype) := by
  intro x
  obtain ⟨y, hy, z, hz, hx⟩ := Submodule.exists_add_eq_of_codisjoint h x
  use ⟨⟨y, hy⟩, ⟨z, hz⟩⟩
  simp only [LinearMap.ofProd_apply, subtype_apply]
  exact hx

/-- If two submodules are complementary, then their product is isomorphic to the ambient space. -/
noncomputable def LinearEquiv.ofComplSubmodules (h : IsCompl p q) :
    (p × q) ≃ₗ[K] L :=
  LinearEquiv.ofBijective (LinearMap.ofProd p.subtype q.subtype)
    ⟨Submodule.prod_injective_of_disjoint h.disjoint, Submodule.prod_surjective_of_codisjoint h.codisjoint⟩

@[simp]
theorem LinearEquiv.ofComplSubmodules_apply (h : IsCompl p q) (x : p × q) :
    (LinearEquiv.ofComplSubmodules h) x = x.1.val + x.2.val := rfl

theorem LinearEquiv.ofComplSubmodules_symm_apply (h : IsCompl p q)
      (x y z : L) (hy : y ∈ p) (hz : z ∈ q) (hx : x = y + z) :
    (LinearEquiv.ofComplSubmodules h).symm x = ⟨⟨y, hy⟩, ⟨z, hz⟩⟩ := by
  simp only [symm_apply_eq, LinearEquiv.ofComplSubmodules_apply h, hx]

theorem LinearEquiv.ofComplSubmodules_symm_apply_left (h : IsCompl p q) (x : L) (hx : x ∈ p) :
    (LinearEquiv.ofComplSubmodules h).symm x = ⟨⟨x, hx⟩, 0⟩ := by
  apply LinearEquiv.ofComplSubmodules_symm_apply
  rw [add_zero]

theorem LinearEquiv.ofComplSubmodules_symm_apply_right (h : IsCompl p q) (x : L) (hx : x ∈ q) :
    (LinearEquiv.ofComplSubmodules h).symm x = ⟨0, ⟨x, hx⟩⟩ := by
  apply LinearEquiv.ofComplSubmodules_symm_apply
  rw [zero_add]

theorem LinearEquiv.ofComplSubmodules_symm_add (h : IsCompl p q) (x : L) :
    x = ((LinearEquiv.ofComplSubmodules h).symm x).1.val + ((LinearEquiv.ofComplSubmodules h).symm x).2.val := by
  obtain ⟨y, hy, z, hz, hx⟩ := Submodule.exists_add_eq_of_codisjoint h.codisjoint x
  simp only [LinearEquiv.ofComplSubmodules_symm_apply h x y z hy hz hx.symm]
  exact hx.symm

It might very well be that something like this is already in mathlib but we just couldn't find it. Any feedback is appreciated.

[Kenny Lau]

@Paul Schwahn

1. Lean Search, "Conditions for internal direct sum" -> DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top
2. Lean Search, "DirectSum.isInternal but only for two submodules" -> DirectSum.isInternal_submodule_iff_isCompl
3. DirectSum.isInternal_submodule_iff_isCompl

/-- If a collection of submodules has just two indices, `i` and `j`, then
`DirectSum.IsInternal` is equivalent to `isCompl`. -/
theorem isInternal_submodule_iff_isCompl (A : ι → Submodule R M) {i j : ι} (hij : i ≠ j)
    (h : (Set.univ : Set ι) = {i, j}) : IsInternal A ↔ IsCompl (A i) (A j) := by

[Paul Schwahn]

That's great, thanks!

Do you think it would still be worthwhile to have LinearEquiv.ofComplSubmodules? Think of it just as API for products. In my opinion, working with a direct sum indexed over a type of cardinality two is a bit awkward, both for stating theorems (because the statements are much longer and harder to read) and for proving stuff about them (because binary products already have a lot of API, and carrying the index type around is a bit annoying).

[Kenny Lau]

@Paul Schwahn Loogle, "IsCompl, LinearEquiv":

• Submodule.prodEquivOfIsCompl :clipboard: Mathlib.LinearAlgebra.Projection
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) : (↥p × ↥q) ≃ₗ[R] E

[Paul Schwahn]

Oh wow. And LinearMap.coprod is also in mathlib. I genuinely don't know how I missed them. Thanks again!

[Notification Bot]

Paul Schwahn has marked this topic as resolved.

[Notification Bot]

Paul Schwahn has marked this topic as unresolved.

[Paul Schwahn]

On that note:

• using these theorems, I found that it might be more useful if the submodules in Submodule.prodEquivOfIsCompl and Submodule.linearProjOfIsCompl and the theorems about it were implicit arguments - I think Submodule.linearProjOfIsCompl h would be much nicer than Submodule.linearProjOfIsCompl _ _ h or p.linearProjOfIsCompl q h, especially if the submodules p and q are not single letters/words.
• there seem to be no mathlib analogues of the theorems LinearEquiv.ofComplSubmodules_symm_apply and LinearEquiv.ofComplSubmodules_symm_add from my snippet above, and I would find them useful to have.

Opinions? (I'm happy to make a PR; also please let me know if there is a better place to discuss this)

[Paul Schwahn]

Paul Schwahn said:

• there seem to be no mathlib analogues of the theorems LinearEquiv.ofComplSubmodules_symm_apply and LinearEquiv.ofComplSubmodules_symm_add from my snippet above, and I would find them useful to have.

I've made this a PR: #26462