PRs from Toric

Stream: PR reviews

[Yaël Dillies]

There are a few PRs from Toric that have been waiting for a while. Could anybody review them, to get things going? Here they are, in decreasing order of priority from the point of view of Toric:

[Yaël Dillies]

• #24730 feat(Bialgebra): group-like elements

[Yaël Dillies]

• #24769 feat: X ⟶ M is a commutative monoid if M is a commutative monoid object

[Yaël Dillies]

• #24912 feat: affine monoids

[Yaël Dillies]

• #25365 feat: CommAlgCat is cocartesian-monoidal

[Yaël Dillies]

• #24778 feat: CommGrp-valued Yoneda embedding

[Yaël Dillies]

• #25183 feat: convolution product on linear maps from a coalgebra to an algebra

[Robin Carlier]

Left a few more comments on #24769.

[Yaël Dillies]

Thanks @Robin Carlier ! If you're bored, here are all the current Toric PRs: https://github.com/leanprover-community/mathlib4/pulls?q=is%3Aopen+is%3Apr+label%3Atoric+

[Robin Carlier]

#24769 has just yet a last minor comment and then it’s good to go.

I’ll look at the list but I won’t review anything non- t-category-theory, which is my comfort zone for reviewing.

[Yaël Dillies]

Thanks! I think you could still enjoy #25365, which is at the intersection of algebra and category theory

[Yaël Dillies]

Robin Carlier said:

#24769 has just yet a last minor comment and then it’s good to go.

Not anymore :wink:

[Sophie Morel]

Left a review on #24912.

[Damiano Testa]

(I took the liberty of editing one of the code-blocks in the review to add lean for syntax highlighting.)

[Sophie Morel]

Yaël Dillies said:

• #25365 feat: CommAlgCat is cocartesian-monoidal

After reading the discussion on this one, I am convinced that I do not want to touch it. :sweat_smile:

[Robin Carlier]

I am worried @Yaël Dillies will never ask me for review ever again :sweat_smile:

[Sophie Morel]

I just left a long false "proof" of a wrong generalization of one of the results in a PR, so they will probably never ask me either. :sweat_smile:

[Sophie Morel]

We can create a club of Reviewers From Hell.

[Yaël Dillies]

• #25271 feat: promote an AlgEquiv preserving counit and comul to a BialgEquiv

[Yaël Dillies]

I didn't previously mention the above PR because it is very routine and simple, but it has just become the blocker now that #25365 is merged

[Riccardo Brasca]

I've left a comment about a name and delegated.

[Yaël Dillies]

• #27026 chore: rename braidedCategoryOfFaithful to BraidedCategory.ofFaithful

[Yaël Dillies]

Yaël Dillies said:

• #24778 feat: CommGrp-valued Yoneda embedding

This one is still a real blocker. We need a lot of results about group objects that we get from Yoneda, and therefore we need this PR quite crucially

[Yaël Dillies]

Thank you Markus!

[Yaël Dillies]

• #27031 feat: Spec(R) notation for Spec (CommRingCat.of R)

[Yaël Dillies]

• #27030 refactor: use Algebra.FiniteType as a class

[Yaël Dillies]

• #27032 feat: FreeAbelianGroup.lift as an equivalence of groups

[Yaël Dillies]

• #27033 feat: F.op is a right adjoint if F is a left adjoint

[Yaël Dillies]

• #27034 chore: generalise syntactically Over.tensorHom_left_fst

[Yaël Dillies]

• #27041 feat(Bialgebra/Equiv): basic lemmas

[Yaël Dillies]

• #27044 feat: the tensor product of representable functors is representable

[Yaël Dillies]

• #27045 feat: AddEquiv.finsuppUnique v = v default

[Yaël Dillies]

• #27047 feat: MonoidHom.toAdditive'' as a MulEquiv

[Yaël Dillies]

• #27060 feat: missing definitional lemmas for the braiding on Mon_ C

[Yaël Dillies]

• #27061 feat(CategoryTheory): inv (μ F X Y) = δ F X Y

[Yaël Dillies]

• #27062 feat: cancelling a fully faithful functor on the right in a natural isomorphism

[Yaël Dillies]

• #27063 feat: Spec.map (Spec.fullyFaithful.preimage f).unop = f

[Yaël Dillies]

• #27064 feat: considering an iso over S as an iso in Over S

[Yaël Dillies]

The following one is from a new contributor, has been waiting for a long long time and is on its way to becoming blocking for upstreaming Toric:

• #24804 feat(CategoryTheory/Limits/Preserves/Shapes): show that if a functor preserves limits, so does Over.post

[Robin Carlier]

Took the liberty to specify the subfolder in #27044, as this is a property specific to cartesian monoidal categories, not general ones.

[Yaël Dillies]

Whoops, yes

[Yaël Dillies]

Yaël Dillies said:

• #24730 feat(Bialgebra): group-like elements

It would great to move forward on this one

[Yaël Dillies]

Yaël Dillies said:

• #25183 feat: convolution product on linear maps from a coalgebra to an algebra

That one is blocking a lot more PRs

[Yaël Dillies]

• #27580 feat: if F is fully faithful, then so is F.mapGrp

[Yaël Dillies]

• #27137 feat(CategoryTheory/Monoidal: an isomorphism of group objects is an isomorphim of the underlying objects

[Yaël Dillies]

Yaël Dillies said:

Yaël Dillies said:

• #24730 feat(Bialgebra): group-like elements

It would great to move forward on this one

@Amelia Livingston, do you think you can review this?

[Yaël Dillies]

Could we get things moving on
Yaël Dillies said:

• #25183 feat: convolution product on linear maps from a coalgebra to an algebra

? This is one of the most blocking PRs from Toric to date

[Yaël Dillies]

The most blocking PR right now is:

• #26057 feat: mon_tauto, a simp set to prove tautologies about a monoid object

[Robin Carlier]

I was actually looking at #26057, should complete the review by this evening.

[Yaël Dillies]

Two months later, I am back at it: Could a ring theorist please review #25183, which introduces the convolution product on linear maps? This is still blocking further upstreaming from Toric, and has now been waiting for review for five months (!!)

[Kim Morrison]

@Yaël Dillies, I see it's been merged already, but if you touch the file again it might be useful to add a cross-reference to Mathlib.CategoryTheory.Monoidal.Conv.

[Yaël Dillies]

Sure thing. I suspect @Monica Omar will be the one touching it next