← Z-module example

Index

Next: Linear maps →

---

Recall

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

• Submodule. “An $R$-submodule of $M$ is a subgroup $N$ of $M$ which is closed under the action of ring elements, i.e., $rn \in N$, for all $r \in R, n \in N$” (DummitFoote2003, §10.1 “Basic Definitions and Examples,” p. 337).

A submodule of $M$ is a subset closed under $+$, containing $0$, and closed under the scalar action. In Lean, “a subset closed under some operations” is naturally a structure bundling a predicate on M together with closure proofs. This is the same “data + proofs” idea as Group, just with the “data” being a property instead of an operation:

structure Submodule {R : Type} (Rg : Ring R) {M : Type} (Mod : Module R Rg M) where
  carrier : M → Prop
  zero_mem : carrier Mod.addGrp.toGroup.id
  add_mem : ∀ {m n : M}, carrier m → carrier n → carrier (Mod.addGrp.op m n)
  smul_mem : ∀ (r : R) {m : M}, carrier m → carrier (Mod.smul r m)

carrier : M → Prop is the subset, viewed as its membership predicate (carrier m reads “m is in the submodule”). This is the standard Lean idiom for “subobject of X”: not a Set X wrapped separately, but a predicate directly, since carrier m is a proposition usable directly as a hypothesis.

Mathematical reading. Submodule Rg Mod is a submodule $N \le M$, presented by its membership predicate $\chi_N : M \to \mathrm{Prop}$ (a subset $N = {\,m \in M \mid \chi_N(m)\,}$) together with closure proofs: $0 \in N$, $m,n \in N \Rightarrow m+n \in N$, and $r\in R,\, m\in N \Rightarrow r\cdot m \in N$. These are exactly the conditions for $N$ to be an $R$-submodule: closed under the abelian-group operations and stable under scalars. So $N$ inherits an $R$-module structure and the inclusion $N \hookrightarrow M$ is $R$-linear. Categorically this is a subobject of $M$ in $R\text{-}\mathbf{Mod}$.

Example: the submodule of even integers, as a $\mathbb{Z}$-submodule of $\mathbb{Z}$

The $\mathbb{Z}$-module structure on $\mathbb{Z}$ itself, described only in passing so far, is required first:

def intZModule : Module Int intRing Int where
  addGrp := intCommGroup
  smul := fun r m => r * m
  smul_add := by
    intro r m n
    exact Int.mul_add r m n
  add_smul := by
    intro r s m
    exact Int.add_mul r s m
  smul_smul := by
    intro r s m
    exact Int.mul_assoc r s m
  one_smul := by
    intro m
    exact Int.one_mul m

-- NOTE: `intZModule.addGrp.op`/`.id`/`.smul` are definitionally (but not
-- syntactically) equal to plain `+`/`0`/`*` on `Int` — true by `rfl`, but
-- `rw` only fires on syntactic matches, so a bare `rw [...]` (or `ring`,
-- which this book doesn't import from Mathlib anyway) would leave
-- an unsolved goal even though the underlying statement is true. `show`
-- restates the goal in its reduced (defeq) form explicitly first.
def evenSubmodule : Submodule intRing intZModule where
  carrier := fun m => ∃ k : Int, m = 2 * k
  zero_mem := ⟨0, rfl⟩
  add_mem := by
    intro m n ⟨k, hk⟩ ⟨j, hj⟩
    refine ⟨k + j, ?_⟩
    show m + n = 2 * (k + j)
    rw [hk, hj, Int.mul_add]
  smul_mem := by
    intro r m ⟨k, hk⟩
    refine ⟨r * k, ?_⟩
    show r * m = 2 * (r * k)
    rw [hk, ← Int.mul_assoc, Int.mul_comm r 2, Int.mul_assoc]

Each closure proof follows the same shape: destructure the hypothesis to expose its witness (⟨k, hk⟩ denotes “m is even, with witness k and proof hk : m = 2 * k”), then supply a new witness and discharge the resulting Int equation. zero_mem’s witness 0 makes the goal id = 2 * 0, true by rfl directly (both sides compute to 0). add_mem and smul_mem require show first to reveal the goal’s +/*-form before rw can find anything to rewrite, since Mod.addGrp.op/Mod.smul do not display as plain +/*, even though they compute to exactly that here.

Mathematical reading. This is the submodule $2\mathbb{Z} \le \mathbb{Z}$ of even integers, $2\mathbb{Z} = {\, m \mid \exists k,\ m = 2k \,}$. It’s the image of multiplication-by-$2$, and equivalently the principal ideal $(2)\trianglelefteq \mathbb{Z}$ (submodules of the $\mathbb{Z}$-module $\mathbb{Z}$ are exactly its ideals). The closure checks are the elementary facts $0 = 2\cdot 0$, $2k + 2j = 2(k+j)$, and $r\cdot(2k) = 2(rk)$, each an identity in the commutative ring $\mathbb{Z}$. The existential witnesses $0,\ k+j,\ rk$ are precisely the elements that show closure.

Mathlib equivalent. Mathlib builds the submodule generated by a set generically, using Submodule.span. Thus evenSubmodule’s three hand-written closure proofs (zero_mem/add_mem/smul_mem) become a single call, applicable to any generating set at all, not just {2}:

def evenSubmodule' : Submodule Int Int := Submodule.span Int {(2 : Int)}

example : (2 : Int) ∈ evenSubmodule' := Submodule.subset_span rfl

Submodule.span R s is, by construction, the smallest submodule containing s. Submodule.subset_span is the one fact that does all the work here: “the generators are always members”, proved once, generically, instead of the book’s custom zero_mem/add_mem/smul_mem triple for this specific subset.

---

References

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

• Dummit and Foote (DummitFoote2003), §10.1 “Basic Definitions and Examples,” p. 337 — submodules and their axioms.

---

← Z-module example

Index

Next: Linear maps →