Left submodules over commutative rings

Content created by Louis Wasserman.

Created on 2026-01-30.
Last modified on 2026-01-30.

module linear-algebra.left-submodules-commutative-rings where
Imports 
open import commutative-algebra.commutative-rings

open import foundation.propositions
open import foundation.universe-levels

open import linear-algebra.left-modules-commutative-rings
open import linear-algebra.left-submodules-rings
open import linear-algebra.subsets-left-modules-commutative-rings

Idea

A left submodule of a left module M over a commutative ring R is a subset of M that is closed under addition and multiplication by a scalar from R.

Definition

module _
  {l1 l2 l3 : Level}
  (R : Commutative-Ring l1)
  (M : left-module-Commutative-Ring l2 R)
  (S : subset-left-module-Commutative-Ring l3 R M)
  where

  is-left-submodule-prop-Commutative-Ring : Prop (l1 ⊔ l2 ⊔ l3)
  is-left-submodule-prop-Commutative-Ring =
    is-left-submodule-prop-Ring (ring-Commutative-Ring R) M S

  is-left-submodule-Commutative-Ring : UU (l1 ⊔ l2 ⊔ l3)
  is-left-submodule-Commutative-Ring =
    type-Prop is-left-submodule-prop-Commutative-Ring

left-submodule-Commutative-Ring :
  {l1 l2 : Level} (l3 : Level) (R : Commutative-Ring l1) →
  left-module-Commutative-Ring l2 R → UU (l1 ⊔ l2 ⊔ lsuc l3)
left-submodule-Commutative-Ring l3 R =
  left-submodule-Ring l3 (ring-Commutative-Ring R)

module _
  {l1 l2 l3 : Level}
  (R : Commutative-Ring l1)
  (M : left-module-Commutative-Ring l2 R)
  (S : left-submodule-Commutative-Ring l3 R M)
  where

  left-module-left-submodule-Commutative-Ring :
    left-module-Commutative-Ring (l2 ⊔ l3) R
  left-module-left-submodule-Commutative-Ring =
    left-module-left-submodule-Ring (ring-Commutative-Ring R) M S

Recent changes