Prove2Me

p×q≅p×qp \times q \cong p \times q: the product submodule as a product module

Definition
submodule_prodEquiv

by t4v1 · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebralinear-algebra

Let RR be a ring and let MM, NN be RR-modules. For submodules p⊆Mp \subseteq M and q⊆Nq \subseteq N, Mathlib's Submodule.prod forms the submodule p×q⊆M×Np \times q \subseteq M \times N. This file records the RR-linear isomorphism

p×q  ≅  p×q,p \times q \;\cong\; p \times q,

between the submodule p×qp \times q of M×NM \times N, regarded as a module in its own right, and the product module of pp and qq. The map sends ((m,n),h)((m,n), h) to ((m,h1),(n,h2))((m, h_1), (n, h_2)), where h=(h1,h2)h = (h_1, h_2) witnesses m∈pm \in p and n∈qn \in q; its inverse reassembles the pair. Every structure field, including linearity and the two inverse laws, holds by rfl. Two simp lemmas describe the map and its inverse pointwise.

Together with Submodule.quotientProdEquiv (the analogous statement for quotients) it lets a rank computation on a direct sum f⊕gf \oplus g of linear maps be split into one on ff and one on gg: for instance ker⁡(f⊕g)=ker⁡f×ker⁡g\ker(f \oplus g) = \ker f \times \ker g as modules.

Definition code
import Mathlib.LinearAlgebra.Prod

/-!
The submodule `p × q` of `M × N`, viewed as a module in its own right, is the
product module `p × q`. Every structure field is definitional.
-/

namespace Submodule

variable {R M N : Type*} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

/-- The submodule `p × q` of `M × N`, viewed as a module, is the product of `p`
and `q`. -/
def prodEquiv (p : Submodule R M) (q : Submodule R N) : p.prod q ≃ₗ[R] p × q where
  toFun z := (⟨z.1.1, z.2.1⟩, ⟨z.1.2, z.2.2⟩)
  invFun w := ⟨(w.1.1, w.2.1), ⟨w.1.2, w.2.2⟩⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  left_inv _ := rfl
  right_inv _ := rfl

@[simp]
theorem prodEquiv_apply (p : Submodule R M) (q : Submodule R N) (z : p.prod q) :
    prodEquiv p q z = (⟨z.1.1, z.2.1⟩, ⟨z.1.2, z.2.2⟩) := rfl

@[simp]
theorem prodEquiv_symm_apply (p : Submodule R M) (q : Submodule R N) (w : p × q) :
    (prodEquiv p q).symm w = ⟨(w.1.1, w.2.1), ⟨w.1.2, w.2.2⟩⟩ := rfl

end Submodule
Source
Drafted as a Mathlib contribution for `Mathlib/LinearAlgebra/Prod.lean`, beside `Submodule.prod`; source repository: github.com/tavi-halmaghi (MorseFloer project, `contrib/Mathlib/LinearAlgebra/Prod.lean`).

View graph