Function left modules on rings

Content created by Louis Wasserman.

Created on 2026-04-26.
Last modified on 2026-04-26.

module linear-algebra.function-left-modules-rings where
Imports 
open import foundation.universe-levels

open import linear-algebra.dependent-products-left-modules-rings
open import linear-algebra.left-modules-rings

open import ring-theory.rings

Idea

Given a type X and a left module M over a ring R, the functions X → M form a left module over R.

Definition

module _
  {l1 l2 l3 : Level}
  (R : Ring l1)
  (M : left-module-Ring l2 R)
  (X : UU l3)
  where

  function-left-module-Ring : left-module-Ring (l2 ⊔ l3) R
  function-left-module-Ring = Π-left-module-Ring R X (λ _ → M)

Properties

The functions X → R form a left module over R

function-left-module-ring-Ring :
  {l1 l2 : Level} (R : Ring l1) → UU l2 → left-module-Ring (l1 ⊔ l2) R
function-left-module-ring-Ring R =
  function-left-module-Ring R (left-module-ring-Ring R)

Recent changes