Skip to content

fix: mathlib4 monoidal structure on presheaves of modules, from nightly-2026-09-05 #49

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Kha wants to merge 1 commit into from
Closed

fix: mathlib4 monoidal structure on presheaves of modules, from nightly-2026-09-05 #49

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 18 additions & 6 deletions mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,18 +150,30 @@ noncomputable instance monoidalCategory :
MonoidalCategory (PresheafOfModulesOfCommRing.{u} R) where
tensorHom_def _ _ := by ext1; apply tensorHom_def
id_tensorHom_id _ _ := by ext1; apply id_tensorHom_id
tensorHom_comp_tensorHom _ _ _ _ := by ext1; apply tensorHom_comp_tensorHom
tensorHom_comp_tensorHom _ _ _ _ := by
ext1 X
apply MonoidalCategory.tensorHom_comp_tensorHom (C := ModuleCat (R.obj X))
whiskerLeft_id M₁ M₂ := by
ext1 X
apply MonoidalCategory.whiskerLeft_id (C := ModuleCat (R.obj X))
id_whiskerRight _ _ := by
ext1 X
apply MonoidalCategory.id_whiskerRight (C := ModuleCat (R.obj X))
associator_naturality _ _ _ := by ext1; apply associator_naturality
leftUnitor_naturality _ := by ext1; apply leftUnitor_naturality
rightUnitor_naturality _ := by ext1; apply rightUnitor_naturality
pentagon _ _ _ _ := by ext1; apply pentagon
triangle _ _ := by ext1; apply triangle
associator_naturality _ _ _ := by
ext1 X
apply MonoidalCategory.associator_naturality (C := ModuleCat (R.obj X))
leftUnitor_naturality _ := by
ext1 X
apply MonoidalCategory.leftUnitor_naturality (C := ModuleCat (R.obj X))
rightUnitor_naturality _ := by
ext1 X
apply MonoidalCategory.rightUnitor_naturality (C := ModuleCat (R.obj X))
pentagon _ _ _ _ := by
ext1 X
apply MonoidalCategory.pentagon (C := ModuleCat (R.obj X))
triangle _ _ := by
ext1 X
apply MonoidalCategory.triangle (C := ModuleCat (R.obj X))

open BraidedCategory

Expand Down
Loading