Theorems · Inductive type · category theory

SemimoduleCat

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

The category of R-semimodules and their morphisms. Note that in the case of R = ℕ, we can not impose here that the ℕ-multiplication field from the module structure is defeq to the one coming from the isAddCommMonoid 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.Semi

Cited by

108 results in Mathlib

Foundations

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

Assumes

Semiring