IsIso in definition of MonoidalFunctor

Stream: mathlib4

[Brendan Seamas Murphy]

Why does the definition of MonoidalFunctor have Prop-valued fields ε_isIso, μ_isIso instead of inverses for ε, μ? It seems like it would be nice for things like MonoidalClosed.ofEquiv to compute, but this is not the case right now. It seems like this is at odds with other parts of the category theory library like IsLimit, IsLeftAdjoint, IsEquivalence where we use data-carrying subsingletons (or objects of contractible groupoids more generally) instead of Props

[Eric Wieser]

(docs#CategoryTheory.MonoidalFunctor for reference)

[Eric Wieser]

It might just be done this way because it was easiest, since you can use extends

[Eric Wieser]

(which isn't an argument for keeping it the way it is)

[Brendan Seamas Murphy]

Why does extends not work if we do it the other way?

[Brendan Seamas Murphy]

Oh, what I had in mind was adding fields called something like μinv, εinv and proofs that they're inverses, then deriving projections μIso, εIso from these (not making μIso, εIso themselves fields)

[Eric Wieser]

I was indeed thinking of the other approach you describe

[Eric Wieser]

Both are reasonable, I think the second one is shorter overall

[Johan Commelin]

Does this risk introducing diamonds?

[Kim Morrison]

I'm generally pretty unhappy with the state of MonoidalFunctor, so if you feel like making major changes, sounds good to me. :-)

[Adam Topaz]

Johan Commelin said:

Does this risk introducing diamonds?

I don’t think diamonds would be an issue with the proposed approach. It’s still just forgetting data when you pass to lax monoidal functors

[Brendan Seamas Murphy]

I have a first draft of this refactor, but as I was cleaning things up I realized the approach Eric had in mind would probably be better... I expect that most of the work I've done here will be compatible with that definition too, though. #10845

[Brendan Seamas Murphy]

The PR is a somewhat unavoidably monstrous size, since so many files are descendents of MonoidalFunctor

[Brendan Seamas Murphy]

There's also a fair amount of boilerplate that only exists because I can't generate εIso, μIso with simps. A tactic that generates them in a similar way could be implemented, but it would be simplest to make the existing infrastructure available by having εIso, μIso be fields of MonoidalFunctor

[Brendan Seamas Murphy]

Also, for oplax monoidal functors would we still use ε, μ or use the names η, δ? This is really a question about comonoids more generally. Comonads in mathlib use ε, δ which is consistent with the first source I checked (category theory in context) but feels wrong to me (it's not consistent with the names for the comultiplication/counit of a bialgebra)

[Brendan Seamas Murphy]

Er wait I'm backwards, I think the convention I'm suggesting would say the unitor structure map for a lax monoidal functor should be named η instead of ε? This is very confusing

[Kevin Buzzard]

We only added bialgebras a few weeks ago and I'm definitely open to a change of names there if you're looking for consistency. I don't know what the literature says, we just copied out of a random book

[Joël Riou]

The suggested refactor would slightly ease some proofs in the internals of the API for shift functors . For example, I think that docs#CategoryTheory.ShiftMkCore.shiftFunctorZero_eq would become rfl.

[Eric Wieser]

Alternatively, should IsIso be made to carry data (so that it matches IsLimit, IsLeftAdjoint, IsEquivalence)?

[Joël Riou]

The with-data version of IsIso is Iso! I think it is useful to have both.

[Eric Wieser]

docs#Iso is to my proposed IsIso as docs#Units is to docs#Invertible

[Eric Wieser]

Or I think as Adjunction is to IsLeftAdjoint, though I could be mistaken there

[Joël Riou]

If IsIso was carrying data, there would be great risks of diamonds.

[Eric Wieser]

Indeed, but it sounds like we were ok with that for the three other Is*s described above

[Kevin Buzzard]

For some reason seeing all these Is things which aren't Props today, combined with seeing a bunch of non-Is things which are props in the question about topology and spectral spaces yesterday (CompactSpace, sober space, T0 space etc) really surprises me. This community is usually so consistent with naming conventions but with Is we are absolutely all over the place.

[Johan Commelin]

I guess it's even something that we can lint against.

[Joël Riou]

Eric Wieser said:

Indeed, but it sounds like we were ok with that for the three other Is*s described above

IsLimit is not a typeclass so that it carries data is not a problem (but we may consider changing the name). For IsLeftAdjoint and IsEquivalence, I am not super-happy that they contain data...

[Yaël Dillies]

May I interest you in #10819?

[Eric Wieser]

Did we agree on _Like as a naming pattern for data-like Is_? (I'm fine with it)

[Brendan Seamas Murphy]

I think the prop vs data carrying defintions in the category theory library are sort of a mess, it's not clear to me why some are one way and some are the other. Like, why is preservation of (co)limits a data carrying subsingleton when their existence is a prop? At the very least it would be good to have some design docs explaining the various design decisions

[Brendan Seamas Murphy]

Kevin Buzzard said:

We only added bialgebras a few weeks ago and I'm definitely open to a change of names there if you're looking for consistency. I don't know what the literature says, we just copied out of a random book

The change in names would be for lax monoidal functors, renaming ε to η for consistent with monads (both are unit maps of monoids). Unfortunately I think ε is very common for the unitor of a lax monoidal functor in the literature. I'd just prefer if we uniformly stuck with:

• μ as the name for a multiplication
• δ (or Δ) as the name for a comultiplication
• η as the name for a unit
• ε as the name for a counit

[Joël Riou]

For the preservation of limits/colimits, I think most of us agree it should be props.

[Adam Topaz]

@Brendan Seamas Murphy . Could you give an update regarding #10845? I would like to see this refactor happen sooner rather than later. If you need someone to adopt your work, please say so!

[Brendan Seamas Murphy]

Hey! Sorry, I haven't had time to work on lean recently. It might need to be adopted. I stopped working on it when I ran into a bug in lean4, hoping it would be fixed eventually and I could return to this PR. The issue comes in when I decided to make strong monoidal functors extend both lax and oplax monoidal functors. The diamond inheritance shouldn't have caused any problems except there's an issue with namespace resolution.

Probably the best thing to do is to have strong monoidal functors be their own structure with custom projections to lax and oplax functors (not actually using the inheritance system)

[Matthew Ballard]

Is there lean4 issue?

[Brendan Seamas Murphy]

https://github.com/leanprover/lean4/issues/3467

[Matthew Ballard]

In the mwe I guess you just have to force the projection to B?

[Brendan Seamas Murphy]

What do you mean?

[Matthew Ballard]

C.toB.getTwiceCountB

[Brendan Seamas Murphy]

Ah yeah

[Matthew Ballard]

But I agree it would be more ergnomic if it "just worked"