enriched cotensors

Stream: Infinity-Cosmos

[Daniel Carranza]

I have some code on enriched cotensors that I would like to merge into the infinity-cosmos repository. How should I go about doing this?

Currently, I have the definition of V-cotensors in a V-category, and a proof that if a V-category admits V-cotensors then these form an enriched bifunctor. There are also some additional definitions such as the opposite V-category and the tensor product of V-categories

[Emily Riehl]

@Daniel Carranza why don't you create a new folder called "Enriched" under "ForMathlib/CategoryTheory" (to mirror the mathlib directory structure) and create a file called Cotensors.lean in there. Eventually we'll most likely delete (or replace) the file "Cotensors.lean" that is currently under "ForMathlib/AlgebraicTopology/SimplicialCategory" but to start it might be nice to be able to directly compare them.

[Emily Riehl]

To add your code, the best thing is to branch the infinitycosmos repository and send us a PR. We're not nearly as picky as mathlib, so I'll most likely merge it right away for us to start experimenting with, unless anyone else has a better idea for the workflow.

[Daniel Carranza]

A PR has been created with the changes:
https://github.com/emilyriehl/infinity-cosmos/pull/33

Any and all suggestions from folks are strongly encouraged, since the code is in VERY rough shape at the moment. Thank you so much for your help!

[Daniel Carranza]

Thanks for merging this PR @Emily Riehl! Unfortunately (and embarrassingly!), the PR contained errors in the Cotensors.lean file caused by changing an argument in a different file to be implicit. These errors have been corrected in a new PR: https://github.com/emilyriehl/infinity-cosmos/pull/35

Sorry for the trouble!

[Kevin Buzzard]

I've merged PRs which broke my build in the FLT project and I was never too bothered about this, until Kim Morrison explained to me that this hinders progress because when other people try to make PRs the build is broken and this confuses them. Since I understood this properly I've always been careful to only merge stuff with a green tick and I think that we even have FLT set up so that it's only possible to merge PRs which don't break the build? I don't know anything about how CI is set up in this project but you might want to get some CI whizz to make this project work like that too if it doesn't already.

[Emily Riehl]

@Kevin Buzzard where do I find such a CI wiz? This is way above my paygrade... (The early merge was my fault too.)

[Pietro Monticone]

I can do it later

[Pietro Monticone]

Unfortunately I can't make the changes directly because I'm not the repo owner, but here is what you need to do:

1. Go to https://github.com/emilyriehl/infinity-cosmos/settings
2. Left sidebar: Code and automation > Rules > Rulesets
3. Ruleset Name: main
4. Enforcement status: Active
5. Bypass list: add bypass > select Repository admin, Maintain, Write
6. Targets: add target > include default branch
7. Check Require status checks to pass
8. Add checks: write build_project and check it.
9. Click on Create

Screenshot 2024-11-08 at 01.04.42.png

Screenshot 2024-11-08 at 01.04.50.png

Screenshot 2024-11-08 at 01.05.02.png

[Emily Riehl]

Thanks to @Pietro Monticone this should be all set up now!

[Pietro Monticone]

I can confirm it works as expected. See this PR for example https://github.com/emilyriehl/infinity-cosmos/pull/36

[Emily Riehl]

@Daniel Carranza when you have a minute could you check out the new PR by @Pietro Monticone which golfs a few of your proofs? If you approve, we can go ahead and merge.

Another thing which is not urgent: I'd also be grateful for advice about what to do with the enriched opposite categories, which are now in mathlib. I didn't follow the discussion closely while it was being reviewed.

[Daniel Carranza]

The new PR looks great - thank you @Pietro Monticone for the improvement!

I updated my local repo to the newest version of mathlib, and it looks like the only file that requires changes is Cotensors.lean, which only requires small re-writes to use the type V^op as opposed to eOpposite V V. I can make the changes to the file in a PR if the current version of the repo has an updated installation of mathlib.

(For reference, the relevant changes in mathlib are from this PR: https://github.com/leanprover-community/mathlib4/pull/19483 )

[Pietro Monticone]

Ok @Daniel Carranza, so we can merge cosmos#52 and then bump Mathlib in a new PR.

[Daniel Carranza]

I've created a PR with the changes: https://github.com/emilyriehl/infinity-cosmos/pull/56

I tried to delete the Opposite.lean file currently in the ForMathLib folder, but there was an error that I don't know how to fix (see here for the error message: https://github.com/emilyriehl/infinity-cosmos/pull/56/checks?check_run_id=33822523324 ). Instead, I have removed all code in the file and replaced it with a comment. If anyone knows how to fix this problem, I'm more than happy to update the PR - thank you!

[Kevin Buzzard]

It looks to me like there's a file/files trying to import the file you deleted. Search the project for import InfinityCosmos.ForMathlib.CategoryTheory.Enriched.Opposite and delete the import too?

[Pietro Monticone]

Yes, the import InfinityCosmos.ForMathlib.CategoryTheory.Enriched.Opposite was left in the build file InfinityCosmos.lean. Pushed the fix now.

[Emily Riehl]

Thanks @Pietro Monticone and @Daniel Carranza. Just merged this.