Direct sums of modules

Recall

Formal definition cited in this section, gathered here for quick reference (full citation in the Bibliography):

Direct sum of modules. “Let $M_1, \ldots, M_k$ be a collection of $R$-modules. The collection of $k$-tuples $(m_1, \ldots, m_k)$ where $m_i \in M_i$ with addition and action of $R$ defined componentwise is called the direct product of $M_1, \ldots, M_k$ … also referred to as the (external) direct sum … denoted $M_1 \oplus \cdots \oplus M_k$” (DummitFoote2003, §10.3 “Generation of Modules, Direct Sums, and Free Modules,” p. 351, Proposition 5). D&F’s explicit universal-property discussion in this section covers free modules and tensor products, not direct sums specifically — the universal-property framing of direct sums used elsewhere in this book is its own extension of the pattern.

Given two $R$-modules $M$, $N$, their direct sum $M \oplus N$ has carrier $M \times N$, componentwise addition, and componentwise scalar action:

structure DirectSum (M N : Type) where
  fst : M
  snd : N

def directSumModule {R : Type} (Rg : Ring R) {M N : Type}
    (ModM : Module R Rg M) (ModN : Module R Rg N) :
    Module R Rg (DirectSum M N) where
  addGrp := {
    toGroup := {
      op := fun x y => ⟨ModM.addGrp.op x.fst y.fst, ModN.addGrp.op x.snd y.snd⟩
      id := ⟨ModM.addGrp.toGroup.id, ModN.addGrp.toGroup.id⟩
      inv := fun x => ⟨ModM.addGrp.toGroup.inv x.fst, ModN.addGrp.toGroup.inv x.snd⟩
      assoc := by
        intro x y z
        show DirectSum.mk _ _ = DirectSum.mk _ _
        congr 1
        · exact ModM.addGrp.toGroup.assoc x.fst y.fst z.fst
        · exact ModN.addGrp.toGroup.assoc x.snd y.snd z.snd
      id_left := by
        intro x
        show DirectSum.mk _ _ = DirectSum.mk _ _
        congr 1
        · exact ModM.addGrp.toGroup.id_left x.fst
        · exact ModN.addGrp.toGroup.id_left x.snd
      id_right := by
        intro x
        show DirectSum.mk _ _ = DirectSum.mk _ _
        congr 1
        · exact ModM.addGrp.toGroup.id_right x.fst
        · exact ModN.addGrp.toGroup.id_right x.snd
      inv_left := by
        intro x
        show DirectSum.mk _ _ = DirectSum.mk _ _
        congr 1
        · exact ModM.addGrp.toGroup.inv_left x.fst
        · exact ModN.addGrp.toGroup.inv_left x.snd
      inv_right := by
        intro x
        show DirectSum.mk _ _ = DirectSum.mk _ _
        congr 1
        · exact ModM.addGrp.toGroup.inv_right x.fst
        · exact ModN.addGrp.toGroup.inv_right x.snd
    }
    comm := by
      intro x y
      show DirectSum.mk _ _ = DirectSum.mk _ _
      congr 1
      · exact ModM.addGrp.comm x.fst y.fst
      · exact ModN.addGrp.comm x.snd y.snd
  }
  smul := fun r x => ⟨ModM.smul r x.fst, ModN.smul r x.snd⟩
  smul_add := by
    intro r x y
    show DirectSum.mk _ _ = DirectSum.mk _ _
    congr 1
    · exact ModM.smul_add r x.fst y.fst
    · exact ModN.smul_add r x.snd y.snd
  add_smul := by
    intro r s x
    show DirectSum.mk _ _ = DirectSum.mk _ _
    congr 1
    · exact ModM.add_smul r s x.fst
    · exact ModN.add_smul r s x.snd
  smul_smul := by
    intro r s x
    show DirectSum.mk _ _ = DirectSum.mk _ _
    congr 1
    · exact ModM.smul_smul r s x.fst
    · exact ModN.smul_smul r s x.snd
  one_smul := by
    intro x
    show DirectSum.mk _ _ = DirectSum.mk _ _
    congr 1
    · exact ModM.one_smul x.fst
    · exact ModN.one_smul x.snd

congr 1 is a tactic worth noting, as this is its first appearance. Given a goal f a1 a2 = f b1 b2 (here f is DirectSum.mk), congr 1 reduces it to the componentwise goals a1 = b1 and a2 = b2. This is the categorical fact that a product’s equality is checked pairwise, turned into a one-line tactic instead of a hand-unfolded Prod.ext-style lemma. Every proof obligation above genuinely is two independent facts, one from M and one from N, glued together by the direct-sum’s product structure. congr 1 is the right tool exactly because it exposes that independence directly, instead of hiding it inside a single opaque equality on pairs. Note the show DirectSum.mk _ _ = DirectSum.mk _ _ line before each congr 1: without it, the goal is stated in terms of the anonymous-constructor lambda (op := fun x y => ⟨...⟩) rather than the visible DirectSum.mk application. congr 1 cannot reliably split a goal it does not recognize as “one constructor applied to arguments on both sides” — a real gap that the compiler catches immediately if the show line is left out.

Mathematical reading. This builds the direct sum $M \oplus N$: its carrier is the product $M \times N$, with all structure defined componentwise — $(m,n) + (m’,n’) = (m+m’,\, n+n’)$, $0 = (0,0)$, $-(m,n) = (-m,-n)$, and $r\cdot(m,n) = (r\cdot m,\, r\cdot n)$. Every axiom holds because it holds in each coordinate independently, which is exactly what congr 1 exposes: an equation of pairs splits into one equation in $M$ and one in $N$. For finitely many summands the direct sum $M \oplus N$ is both a product and a coproduct at once in $R\text{-}\mathbf{Mod}$: the projections $\pi_M, \pi_N$ and inclusions $\iota_M, \iota_N$ satisfy $\pi_M\iota_M = \mathrm{id}$, $\pi_N\iota_N = \mathrm{id}$, $\pi_M\iota_N = 0$, and $\iota_M\pi_M + \iota_N\pi_N = \mathrm{id}$.

graph LR
    M -->|iota_M| MN["M ⊕ N"]
    MN -->|pi_M| M
    N -->|iota_N| MN
    MN -->|pi_N| N

A concrete instance: $\mathbb{Z} \oplus \mathbb{Z}$

Instantiating the generic construction requires nothing beyond supplying two modules — here, intZModule twice.

def zSquaredModule := directSumModule intRing intZModule intZModule

#eval (zSquaredModule.addGrp.op ⟨2, 3⟩ ⟨10, 20⟩ : DirectSum Int Int)
-- { fst := 12, snd := 23 }, i.e. (2,3) + (10,20) = (12,23)

#eval (zSquaredModule.smul 5 ⟨2, 3⟩ : DirectSum Int Int)
-- { fst := 10, snd := 15 }, i.e. 5 · (2,3) = (10,15)

Both outputs are exactly the componentwise formulas from the mathematical reading above, computed rather than merely asserted.

Mathlib equivalent. The book builds DirectSum/directSumModule field by field (five group axioms, four module axioms, each split componentwise via congr 1). Mathlib already gives the ordinary product type M × N a Module R instance directly. There is no DirectSum wrapper to define at all:

example {M N : Type*} [AddCommGroup M] [AddCommGroup N]
    [Module Int M] [Module Int N] : Module Int (M × N) := inferInstance

#eval ((2, 3) + (10, 20) : Int × Int)     -- (12, 23)
#eval ((5 : Int) • ((2, 3) : Int × Int))   -- (10, 15)

These are the same componentwise formulas as zSquaredModule’s #evals above. But Prod’s AddCommGroup/Module instances (and the componentwise +/• they provide) are already in the library, built once for any two additive groups or modules, instead of assembled here for Int and Int specifically.

The first projection $\pi_1 : \mathbb{Z}\oplus\mathbb{Z} \to \mathbb{Z}$, one of the defining maps from the product/coproduct structure above, is itself a LinearMap (previous section), built directly from DirectSum’s own field accessor:

def proj1 : LinearMap intRing zSquaredModule intZModule where
  toFun := fun x => x.fst
  map_add := by intro x y; rfl
  map_smul := by intro r x; rfl

#eval proj1.toFun ⟨7, 100⟩   -- 7

Both proof obligations are rfl directly: zSquaredModule.addGrp.op unfolds to componentwise addition (by the construction two sections back), so taking .fst of a sum is definitionally the same as summing the .fsts. No arithmetic argument is needed, only unfolding.

Mathlib equivalent, continued. The projection proj1 is, again, not something that needs to be built. Mathlib’s LinearMap.fst already is $\pi_1$, generic over any two modules over any ring:

def proj1' : (Int × Int) →ₗ[Int] Int := LinearMap.fst Int Int Int

#eval proj1' (7, 100)   -- 7

References

Full citations in the Bibliography. Formal definitions are gathered in Recall, above.

Dummit and Foote (DummitFoote2003), §10.3 “Generation of Modules, Direct Sums, and Free Modules,” pp. 351–353, Proposition 5 — direct sums of modules, internal/external direct-sum equivalence.

← Linear maps

Index

Next: Exercises →