Commit 2025-10-28 22:42 eaf3ffb2

View on Github →

feat(Algebra): SemimoduleCat, category of modules over semiring (#31023)

  • Introduce SemimoduleCat, the category of semimodules (mathlib's Module) over a Semiring. The new file ModuleCat/Semi.lean is copied from ModuleCat/Basic.lean. The additive/linear instances would require #28826.

Estimated changes

added structure SemimoduleCat.Hom
added theorem SemimoduleCat.coe_of
added theorem SemimoduleCat.hom_add
added theorem SemimoduleCat.hom_comp
added theorem SemimoduleCat.hom_ext
added theorem SemimoduleCat.hom_id
added theorem SemimoduleCat.hom_smul
added theorem SemimoduleCat.hom_sum
added theorem SemimoduleCat.hom_zero
added theorem SemimoduleCat.id_apply
added theorem SemimoduleCat.ofHom_id
added theorem SemimoduleCat.of_coe
added structure SemimoduleCat