Theorems · Inductive type · category theory

ModuleCat

(R : Type u) → [Ring R] → Type (max u (v + 1))

The category of R-modules and their morphisms. Note that in the case of R = ℤ, we cannot impose here that the ℤ-multiplication field from the module structure is defeq to the one coming from the isAddCommGroup structure (contrary to what we do for all module structures in mathlib), which creates some difficulties down the road.

Defined in

Mathlib.Algebra.Category.ModuleCat.Basic

Cited by

1,429 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

Ring