Skip to content

[Merged by Bors] - feat(Algebra): SemimoduleCat, category of modules over semiring#31023

Closed
alreadydone wants to merge 3 commits intoleanprover-community:masterfrom
alreadydone:Semimodule_Cat
Closed

[Merged by Bors] - feat(Algebra): SemimoduleCat, category of modules over semiring#31023
alreadydone wants to merge 3 commits intoleanprover-community:masterfrom
alreadydone:Semimodule_Cat

Conversation

@alreadydone
Copy link
Copy Markdown
Contributor

@alreadydone alreadydone commented Oct 28, 2025 •
edited
Loading

Open in Gitpod

@alreadydone alreadydone added t-category-theory Category theory t-algebra Algebra (groups, rings, fields, etc) labels Oct 28, 2025
@alreadydone alreadydone changed the title feat(Algebra): SemimoduleCat, category of modules over semiring feat(Algebra): SemimoduleCat, category of modules over semiring Oct 28, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 28, 2025 •
edited
Loading

PR summary 6c19380648

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
200 files Mathlib.Algebra.BrauerGroup.Defs Mathlib.Algebra.Category.AlgCat.Basic Mathlib.Algebra.Category.AlgCat.Limits Mathlib.Algebra.Category.AlgCat.Monoidal Mathlib.Algebra.Category.AlgCat.Symmetric Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.Algebra.Category.BialgCat.Basic Mathlib.Algebra.Category.BialgCat.Monoidal Mathlib.Algebra.Category.CoalgCat.Basic Mathlib.Algebra.Category.CoalgCat.ComonEquivalence Mathlib.Algebra.Category.CoalgCat.Monoidal Mathlib.Algebra.Category.CommAlgCat.Basic Mathlib.Algebra.Category.CommAlgCat.FiniteType Mathlib.Algebra.Category.CommAlgCat.Monoidal Mathlib.Algebra.Category.CommBialgCat Mathlib.Algebra.Category.ContinuousCohomology.Basic Mathlib.Algebra.Category.FGModuleCat.Abelian Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Algebra.Category.FGModuleCat.Colimits Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Algebra.Category.Grp.Images Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.Grp.IsFinite Mathlib.Algebra.Category.Grp.LargeColimits Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.Grp.Ulift Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Algebra.Category.HopfAlgCat.Basic Mathlib.Algebra.Category.HopfAlgCat.Monoidal Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.ExteriorPower Mathlib.Algebra.Category.ModuleCat.FilteredColimits Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Category.ModuleCat.Topology.Basic Mathlib.Algebra.Category.ModuleCat.Topology.Homology Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Module.CharacterModule Mathlib.Algebra.Module.PID Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Injective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Adjunction.Additive Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.CategoryTheory.Linear.Yoneda Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Condensed.AB Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Explicit Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.FieldTheory.Galois.NormalBasis Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.MulChar.Duality Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.Coinduced Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Functoriality Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.RepresentationTheory.Homological.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro Mathlib.RepresentationTheory.Homological.GroupHomology.Basic Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro Mathlib.RepresentationTheory.Homological.Resolution Mathlib.RepresentationTheory.Induced Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Rep Mathlib.RepresentationTheory.Tannaka Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.Tensor Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.Morita.Basic Mathlib.RingTheory.PicardGroup Mathlib.RingTheory.Regular.Category Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Unramified.LocalRing Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Successor Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Topology.Sheaves.MayerVietoris
 1
Mathlib.Algebra.Category.ModuleCat.Semi (new file) 734

Declarations diff

+ Hom
+ Hom.Simps.hom
+ Hom.hom
+ Hom.hom₂
+ Hom.hom₂_ofHom₂
+ Hom.instModule
+ Iso.conj_eq_conj
+ Iso.homCongr_eq_arrowCongr
+ LinearEquiv.toModuleIsoₛ
+ LinearMap.comp_id_semiModuleCat
+ LinearMap.id_semiModuleCat_comp
+ SemimoduleCat
+ coe_of
+ comp_apply
+ equivalenceSemimoduleCat
+ forget_map
+ forget_obj
+ forget₂_map
+ forget₂_obj
+ forget₂_obj_moduleCat_of
+ hasForgetToAddCommMonoid
+ homAddEquiv
+ homEquiv
+ homLinearEquiv
+ hom_add
+ hom_bijective
+ hom_comp
+ hom_ext
+ hom_id
+ hom_injective
+ hom_inv_apply
+ hom_nsmul
+ hom_ofHom
+ hom_smul
+ hom_sum
+ hom_surjective
+ hom_zero
+ hom_zsmul
+ id_apply
+ instance : (forget (SemimoduleCat.{v} R)).ReflectsIsomorphisms
+ instance : (forget₂ (SemimoduleCat.{v} R) AddCommMonCat).Additive where -/
+ instance : (forget₂ (SemimoduleCat.{v} R) AddCommMonCat.{v}).ReflectsIsomorphisms
+ instance : Add (M ⟶ N)
+ instance : AddCommMonoid (M ⟶ N)
+ instance : CoeSort (SemimoduleCat.{v} R) (Type v)
+ instance : ConcreteCategory (SemimoduleCat.{v} R) (· →ₗ[R] ·)
+ instance : HasZeroMorphisms (SemimoduleCat.{v} R)
+ instance : HasZeroObject (SemimoduleCat.{v} R)
+ instance : Inhabited (SemimoduleCat R)
+ instance : Linear S (SemimoduleCat.{v} S) := SemimoduleCat.Algebra.instLinear -/
+ instance : Presemiadditive (SemimoduleCat.{v} R)
+ instance : SMul S (M ⟶ N)
+ instance : Zero (M ⟶ N)
+ inv_hom_apply
+ isZero_iff_subsingleton
+ isZero_of_iff_subsingleton
+ isZero_of_subsingleton
+ linearEquivIsoModuleIsoₛ
+ moduleCategory
+ of
+ ofHom
+ ofHom_apply
+ ofHom_comp
+ ofHom_hom
+ ofHom_id
+ ofHom₂
+ ofHom₂_hom₂
+ ofSelfIso
+ of_coe
+ subsingleton_of_isZero
+ toLinearEquivₛ
++ instance : SMul ℕ (M ⟶ N)

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@alreadydone alreadydone mentioned this pull request Oct 28, 2025
Closed
1 task
jcommelin
jcommelin reviewed Oct 28, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 28, 2025

✌️ alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 28, 2025
alreadydone and others added 2 commits October 28, 2025 23:25
@alreadydone @jcommelin
docstring for equivalence with ModuleCat
c32fb38 
Co-authored-by: Johan Commelin <johan@commelin.net>
@alreadydone
100 chars
94f12fa 
Fix formatting of the comment for clarity.
@alreadydone
Copy link
Copy Markdown
Contributor Author

alreadydone commented Oct 28, 2025

Thanks 🎉
bors r+

mathlib-bors bot pushed a commit that referenced this pull request Oct 28, 2025
@alreadydone
feat(Algebra): SemimoduleCat, category of modules over semiring (#3…
eaf3ffb 
…1023)

+ 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.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 28, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra): SemimoduleCat, category of modules over semiring [Merged by Bors] - feat(Algebra): SemimoduleCat, category of modules over semiring Oct 28, 2025
@mathlib-bors mathlib-bors bot closed this Oct 28, 2025
@alreadydone alreadydone deleted the Semimodule_Cat branch October 28, 2025 23:27
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Nov 7, 2025
@alreadydone @BeibeiX0
feat(Algebra): SemimoduleCat, category of modules over semiring (le…
991f02d 
…anprover-community#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 leanprover-community#28826.
@alreadydone alreadydone mentioned this pull request Nov 14, 2025
Closed
2 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@alreadydone @jcommelin