monoid objects again

Stream: maths

[Matt Earnshaw]

Scott Morrison said:

Then commutative monoid objects in a braided category, then the tensor product on their module objects.

I am working on this here
Now (referring to the linked file/branch) I would like to add something along the lines of

structure ComMon extends Mon_in C :=
(comm : (σ X X).hom ≫ μ = μ)

but this doesn't work verbatim. what incantations do I need?

[Scott Morrison]

What goes wrong?

[Matt Earnshaw]

type mismatch at application
  (σ X X).hom ≫ μ
term
  μ
has type
  (λ {C : Type u} {_inst_1 : category C} {_inst_2 : monoidal_category C} (c : Mon_in C),
     Mon_in.X ⊗ Mon_in.X ⟶ Mon_in.X)
    to_Mon_in
but is expected to have type
  X ⊗ X ⟶ ?m_1

[Scott Morrison]

ah!

[Scott Morrison]

Mon_in should not be a class.

[Scott Morrison]

Let's just make it a fully bundled object.

[Scott Morrison]

(Certainly at least this will fix your problem here.)

[Scott Morrison]

But if we want to discuss making it a class again, that's probably a good discussion to have.

[Scott Morrison]

Some requests:

1. don't assume symmetric, or even braided, just to define a Mon_in.
2. only assume braided when defining CommMon_in. (I have applications later that need this, and the symmetry is irrelevant.)
3. It should be CommMon_in, not ComMon.

[Scott Morrison]

a suggestion for the naming for internal objects: how about we drop the in, and just write Mon_? Then users will write it as X : Mon_ C, which looks quite nice to me.

It's also slightly consistent with the existing notation conventions for monoidal categories, using α_ X Y Z for the associator, etc.

[Scott Morrison]

(To clarify my comment above, changing Mon_in back from a class to a structure will resolve your type mismatch error.)

[Matt Earnshaw]

agreed with the naming and thanks for the comments. sadly, changing class to structure still gives me a variant of the above error:

type mismatch at application
  (σ X X).hom ≫ μ
term
  μ
has type
  (λ {C : Type u} {_inst_1 : category C} {_inst_2 : monoidal_category C} (c : Mon_in C), c.X ⊗ c.X ⟶ c.X) to_Mon_in
but is expected to have type
  X ⊗ X ⟶ ?m_1

[Reid Barton]

what's the relationship between monoidal_category and symmetric_monoidal_category?

[Matt Earnshaw]

symmetric extends braided extends monoidal:
https://github.com/mattearnshaw/mathlib/blob/monoid_objects/src/category_theory/monoidal/category.lean#L475

[Scott Morrison]

oh!

[Scott Morrison]

I assumed you were building on top of #3550, which is slightly different

[Reid Barton]

You don't want both classes as variables then

[Scott Morrison]

There braided is an additional typeclass beyond monoidal, while symmetric extends braided.

[Matt Earnshaw]

aha

[Scott Morrison]

This was on the principle that braided has extra data, and symmetric is just a condition, but maybe that is applying a bad principle.

[Scott Morrison]

What would you suggest for this Reid?

[Scott Morrison]

My version is pretty verbose, requiring us to write [category C] [monoidal_category C] [braided_monoidal_category C], but I'm really hoping to have [[ ]] soon. :-)

[Scott Morrison]

I should also rename braided_monoidal_category down to braided_category, and similarly for symmetric, I guess.

[Scott Morrison]

I'm very happy to change anything in #3550 as suits you. I just sent you an invite giving you commit access to non-master branches, as well. (It's often easier to work on a branch of the main repo, rather than a fork, because you get included in our CI.)

[Scott Morrison]

Just let me know!

[Adam Topaz]

What's this about [[ ]]?

[Scott Morrison]

There's a suggestion that we add syntax for typeclasses that automatically pulls in any "missing" typeclasses.

[Adam Topaz]

Oh that would be nice!

[Scott Morrison]

So merely typing variables (C: Type) [[monoidal_category C]] would be sugar for variables (C: Type) [category C] [monoidal_category C].

[Scott Morrison]

Someone had a truly spectacular typeclass chain when setting up Lie groups. So perhaps the time has come.

[Reid Barton]

Have we considered just making [] do this?

[Matt Earnshaw]

thanks @Scott Morrison – I don't have a strong opinion on how this should be set up so I'm happy to adapt to what you have in #3550

[Scott Morrison]

@Reid Barton, sounds good to me! Hopefully if someone implements it, that will be easy to field test.

[Reid Barton]

I mean I'm not sure if it is crazy, but if it is then probably [[ ]] has problems as well.

[Scott Morrison]

I guess maybe it might hide problems? At least using the [[ ]] might be a reminder to check the signature of your function afterwards to see if it is what you expected.

[Scott Morrison]

@Matt Earnshaw, not sure if you saw, but Exercise 7 of the category theory tutorial for LftCM2020 includes, in the solutions, the construction of category (Mon_in C).

[Matt Earnshaw]

well that seems a bit more concise :-)

[Scott Morrison]

Obsessive use of obviously in parameter fields, and appropriate simp lemmas. :-) Eventually it breaks down, but it's nice while it lasts.

[Matt Earnshaw]

I would like to have a go at Mon_in Mon ≌ CommMon, and made a start but there seems to be some finicky things required in handling the cartesian monoidal structure and so on. in any case, it will have to wait until tomorrow

[Scott Morrison]

The things I'd like to try are:

1. check Mon_ Type ~ Mon
2. check Mon_ Mon ~ CommMon
3. check Mon_ Ab ~ Ring
4. construct Mod_ R C, where R : Mon_ C
5. show Mon_ C and Mod_ R C are monoidal when C is braided
6. check that Mod_ R Ab ~ Module R', where R : Mon_ Ab, and R' is the corresponding honest Ring.
7. check that Mon_ (C ⥤ D) ~ C ⥤ (Mon_ D) (is that even the right statement?)

[Scott Morrison]

Yeah, I didn't attempt that, but even trying Mon_ Type ~ Mon it was clear we need some infrastructure first.

[Scott Morrison]

Maybe I will have a go at that today, and if it works move on to Mon_ Ab ~ Ring, leaving Mon_ Mon ~ CommMon for you tomorrow. :-)

[Scott Morrison]

The cartesian monoidal structure on Mon at least is available from #3463, which hopefully will land soon.

[Matt Earnshaw]

now working here, with shameless inspiration

[Scott Morrison]

@Matt Earnshaw, I got as far as #3562, showing Mon_ (Type u) ≌ Mon.{u}.

[Matt Earnshaw]

@Scott Morrison I've merged #3463 into a branch but I'm getting grief from various coerelated things in trying to write down this proof, see the commented lines here. any hints would be much appreciated!

[Reid Barton]

I'm guessing this is related to the sleight of hand used at https://github.com/leanprover-community/mathlib/pull/3562/files#diff-bf95aa3a2dfae4af9442dade82298849R18

[Reid Barton]

IMO, this approach is not really sustainable.

[Reid Barton]

However, you could imitate it--or just define the monoidal structure of Mon manually.

[Scott Morrison]

Yeah, I am really torn about those simp lemmas that Reid calls "sleight of hand". :-) It seems there are two choices: completely refuse to look at the definition of the limits you've constructed in the particularly concrete category you're working with, and just use the limits API, or write simp lemmas to get the limits API completely out of the way. For Mon_ Type ~ Mon, I took the later approach, but I fully endorse Reid's concern about this.

I did try the first approach, and really struggled. :-(

@Reid Barton, do you have a suggestion about an alternate approach? Or advice on how to prove things like this without "peeking at the definitions"?

[Reid Barton]

I actually tried to link to the line

 local attribute [instance] types.types_has_terminal types.types_has_binary_products

but linking to a specific line in a PR doesn't seem to work so well.

[Reid Barton]

The one in category_theory.monoidal.types.

[Reid Barton]

I was wondering how you were going to do this given the inconvenient definition of $\otimes$--the solution was to replace it by a convenient one

[Reid Barton]

With the benefit of hindsight, it seems like we ended up with the worst of both worlds with the classes like has_binary_products--we have a pretty large API to deal with anyways (and a larger one would be useful), but we don't have the flexibility to choose convenient instances.

[Reid Barton]

I think the design you may have had in the pre-mathlib days (or perhaps it was one of several possible designs) was better--just have a totally separate, elementary definition of binary products and then have an equivalence with limits over a two-object category available for when you don't care about the specific construction.

[Scott Morrison]

Where is the first place we're going to see this inflexibility of in choosing limits cause pain, if we use this local attribute [instance] trick to produce definitionally more convenient limits in some places, but also have global instances with different definitions available?

Presumably we going to get to some situation where we have two copies of limits.prod X Y, but they have two unrelated instances making the choices. We're still going to be able to use def cone_point_unique_up_to_iso {s t : cone F} (P : is_limit s) (Q : is_limit t) : s.X ≅ t.X := (or possibly even more convenient formulations) to obtain an isomorphism between them.

[Reid Barton]

Well any definition with a [has_binary_products] are going to have to be transported manually across those isomorphisms

[Reid Barton]

For example, if you proved a locally compact space was exponentiable with respect to some local notion of products you will need to do some work to show it's exponentiable with respect to some other products

[Reid Barton]

and most likely this will manifest as some unification problem failing to solve for no apparent reason

[Kevin Buzzard]

Mathematicians don't need to do any work, right?

[Kevin Buzzard]

What do we have that this system doesn't?

[Reid Barton]

I would argue that you do have to do some work

[Reid Barton]

or alternatively that, in category theory, we have an extra layer of "reasonableness" for definitions on top of the basic one

[Kevin Buzzard]

If we could rewrite along isomorphisms would it all be easy?

[Reid Barton]

it's not really the usual kind of rewriting along isomorphisms

[Kevin Buzzard]

You shouldn't be proving things about some explicit definition of a product, if you're in a category, right? You should be proving things about anything satisfying the universal property of a product

[Reid Barton]

rewriting along isomorphisms would be like, if an object X of C is exponentiable, and C' is another category isomorphic to C, then the corresponding object X' of C' is exponentiable

[Kevin Buzzard]

This is what we do in localisation now, we don't prove things about R[1/S], we prove things about R-algebras satisfying the universal property that R[1/S] has

[Reid Barton]

okay I guess maybe you can always swap two isomorphic objects of a category? but it's very unnatural

[Kevin Buzzard]

Not if they're canonically isomorphic

[Reid Barton]

no I mean, find an automorphism of the category which interchanges the objects

[Reid Barton]

that requires LEM for example

[Reid Barton]

We really do also consider notions in category theory which are not isomorphism-independent in this sense--I think this generally manifests as the notion itself not being equivalence-invariant

[Kevin Buzzard]

I was just imagining some internal rewriting -- if P is a predicate on objects tagged with the magic sauce, then P(X) iff P(Y) if Y is isomorphic to X

[Reid Barton]

It's possible that there is a framework which covers both of these kinds of problems

[Reid Barton]

but anyways, you would still have to use it explicitly, presumably

[Kevin Buzzard]

if you were foolish enough to prove things about a product rather than all things satisfying the universal property of a product

[Kevin Buzzard]

like I was with localisations

[Kevin Buzzard]

but I don't really understand the extra complications categories bring to this issue

[Reid Barton]

Maybe it's really that what we usually think about as transport across isomorphisms is a special case of this? but I'm not convinced that category theory is really a good framework to think about that problem

[Reid Barton]

Doesn't the characterization of localizations itself use products? I think they are kind of too fundamental to do the same thing

[Kevin Buzzard]

Strickland's characterisation for f:R->A to be R[1/S] has a line "if a in A then there exists r in R and s in S with a*f(s)=f(r)"

[Reid Barton]

Anyways these are not facts of a formal nature I have in mind. For example $- \times Y$ preserves colimits if $Y$ is locally compact--obviously it can't be too formal because it has the condition "$Y$ locally compact". In principle you could prove statements like this from the universal property of the product but I think the proof would basically amount to building the usual product and arguing there.

[Reid Barton]

The actual product has some bonus technical features too, like a computation rule and elimination into any universe

[Kevin Buzzard]

and now you want to prove that any functor satisfying the universal property of x Y preserves colimits.

[Kevin Buzzard]

meh yeah it's kind of like one level up from the localisation situation

[Reid Barton]

The situation in homotopy theory is particularly striking because the fact that $- \times [0,1]$ is characterized by some universal property literally never comes up. I use it to define homotopies and I want to know that I can glue homotopies together to get a homotopy on a space that was glued together, and in order to do this I need to know various point-set facts about the space $[0, 1]$ and its prod with other spaces

[Reid Barton]

and at some point I need to write down an explicit formula for a map $[0, 1] \times [0, 1] \to [0, 1] \times [0, 1]$ and check that it's continuous, and I need to know what the domain is to do this

[Reid Barton]

Like, I need the fact that addition and multiplication are continuous

[Reid Barton]

and this is phrased in terms of prod

[Reid Barton]

so it's all extremely convenient; but in mathlib the products in Top are defined by some different construction

[Reid Barton]

(incidentally, Mon_ Top would be good to add to the above list!)

[Reid Barton]

https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/topological_spaces/category.lean#L42-L80 is basically the whole "theory" of products I worked with

[Matt Earnshaw]

rewinding to something more mundane, I am defining the monoidal structure of Mon manually in an attempt to ameliorate my problems above but now really fumbling with this simple lemma:

import algebra.category.Mon.limits
import category_theory.monoidal.category

open category_theory category_theory.limits category_theory.iso

namespace category_theory.monoidal

def assoc : Π (X Y Z : Mon), Mon.of (↥(Mon.of (↥X × ↥Y)) × ↥Z) ≅ Mon.of (↥X × ↥(Mon.of (↥Y × ↥Z))) :=
begin
  intros,
  apply mul_equiv.to_Mon_iso,
  refine {to_fun := _, inv_fun := _, left_inv := _, right_inv := _, map_mul' := _},
  intro,
  --- ?
  /- a: ↥(Mon.of (↥X × ↥Y)) × ↥Z
     ⊢ ↥X × ↥(Mon.of (↥Y × ↥Z)) -/
end

[Kevin Buzzard]

Did the a come from intros? Why not replace with a fancy rintro?