fix: mathlib4 monoidal structure on presheaves of modules, from nightly-2026-09-05 - #49
Closed
Kha wants to merge 1 commit into
Closed
fix: mathlib4 monoidal structure on presheaves of modules, from nightly-2026-09-05#49Kha wants to merge 1 commit into
Kha wants to merge 1 commit into
Conversation
`downstream: update repo mathlib4` brought in mathlib master's refactor of
`Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean` onto the
`PresheafOfModulesOfCommRing R` abbreviation, whose `obj X` is a
`ModuleCat (R.obj X)` while the underlying `PresheafOfModules.Hom.app X` still
lands in `ModuleCat ((R ⋙ forget₂ CommRingCat RingCat).obj X)` — the same ring
bundled twice. Since `lean4#14624` an instance is only assigned when its type
matches the expected one at `.instances` transparency, and seeing that those two
agree needs `⋙` unfolded, which is `@[implicit_reducible]`; that is the gap the
file's own `#adaptation_note` already describes. So `apply` could no longer infer
`C` in six fields of the `monoidalCategory` instance:
error: Tactic `apply` failed: could not unify the conclusion of
`@tensorHom_comp_tensorHom`
(?f₁ ⊗ₘ ?f₂) ≫ (?g₁ ⊗ₘ ?g₂) = ?f₁ ≫ ?g₁ ⊗ₘ ?f₂ ≫ ?g₂
with the goal
((x✝³ ⊗ₘ x✝²) ≫ (x✝¹ ⊗ₘ x✝)).app X✝ = (x✝³ ≫ x✝¹ ⊗ₘ x✝² ≫ x✝).app X✝
and the resulting instance-with-metavariables took `symmetricCategory`, the
`braiding_*_app` lemmas and the two `PreservesColimitsOfSize` instances with it.
Pass `C` explicitly, as the same instance already does for `whiskerLeft_id` and
`id_whiskerRight`, which upstream needed for the same reason. Attribution
checked, not guessed: `set_option
backward.isDefEq.respectTransparency.instanceSearchTypes false` alone makes the
unmodified file compile, while `backward.isDefEq.respectTransparency` and
`backward.isDefEq.respectTransparency.types` do not.
Verified: `lake build Mathlib Archive Counterexamples Wanted --wfail`,
`lake test --iofail` and `lake lint`.
Contributor
Build report for fix: mathlib4 monoidal structure on presheaves of modulesStayed red
Stayed green
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
masteris red onnightly-2026-09-05(run34006523467). Today's
downstream: update repo mathlib4(87765e8b) brought in a second, independentmathlib4failure that the
rwaparse error of #48 had been masking — here and inmathlib4-nightly-testing, whose own CI stops at that same parse error, so it is not visibleupstream either. This PR fixes that one failure;
masteralso needs #48 and theversoblocker below, so it will not by itself make the run green.
mathlib4—MonoidalCategoryfields can no longer inferCthroughPresheafOfModulesOfCommRingmathlib master refactored
Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.leanonto thePresheafOfModulesOfCommRing Rabbreviation (mathlib47974e751, merged intonightly-testingan hour before the run). Its
obj Xis aModuleCat (R.obj X), while the underlyingPresheafOfModules.Hom.app Xstill lands inModuleCat ((R ⋙ forget₂ CommRingCat RingCat).obj X)— the same ring bundled twice. Since lean4#14624 an instance is only assigned when its type
matches the expected one at
.instancestransparency, and seeing that those two agree requiresunfolding
⋙, which is@[implicit_reducible]. That is exactly the gap the file's own#adaptation_note— written when mathlib adapted to that very PR — describes.So
applycould no longer pickCitself in six fields of themonoidalCategoryinstance:and the resulting instance-with-metavariables took
symmetricCategory, thebraiding_*_applemmas and the two
PreservesColimitsOfSizeinstances with it — 18 errors from the one cause.Cis now passed explicitly, exactly as the same instance already does forwhiskerLeft_idandid_whiskerRight, which upstream needed for the same reason on the release toolchain. Theattribution was checked rather than guessed:
set_option backward.isDefEq.respectTransparency.instanceSearchTypes falsealone (the flag lean4#14624 added)makes the unmodified file compile, while
backward.isDefEq.respectTransparencyandbackward.isDefEq.respectTransparency.typesdo not.Expect more of these: mathlib master builds on a release toolchain (
v4.34.0-rc2), so new mastercode that trips
instanceSearchTypesis invisible upstream until it reaches a nightly here.Verified
With #48's four files applied locally, since
mathlib4does not build at all without them:mathlib4--wfail)--iofail)cslib--wfail --iofail)--wfail --iofail)repltest/MathlibNot fixed here
rwaparse error inMathlib.Tactic.TacticAnalysis.Declarationsand thecslibrwasuggestion. It still appliesto
masterbyte-for-byte. This PR is independent of it — different files, no conflict — but CIon this branch alone will still show that parse error.
verso, andverso-slides,verso-web-componentsand the criticalreference-manualskipped behind it, are red on the unchanged
.downstream/blocker, fifth day:Updater.fixup_subrepo_dependencieswrites the in-treesubversointo the.lake/package-overrides.jsonof verso's nested test projects, which pinleanprover/lean4:v4.31.0and therefore rewritesubverso/.lake/buildmid-build.fixup_subrepo_toolchain, one function above, has the content guard this one lacks. Unattendedruns may not touch
.downstream/. fix: restore subverso definition sites, unbreaking verso-slides #41 fixes the subverso half of that story.🤖 Generated with Claude Code