Month in Mathlib

Stream: mathlib4

[Yaël Dillies]

This is some not-so-advanced warning that I will write the Month in Mathlib blogpost for May. Please reply to this thread with cool things you have done/heard about that made it to master this month!

[Yaël Dillies]

I will personally mention two projects of mine

• Roth's theorem on arithmetic progressions
• The import untangling of low level files

[Michael Rothgang]

Do linter/CI changes count? Would performance improvements count?
Must they have been landed or is there also some mention of in-progress items? I compiled a list of those for the past weeks as I'm exhilarated by the movement on this front, let me know to what extent this is in scope.

[Johan Commelin]

In the past I think we only listed PRs that were merged in that particular month

[Rémy Degenne]

Thanks for volunteering! Could that be a "last few months in Mathlib", since there were no other recent blog posts of that type? It's ok if you don't want to: I understand that it would increase the amount of work you need to do.
If that's fine, then #10603 might be worth mentioning (landed April 16).

Also the recent work of @Sébastien Gouëzel on Fourier transform should probably be mentioned. It would be good if we manage to merge the final PR #12144 before the end of the month.

[Yaël Dillies]

I'm happy to cover previous months too, but I would rather do that in several Months in Mathlib than trying to lump everything together. What do people think?

[Yaël Dillies]

Johan Commelin said:

In the past I think we only listed PRs that were merged in that particular month

+- a few days

[Yaël Dillies]

Michael Rothgang said:

Do linter/CI changes count?

Anything that changes people's experience using mathlib is worth mentioning. Eg I will definitely mention #13271

[Dagur Asgeirsson]

Light condensed sets landed in May: #11586

[Kevin Buzzard]

feat: Lie algebra root spaces are 1-dimensional (mathlib4#12937) was May.

feat(Algebra/Category/ModuleCat): the category of presheaves of modules is abelian (mathlib4#12721)

Eisenstein series uniform convergence (mathlib4#10377)

feat(Condensed): light condensed objects (mathlib4#11586)

feat(Algebra/Lie): existence of Cartan subalgebras (mathlib4#12297)

[Rémy Degenne]

Some PRs that got several reactions in the rss channel: #12917, #12937, #10377, #12619

[Yaël Dillies]

Also the Month in Mathlib blog post can't go into much detail about anything, so we should take the habit of writing longer blog posts about specific topics more often.

[Johan Commelin]

feat(Algebra/Lie/Weights): The root system of a lie algebra. (mathlib4#13307)

[Yaël Dillies]

Btw my timeline for this blogpost is that my exams end on the 10th of June, so hopefully I'll have a draft ready (at least for May, don't know about earlier months) by mid-June.

[Anne Baanen]

feat: port cc tactic (3/3) (mathlib4#5938)

@Pol'tta / Miyahara Kō did a heroic porting effort for getting the cc tactic into Lean 4

[Johan Commelin]

rss-bot said:

feat: the derived category of an abelian category (mathlib4#11806)

The derived category of an abelian category is defined and it is shown that it is a triangulated category.

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Authored-by: joelriou (commit)

[Rida Hamadani]

rss-bot said:

feat: Define Hamiltonian paths and cycles (mathlib4#7102)

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Co-authored-by: Linus Sommer
Co-authored-by: Lode Vermeulen

Co-authored-by: Lode <lode685@gmail.com>
Co-authored-by: Linus <95619282+linus-md@users.noreply.github.com>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Co-authored-by: Doga Can Sertbas <dogacan.sertbas@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Authored-by: LodeVermeulen (commit)

[Eric Wieser]

Looks like @Rishi Mehta somehow got dropped from the list of authors there!

[Rida Hamadani]

I wonder why did that happen, even though Rishi is the author of the PR

[Richard Copley]

Also the Author: of the commit, so no need to be listed in a Co-authored-by: line.

[Eric Wieser]

He's not the author of the commit the bors merged; this is a bug in bors that affects any PR whose first commit is by a different author to the PR

[Richard Copley]

This one? (He is the author of the PR, in this case.)

git merge-base --is-ancestor b4911b22 origin/master && git log -n1 b4911b22

[Michael Rothgang]

A few more CI-related changes which could be worth mentioning:

• the globalAttributeIn linter, which removes a foot-gun (and uncovered a few bugs in mathlib)
• the mk_all script which has landed; can use this locally (draw-back: seems to not work in Windows yet, for reasons unrelated to this script)
• all occurrences of the refine' tactic have been removed: in almost all cases, use refine or apply instead

[Yaël Dillies]

@Michael Rothgang, is refine' linted against now? I couldn't figure it out from a quick zuliping

[Rida Hamadani]

Not yet, this has passed lint just now.

[Yaël Dillies]

Oh okay, will change the phrasing then!

[Damiano Testa]

The linter is #11884, I just merged master.

It has no mechanism to test whether a replacements of refine' with refine could work (I implemented that logic to an autocorrecting branch). I am not sure whether a linter that actually enforces no use at all of refine' is desired, though.

[Yaël Dillies]

I have now opened blog#76. I'm off until this evening, so feel free to help out!

[Yaël Dillies]

Please at this stage do not remove any PR link from the file, but only move the interesting ones from the list at the bottom into the categories at the top

[Ruben Van de Velde]

Might mention FLT starting up

[Yaël Dillies]

Sure. What were the FLT-related PRs in May?

[Yaël Dillies]

@Joël Riou, could you write the paragraph about your work on derived categories? I tried writing something but there are so many PRs of yours and I know so little about the maths that it's probably terribly written.

[Patrick Massot]

@Jireh Loreaux and @Anatole Dedecker should we have a paragraph about functional calculus or is it too early?

[Patrick Massot]

I am also surprised there is not more analytic number theory, and Coxeter group stuff, but maybe this wasn’t in May or is not finished.

[Patrick Massot]

What about #12923 for instance?

[Jireh Loreaux]

If it's okay, I'll probably write a separate blog post about the continuous functional calculus, but also some of it landed in June.

[Patrick Massot]

A separate blog post is much more than ok, it would be great!

[Patrick Massot]

But we could still have a line in a monthly recap linking to the separate blog post. That can be in June of course if there are June PRs involved.

[Yaël Dillies]

Yes. Even if you are planning to write a more detailed, please add a recap to Month in Mathlib so that it stays somewhat exhaustive.

[Joël Riou]

Yaël Dillies said:

Joël Riou, could you write the paragraph about your work on derived categories? I tried writing something but there are so many PRs of yours and I know so little about the maths that it's probably terribly written.

I have added a suggestion of paragraph. I hope the syntax is ok.

[Yaël Dillies]

Thanks Joël and Oliver for contributing the paragraphs! @Sébastien Gouëzel, I would greatly appreciate a paragraph about the Fourier transform if you have time :pray:

[Yaël Dillies]

@Dagur Asgeirsson, could you write the paragraph about condensed sets here?

[Yaël Dillies]

Argh! The monthly-blog.sh script returns all PRs closed since the start of the month, but not until the end of the month. So I accidentally caught a bunch of June PRs :sad:

[Yaël Dillies]

If anybody knows sed, here are the two lines that caused me trouble:

git log --pretty=oneline --abbrev-commit --since="1 ${monthnames_uc[$month]} $year" | tac |
sed 's|\([^ ]*\) \(.*\) (#\([0-9]*\))|* [PR #\3](https://github.com/leanprover-community/mathlib4/pull/\3) :: \2|'

[Damiano Testa]

That sed command seems to select:

• [chars not separated by space] -- call it \1, the short hash
• a space
• anything else until a space -- call it \2, the PR title
• #[numbers] -- call it \3, the PR number

[Yaël Dillies]

Isn't --since="1 ${monthnames_uc[$month]} the problem?

[Damiano Testa]

After that, it recombines it (from the second |, so the output should be

[PR #(numbers in \3)]...

[Damiano Testa]

I was looking just at sed, let me run the git command

[Yaël Dillies]

If as a result you can tell me how many PRs there were in May that would be great

[Damiano Testa]

Give me a minute, I will be back soon!

[Damiano Testa]

Where is the script? I do not know what monthnames_uc is.

[Yaël Dillies]

https://github.com/leanprover-community/blog

[Damiano Testa]

I see, so you want to put an upper time limit, not just a lower time limit, correct?

[Damiano Testa]

There is an --until flag, let me implement it!

[Damiano Testa]

git log --since "MAY 1 2014" --until "MAY 31 2014"

is this what you want, but wrapped in a script?

[Yaël Dillies]

Ten years later, but yes :grinning:

[Damiano Testa]

Oh, yes! I just copy pasted

[Damiano Testa]

That should be easy and I do not think that we need those hand-rolled arrays of month names

[Yaël Dillies]

@Dagur Asgeirsson, tiny update that I accidentally asked you to write a paragraph about a bunch of PRs that landed in June. Please carefully check when the PRs you are talking about landed

[Damiano Testa]

Could this be what you want?

mm=05
yy=2024
git log  --pretty=oneline --abbrev-commit --since "$yy-$mm-01" --until "$yy-$mm-$(date -d "$mm/1 + 1 month - 1 day" "+%d")"

[Damiano Testa]

(and then the rest of the pipe, this should select PRs from yy-mm-01 until yy-mm-(however number of days mm has))

[Yaël Dillies]

Can you run that and tell what the last PR you get is and roughly how many PRs there are?

[Damiano Testa]

last commit:
ac59a83c23 chore: fix formatting of many misplaced "by"s (#13204)

652 commits in total

[Yaël Dillies]

Interesting. You seem to be missing

• PR #13391 :: feat(Algebra/Lie/InvariantForm): Lie algebras with a nondegenerate invariant form are semisimple
• PR #13380 :: feat(Data/Set/Finite): Infinite.nontrivial
• PR #12624 :: feat(Algebra/Homology): morphisms of cochain complexes that are degreewise epi with an injective kernel
• PR #12638 :: feat(Algebra/Homology): consequences of the homology sequence
• PR #13386 :: feat(CategoryTheory): surjective-injective factorizations in concrete categories
• PR #13408 :: chore(CategoryTheory/Sites): remove unused variable
• PR #13265 :: feat(Algebra/Lie): Killing Lie algebras are semisimple
• PR #13398 :: feat(AlgebraicGeometry/StructureSheaf): add two useful lemmas
• PR #13324 :: feat(CategoryTheory/Sites): locally bijective morphisms of presheaves
• PR #13322 :: feat: add the definition of OrzechProperty
• PR #13389 :: feat: add API for additive characters
• PR #13411 :: feat(CategoryTheory): surjective/injective factorizations in concrete categories
• PR #13402 :: chore(test/linarith): remove stray variables from guard_msgs
• PR #13273 :: feat(NumberTheory/LSeries): Riemann zeta as special case of Hurwitz
• PR #13286 :: chore: remove most of the material on BitVec

[Yaël Dillies]

Maybe something about the timezone?

[Damiano Testa]

Yes, I was going to suggest a timezone issue as well...

Are there more commits at the beginning in mine?

[Damiano Testa]

These should be the first commits of the month, in chronological order

8390a31684 chore(CategoryTheory/MorphismProperty): Use le instead of subset (#12520)
154a87cdc7 refactor(Condensed): redefine condensed abelian groups as condensed ℤ-modules (#12510)
9481bfd671 chore: remove simp from Finset.filter_congr_decidable (#12576)
1079fe3f2f chore: update to leanprover/std4#769 (#12476)
7e5c6cb413 chore: remove @[simp] from Fintype.card_fun (#12577)
d24a65801b feat(Order/Minimals, Order/RelIso/Set): four RelIso lemmas (#12558)
6fa9d2b59c chore: missing DecidableEq (DirectSum _ _) instance (#12491)
4fce67d33a perf(AG.RingHomProperties): less defeq abuse (#12563)
bd932a420f chore: adaptations to lean 4.8.0 (#12578)
f09d52971e feat(Algebra/Lie): existence of Cartan subalgebras (#12297)

[Yaël Dillies]

Yes indeed. Mine start

• PR #12583 :: chore: adaptations to lean 4.8.0
• PR #12573 :: chore: Rename Finset.inter_sdiff to Finset.inter_sdiff_assoc
• PR #12574 :: chore: Rename Dart.is_adj to Dart.adj

[Damiano Testa]

Ok, so maybe there should also be a timezone-normalization filter.

[Ruben Van de Velde]

Maybe

git log  --pretty=oneline --abbrev-commit --since "$yy-$mm-01T00:00:00Z" --until "$yy-$mm-$(date -d "$mm/1 + 1 month - 1 day" "+%d")T23:59:59Z"

[Damiano Testa]

Can you try running it with

TZ=UTC git log  --pretty=oneline --abbrev-commit --since "$yy-$mm-01" --until "$yy-$mm-$(date -d "$mm/1 + 1 month - 1 day" "+%d")"

for me the output seems unchanged.

[Ruben Van de Velde]

Damiano Testa said:

TZ=UTC git log --pretty=oneline --abbrev-commit --since "$yy-$mm-01" --until "$yy-$mm-$(date -d "$mm/1 + 1 month - 1 day" "+%d")"

That also misses #13286 and others for me

[Damiano Testa]

Ok, sorry, I have to take care of some non-Lean stuff for a few hours: I will look at this thread when I am back to help out further, if there is the need!

[Damiano Testa]

I fixed (I hope) the script, could I get permission to push to branches of the blog repo to make a PR?

Alternatively, I can post here the diff in the file.

[Yaël Dillies]

Alternatively you can open a PR and I will merge it

[Damiano Testa]

You mean a PR from a fork?

[Damiano Testa]

(I was going via the mathlib approach, but I guess I could do it from a fork...)

[Yaël Dillies]

Yeah, CI considerations don't apply here

[Damiano Testa]

I created a PR, I think.

[Damiano Testa]

Actually, I do not see it: I wonder what I did.

[Yaël Dillies]

Oh I see @Moritz Doll has blog#48 open for improvements to the script

[Damiano Testa]

Ok, I eventually managed to actually open a PR!

[Damiano Testa]

Feel free to use either that one, or Moritz's.

[Yaël Dillies]

I still don't see it here: https://github.com/leanprover-community/blog/pulls :thinking:

[Damiano Testa]

Ok, sorry, earlier I opened a PR to my own fork, now I should have opened it to the blog.

[Yaël Dillies]

Damiano, while you are here, could I please request that the PRs are automatically sorted by t- labels? As in put all the PRs tagged with t-algebra (and nothing else) in a bulleted list starting with Algebra. (or algebra if you don't want to figure out the labels -> subject names mapping), everything tagged with t-order (and nothing else) in a bulleted list starting with Order., everything tagged with t-algebra and t-order (and nothing else) in a bulleted list starting with Algebra & Order., etc...

[Yaël Dillies]

This would help a lot with writing the blogpost, I hope

[Damiano Testa]

Let me try, but I do not know where the tag information is.

[Damiano Testa]

(Also, today I have live things going on intermittently, so I disappear and reapper!)

[Yaël Dillies]

I think Moritz's version of the script will more easily be adapted to get the label information since it directly calls the github API

[Yaël Dillies]

@Amelia Livingston, would you be happy to write a short paragraph here?

[Yaël Dillies]

I am now done sorting the PRs in blog#76 by subject and by who I think should be writing the paragraph (sometimes I gave up and wrote Misc). It would great if the relevant people commented on the PR with their paragraphs. If I have written your name down, feel free to move the paragraph across subjects, to drop some of the PRs from the list I have provided or to put someone else on the job.

[Yaël Dillies]

I don't want to mass ping, so I will wait a few days for things to happen organically before chasing people down/badly writing paragraphs myself.

[Andrew Yang]

(It's blog#76)

[Sébastien Gouëzel]

Is blog#76 ready, or is there still something to polish? It would be better to post it before the end of June, as a blog post on what happened in May in Mathlib.

[Yaël Dillies]

Per my message above, I am waiting for person X to turn

  * X
    * PR A
    * PR B

into a short paragraph about A and B

[Yaël Dillies]

(well in fact I was planning on chasing people up earlier but I spent the last few days being quite sick and I am just recovering now)

[Michael Rothgang]

@Riccardo Brasca @David Loeffler @Mitchell Lee @Scott Carnahan @Jireh Loreaux @Kim Morrison If I see correctly, all your names fall under Yael's message above. You can help them write "This month in mathlib" by writing a few sentences about your sequence of PRs. (No worries if you don't have time to do so - in case you do, this contribution is, I understand, very much appreciated. If you're not sure what to write, see this message and find where https://github.com/leanprover-community/blog/pull/76/files mentions your name.)

[Michael Rothgang]

AFAICT, these are the main people "missing". I believe Oliver Nash already wrote a paragraph, so their name with PR list can be removed.

[Riccardo Brasca]

Sorry, I missed this. I don't have any reasonable PR for May (hoping to have flt3 done soon, but the preliminary PRs are not so interesting I think).

[Jireh Loreaux]

Will do today

[Mitchell Lee]

Hello, I am taking a look right now

[David Loeffler]

I've added something about my Hurwitz-zeta PR's.

[Scott Carnahan]

I wrote something short about vertex operators.

[Jireh Loreaux]

I wrote a bit about the continuous functional calculus. I also included #13541, which was technically merged in early June, but it morally goes with the rest. If you want to remove it, just delete the last sentence from that paragraph.

[Jireh Loreaux]

@Yaël Dillies thanks for this by the way! This is a heroic month in Mathlib blog post.

[Kim Morrison]

I've done my paragraph! Thanks @Yaël Dillies for writing all this, and @Michael Rothgang for the ping!

[Yaël Dillies]

The true lesson learned is that the best work is the work done by others :speak_no_evil:

[Yaël Dillies]

I will look at the suggestions sometime tomorrow hopefully and then it should be mergeable?

[Yaël Dillies]

I also think I now have the insight I need to run Month in Mathlib for June better. I will be unavailable until the 4th of July, so expect plenty of notifications on the 5th. :notifications:

[Mitchell Lee]

I have put in some comments. Thank you!

[Jeremy Tan]

can #9317 be included in the June post?

[Yaël Dillies]

I am removing the following non-formatted entries. If a category theorist finds that outrageous, please shout!

* [PR #12206](https://github.com/leanprover-community/mathlib4/pull/12206) :: feat(CategoryTheory): more functoriality for Comma categories
* [PR #12797](https://github.com/leanprover-community/mathlib4/pull/12797) :: chore(CategoryTheory): fix hasFiniteLimits_of_hasLimitsOfSize
* [PR #10094](https://github.com/leanprover-community/mathlib4/pull/10094) :: feat: comonoid objects are monoid objects in the opposite category
* [PR #12649](https://github.com/leanprover-community/mathlib4/pull/12649) :: feat(CategoryTheory/Abelian): "three" lemmas
* [PR #12625](https://github.com/leanprover-community/mathlib4/pull/12625) :: refactor(CategoryTheory/Adjunction): make uniqueness of adjoints independent of opposites
* [PR #12801](https://github.com/leanprover-community/mathlib4/pull/12801) :: chore(CategoryTheory/Sites): generalise universes for extensive sheaves
* [PR #12839](https://github.com/leanprover-community/mathlib4/pull/12839) :: feat(CategoryTheory/Galois): prorepresentability of fiber functors
* [PR #11701](https://github.com/leanprover-community/mathlib4/pull/11701) :: feat(CategoryTheory/Monoidal): the curried associator isomorphism
* [PR #12909](https://github.com/leanprover-community/mathlib4/pull/12909) :: feat(CategoryTheory/Limits): add classes `ReflectsFiniteLimits` and friends
* [PR #12803](https://github.com/leanprover-community/mathlib4/pull/12803) :: feat(CategoryTheory/Sites): 1-hypercovers
* [PR #12927](https://github.com/leanprover-community/mathlib4/pull/12927) :: feat(CategoryTheory): the adjunction between Over.map and Over.baseChange
* [PR #12374](https://github.com/leanprover-community/mathlib4/pull/12374) :: feat(CategoryTheory/Sites): the category of sheaves is a localization of the category of presheaves
* [PR #12980](https://github.com/leanprover-community/mathlib4/pull/12980) :: feat: moving some adjunctions of over categories to `CategoryTheory.Adjunction.Over`
* [PR #12841](https://github.com/leanprover-community/mathlib4/pull/12841) :: feat(CategoryTheory/Limits): pro-coyoneda lemma
* [PR #12332](https://github.com/leanprover-community/mathlib4/pull/12332) :: feat(CategoryTheory/Sites): functors which preserves sheafification
* [PR #12785](https://github.com/leanprover-community/mathlib4/pull/12785) :: feat(CategoryTheory): transport Kan extensions via equivalences
* [PR #13189](https://github.com/leanprover-community/mathlib4/pull/13189) :: feat(CategoryTheory/Sites): a sieve containing a covering presieve is covering for the associated Grothendieck topology
* [PR #13006](https://github.com/leanprover-community/mathlib4/pull/13006) :: feat(CategoryTheory/Action): category of continuous actions
* [PR #12631](https://github.com/leanprover-community/mathlib4/pull/12631) :: feat(CategoryTheory/Localization): left resolutions for localizer morphisms
* [PR #13320](https://github.com/leanprover-community/mathlib4/pull/13320) :: feat(CategoryTheory/Sites/LeftExact): weaken universe assumptions
* [PR #13318](https://github.com/leanprover-community/mathlib4/pull/13318) :: feat(CategoryTheory/Sites): more properties of locally surjective morphisms of presheaves
* [PR #13371](https://github.com/leanprover-community/mathlib4/pull/13371) :: feat(CategoryTheory/Sites): extensive topology is subcanonical
* [PR #13331](https://github.com/leanprover-community/mathlib4/pull/13331) :: feat(CategoryTheory/MorphismProperty): the factorization axiom
* [PR #13223](https://github.com/leanprover-community/mathlib4/pull/13223) :: feat(CategoryTheory): constructor for functors from the category `ℕ`
* [PR #12929](https://github.com/leanprover-community/mathlib4/pull/12929) :: refactor(CategoryTheory): the structure Functor.FullyFaithful
* [PR #13386](https://github.com/leanprover-community/mathlib4/pull/13386) :: feat(CategoryTheory): surjective-injective factorizations in concrete categories
* [PR #13324](https://github.com/leanprover-community/mathlib4/pull/13324) :: feat(CategoryTheory/Sites): locally bijective morphisms of presheaves
* [PR #13411](https://github.com/leanprover-community/mathlib4/pull/13411) :: feat(CategoryTheory): surjective/injective factorizations in concrete categories
* [PR #12857](https://github.com/leanprover-community/mathlib4/pull/12857) :: feat: the forgetful functor from `Mon_ C` to `C` is monoidal when `C` is braided
* [PR #11719](https://github.com/leanprover-community/mathlib4/pull/11719) :: feat: morphisms of presheaves that are locally injective for a Grothendieck topology
* [PR #11489](https://github.com/leanprover-community/mathlib4/pull/11489) :: feat: the cohomology of a presheaf of groups in degree 1

[Yaël Dillies]

I am removing the following non-formatted entries. If a category theorist finds that outrageous, please shout!

* [PR #12206](https://github.com/leanprover-community/mathlib4/pull/12206) :: feat(CategoryTheory): more functoriality for Comma categories
* [PR #12797](https://github.com/leanprover-community/mathlib4/pull/12797) :: chore(CategoryTheory): fix hasFiniteLimits_of_hasLimitsOfSize
* [PR #10094](https://github.com/leanprover-community/mathlib4/pull/10094) :: feat: comonoid objects are monoid objects in the opposite category
* [PR #12649](https://github.com/leanprover-community/mathlib4/pull/12649) :: feat(CategoryTheory/Abelian): "three" lemmas
* [PR #12625](https://github.com/leanprover-community/mathlib4/pull/12625) :: refactor(CategoryTheory/Adjunction): make uniqueness of adjoints independent of opposites
* [PR #12801](https://github.com/leanprover-community/mathlib4/pull/12801) :: chore(CategoryTheory/Sites): generalise universes for extensive sheaves
* [PR #12839](https://github.com/leanprover-community/mathlib4/pull/12839) :: feat(CategoryTheory/Galois): prorepresentability of fiber functors
* [PR #11701](https://github.com/leanprover-community/mathlib4/pull/11701) :: feat(CategoryTheory/Monoidal): the curried associator isomorphism
* [PR #12909](https://github.com/leanprover-community/mathlib4/pull/12909) :: feat(CategoryTheory/Limits): add classes `ReflectsFiniteLimits` and friends
* [PR #12803](https://github.com/leanprover-community/mathlib4/pull/12803) :: feat(CategoryTheory/Sites): 1-hypercovers
* [PR #12927](https://github.com/leanprover-community/mathlib4/pull/12927) :: feat(CategoryTheory): the adjunction between Over.map and Over.baseChange
* [PR #12374](https://github.com/leanprover-community/mathlib4/pull/12374) :: feat(CategoryTheory/Sites): the category of sheaves is a localization of the category of presheaves
* [PR #12980](https://github.com/leanprover-community/mathlib4/pull/12980) :: feat: moving some adjunctions of over categories to `CategoryTheory.Adjunction.Over`
* [PR #12841](https://github.com/leanprover-community/mathlib4/pull/12841) :: feat(CategoryTheory/Limits): pro-coyoneda lemma
* [PR #12332](https://github.com/leanprover-community/mathlib4/pull/12332) :: feat(CategoryTheory/Sites): functors which preserves sheafification
* [PR #12785](https://github.com/leanprover-community/mathlib4/pull/12785) :: feat(CategoryTheory): transport Kan extensions via equivalences
* [PR #13189](https://github.com/leanprover-community/mathlib4/pull/13189) :: feat(CategoryTheory/Sites): a sieve containing a covering presieve is covering for the associated Grothendieck topology
* [PR #13006](https://github.com/leanprover-community/mathlib4/pull/13006) :: feat(CategoryTheory/Action): category of continuous actions
* [PR #12631](https://github.com/leanprover-community/mathlib4/pull/12631) :: feat(CategoryTheory/Localization): left resolutions for localizer morphisms
* [PR #13320](https://github.com/leanprover-community/mathlib4/pull/13320) :: feat(CategoryTheory/Sites/LeftExact): weaken universe assumptions
* [PR #13318](https://github.com/leanprover-community/mathlib4/pull/13318) :: feat(CategoryTheory/Sites): more properties of locally surjective morphisms of presheaves
* [PR #13371](https://github.com/leanprover-community/mathlib4/pull/13371) :: feat(CategoryTheory/Sites): extensive topology is subcanonical
* [PR #13331](https://github.com/leanprover-community/mathlib4/pull/13331) :: feat(CategoryTheory/MorphismProperty): the factorization axiom
* [PR #13223](https://github.com/leanprover-community/mathlib4/pull/13223) :: feat(CategoryTheory): constructor for functors from the category `ℕ`
* [PR #12929](https://github.com/leanprover-community/mathlib4/pull/12929) :: refactor(CategoryTheory): the structure Functor.FullyFaithful
* [PR #13386](https://github.com/leanprover-community/mathlib4/pull/13386) :: feat(CategoryTheory): surjective-injective factorizations in concrete categories
* [PR #13324](https://github.com/leanprover-community/mathlib4/pull/13324) :: feat(CategoryTheory/Sites): locally bijective morphisms of presheaves
* [PR #13411](https://github.com/leanprover-community/mathlib4/pull/13411) :: feat(CategoryTheory): surjective/injective factorizations in concrete categories
* [PR #12857](https://github.com/leanprover-community/mathlib4/pull/12857) :: feat: the forgetful functor from `Mon_ C` to `C` is monoidal when `C` is braided
* [PR #11719](https://github.com/leanprover-community/mathlib4/pull/11719) :: feat: morphisms of presheaves that are locally injective for a Grothendieck topology
* [PR #11489](https://github.com/leanprover-community/mathlib4/pull/11489) :: feat: the cohomology of a presheaf of groups in degree 1

[Yaël Dillies]

@David Ang, @Junyan Xu, should May MiM mention EDS?

[Yaël Dillies]

@David Ang, @Junyan Xu, should May MiM mention EDS?

[David Ang]

Mathlib only has basic definitions since the main proof is still in a PR... so probably not?

[Yaël Dillies]

Okay, thanks for the info!

[Ruben Van de Velde]

Should we make it May-June? :sweat_smile:

[Yaël Dillies]

Oh no, I'm basically done now!

[Yaël Dillies]

@David Ang, sorry I keep pinging you (please write less interesting stuff :stuck_out_tongue_closed_eyes:). Do you think #9405 is worth mentioning (at a skim, it seems worth mentioning to me)? If so, can you please write a bullet point about it/incorporate it in an existing bullet point?

[Yaël Dillies]

Actually, given that it goes with #9405 and was merged at the very end of May, I suggest we make it part of June

[Yaël Dillies]

Please still write a paragraph, but don't add it to blog#76. I'll tell you when I open the June MiM PR

[David Ang]

Sure I guess. Before this we had an API for affine coordinates (equations, operations, points, group law), and this PR (along with the 5 others it depends on) develops the analogous API for Jacobian coordinates (by reducing difficult computations to the affine case). I don't know how long you want me to write but this is the gist of it.

[David Ang]

Thanks for organising all this btw!

[Yaël Dillies]

David Ang said:

I don't know how long you want me to write but this is the gist of it.

Basically long enough that people don't have to plough through Zulip to understand the context, why it is important and how it happened

[Yaël Dillies]

@Oliver Nash, there are many PRs in blog#76 which I think you are competent to write about (grep for your name). Can you have a look, ditch the uninteresting ones and write a paragraph about the interesting ones? If you don't have time, please say so and I will try to do the aforementiond myself

[Oliver Nash]

I actually do have a little time right now --- I'll rewrite the Lie theory paragraph to include these PRs.

[Oliver Nash]

OK done. I also added some names since I see that is what others have done in this blog PR (my previous version of this paragraph had omitted names since this seemed to be the style in the blog back in 2022).

[Yaël Dillies]

Oh, this was not a conscious decision. If people want the names gone, I'll remove them again.

[Yaël Dillies]

Okay, I have done what I would like to be the final edits. Please review blog#76 ! In the absence of opposition, I will merge the PR at around 2024-06-30T20:00:00+02:00

[Kevin Buzzard]

This looks great! I hope that the community figures out a way of continuing to create informative posts like this. I think it's a good advert for mathlib and also an indication that the maths we're doing is becoming more serious.

[Yaël Dillies]

Merged! Let's start June now

[Riccardo Brasca]

Thanks a lot for doing this!!

Looking at the post itself I think there is a small problem with titles, right? I mean, the first Algebra should be bigger than the rest.

[Yaël Dillies]

You're right, the headers are all wrong. Investigating

[Rida Hamadani]

I think you need to use 4 spaces instead of 2.

[Damiano Testa]

Or * instead of #...#?

[Yaël Dillies]

I'm using * already

[Damiano Testa]

Yes, I wonder whether Algebra should have a #...#, instead of a * to make it a header.

[Damiano Testa]

And then, withing each #-block, you use regular * for the lists.

[Yaël Dillies]

Ah! Sorry, I read your message the wrong way around. I followed whatever was done in the previous posts, see eg https://leanprover-community.github.io/blog/posts/this-month-in-mathlib-oct-and-nov-2022

[Damiano Testa]

Oh, I see. There, they indent more then inner list and use - instead of * for the inner one. I would not expect that to make a difference, but...

[Rida Hamadani]

I'm sure it needs 4 spaces rather than 2 because the * with 4 spaces in the post rendered correctly.

[Rida Hamadani]

I think there is one last problem.
There should be double nested points, for example the two points under:

Thanks to the reviews by Thomas Bloom, a long sequence of three years old material by Yaël Dillies and Bhavik Mehta culminating in Roth's theorem on arithmetic progressions was finally merged:

These points need 8 spaces instead of 6.

[Yaël Dillies]

Yes, I have just fixed this as well

[Rida Hamadani]

It still looks like this:
image.png
The spaces at line 49 are 6 instead of 8.
Do you want me to PR a fix?

[Yaël Dillies]

Sorry, I am still fighting the train wifi to open a PR

[Yaël Dillies]

Should finally be fixed

[Yaël Dillies]

Ugh, there is still something wrong and I don't know how to fix it. @Rida Hamadani, if you're interested, go look at the paragraph starting with "APAP already contains". It swallowed the following bullet points somehow.

[Rida Hamadani]

I'm hoping blog#80 will fix this, but I'm not totally sure!

[Rida Hamadani]

I'm referring to this stack exchange answer for the proposed solution:
https://stackoverflow.com/a/42168153

[Yaël Dillies]

What's the change to the last line? I can't see it

[Rida Hamadani]

Yaël Dillies said:

What's the change to the last line? I can't see it

I only added 2 empty lines, this is very weird. I tried copying the old last line and pasting it instead of the new last line, but the commit turned out to be an empty commit (see here).

[Yaël Dillies]

Oh that must be because you have a different CR/CRLF setting. Are you on Windows by any chance?

[Rida Hamadani]

Yes! Will this cause any problems after merging?

[Yaël Dillies]

Don't think so, but you should take the opportunity to learn about how git handles line endings: https://docs.github.com/en/get-started/getting-started-with-git/configuring-git-to-handle-line-endings

[Yaël Dillies]

Try running git config --global core.autocrlf true and saving the file again.

[Rida Hamadani]

Oops, it seems that I've done a mistake while trying to fix the issue with the last line, and now blog#80 looks very weird, is there an easy fix to this or should I close it and open a new one?

[Rida Hamadani]

I've closed blog#80 and created blog#82. Sorry about this, I find git confusing.

[Oisin McGuinness]

Thanks to everyone who has worked on this Month in Mathlib report; great reading, and very very useful as a snapshot of the activity in Mathlib. Looking forward to June :-)

I noticed two small typos, perhaps one of you who have access can fix?
In the Analysis section, around line 31 in last commit, 'Stone-Weiertrass' should be 'Stone-Weierstrass' (missing 2nd s).
In the "General library maintainance" section (around line 79), the title should be "General library maintenance".

Thanks again to everyone who wrote all this!

[Yaël Dillies]

Thanks for the report! You are free to open a PR to leanprover-community/blog, which I will merge. Else I will fix this next time I'm on a train, in a bit less than a day

[Oisin McGuinness]

I've created a pull request, Fixing two typos in May Blog.

Hope this was done correctly, first pull request I've created!

[Patrick Massot]

Merged, thanks!

[Kim Morrison]

Minor suggestion that I should have made earlier: the first sentence is confusing because it presupposes that the reader even knows what "the port" is!