Commit 2023-08-12 20:56 f2c3294f

View on Github →

feat: presheaf of modules over a presheaf of rings (#4670) This is extracted from the draft PR https://github.com/leanprover-community/mathlib4/pull/4116 which tries to compare this definition with the definition in terms of a presheaf in RingMod.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

added def PresheafOfModules.Hom.app

added def PresheafOfModules.Hom.comp

added theorem PresheafOfModules.Hom.ext

added def PresheafOfModules.Hom.id

added structure PresheafOfModules.Hom

added def PresheafOfModules.map

added theorem PresheafOfModules.map_apply

added theorem PresheafOfModules.map_comp

added theorem PresheafOfModules.map_id

added def PresheafOfModules.obj

added def PresheafOfModules.toPresheaf

added structure PresheafOfModules

Modified Mathlib/Algebra/Module/LinearMap.lean

added def LinearMap.id'

added theorem LinearMap.id'_coe

Modified Mathlib/Algebra/Ring/CompTypeclasses.lean

Modified Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean