Dependent products of left modules over commutative rings

Content created by Louis Wasserman.

Created on 2025-09-09.
Last modified on 2025-09-09.

module linear-algebra.dependent-products-left-modules-commutative-rings where
Imports 
open import commutative-algebra.commutative-rings

open import foundation.function-extensionality
open import foundation.universe-levels

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

Idea

Given a commutative ring R and a family of left modules Mᵢ over R indexed by i : I, the dependent product Π (i : I) Mᵢ is a left module over R.

Definition

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

  Π-left-module-Commutative-Ring : left-module-Commutative-Ring (l2 ⊔ l3) R
  Π-left-module-Commutative-Ring =
    Π-left-module-Ring (ring-Commutative-Ring R) I M

Recent changes