## Stream: maths

### Topic: monoid objects again

#### Matt Earnshaw (Jul 26 2020 at 01:02):

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?

What goes wrong?

#### Matt Earnshaw (Jul 26 2020 at 01:04):

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


ah!

#### Scott Morrison (Jul 26 2020 at 01:05):

Mon_in should not be a class.

#### Scott Morrison (Jul 26 2020 at 01:05):

Let's just make it a fully bundled object.

#### Scott Morrison (Jul 26 2020 at 01:06):

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

#### Scott Morrison (Jul 26 2020 at 01:07):

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

#### Scott Morrison (Jul 26 2020 at 01:08):

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 (Jul 26 2020 at 01:10):

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 (Jul 26 2020 at 01:10):

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

#### Matt Earnshaw (Jul 26 2020 at 01:12):

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 (Jul 26 2020 at 01:15):

what's the relationship between monoidal_category and symmetric_monoidal_category?

#### Matt Earnshaw (Jul 26 2020 at 01:17):

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

oh!

#### Scott Morrison (Jul 26 2020 at 01:17):

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

#### Reid Barton (Jul 26 2020 at 01:17):

You don't want both classes as variables then

#### Scott Morrison (Jul 26 2020 at 01:18):

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

aha

#### Scott Morrison (Jul 26 2020 at 01:18):

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 (Jul 26 2020 at 01:18):

What would you suggest for this Reid?

#### Scott Morrison (Jul 26 2020 at 01:19):

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 (Jul 26 2020 at 01:19):

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

#### Scott Morrison (Jul 26 2020 at 01:46):

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 (Jul 26 2020 at 01:46):

Just let me know!

#### Adam Topaz (Jul 26 2020 at 01:47):

What's this about [[ ]]?

#### Scott Morrison (Jul 26 2020 at 01:48):

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

#### Adam Topaz (Jul 26 2020 at 01:48):

Oh that would be nice!

#### Scott Morrison (Jul 26 2020 at 01:48):

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

#### Scott Morrison (Jul 26 2020 at 01:49):

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

#### Reid Barton (Jul 26 2020 at 01:49):

Have we considered just making [] do this?

#### Matt Earnshaw (Jul 26 2020 at 01:49):

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 (Jul 26 2020 at 01:52):

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

#### Reid Barton (Jul 26 2020 at 01:54):

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

#### Scott Morrison (Jul 26 2020 at 01:55):

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 (Jul 26 2020 at 02:06):

@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 (Jul 26 2020 at 02:10):

well that seems a bit more concise :-)

#### Scott Morrison (Jul 26 2020 at 02:11):

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

#### Matt Earnshaw (Jul 26 2020 at 02:13):

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 (Jul 26 2020 at 02:14):

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 (Jul 26 2020 at 02:14):

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

#### Scott Morrison (Jul 26 2020 at 02:15):

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 (Jul 26 2020 at 02:16):

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

#### Matt Earnshaw (Jul 26 2020 at 02:27):

now working here, with shameless inspiration

#### Scott Morrison (Jul 26 2020 at 12:42):

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

#### Matt Earnshaw (Jul 26 2020 at 21:17):

@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 (Jul 26 2020 at 22:10):

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 (Jul 26 2020 at 22:11):

IMO, this approach is not really sustainable.

#### Reid Barton (Jul 26 2020 at 22:13):

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

#### Scott Morrison (Jul 26 2020 at 22:53):

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 (Jul 26 2020 at 22:54):

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 (Jul 26 2020 at 22:55):

The one in category_theory.monoidal.types.

#### Reid Barton (Jul 26 2020 at 22:56):

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 (Jul 26 2020 at 22:57):

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 (Jul 26 2020 at 23:01):

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 (Jul 26 2020 at 23:12):

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 (Jul 26 2020 at 23:16):

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

#### Reid Barton (Jul 26 2020 at 23:16):

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 (Jul 26 2020 at 23:17):

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

#### Kevin Buzzard (Jul 26 2020 at 23:17):

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

#### Kevin Buzzard (Jul 26 2020 at 23:17):

What do we have that this system doesn't?

#### Reid Barton (Jul 26 2020 at 23:17):

I would argue that you do have to do some work

#### Reid Barton (Jul 26 2020 at 23:18):

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

#### Kevin Buzzard (Jul 26 2020 at 23:18):

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

#### Reid Barton (Jul 26 2020 at 23:19):

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

#### Kevin Buzzard (Jul 26 2020 at 23:19):

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 (Jul 26 2020 at 23:20):

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 (Jul 26 2020 at 23:20):

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 (Jul 26 2020 at 23:21):

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

#### Kevin Buzzard (Jul 26 2020 at 23:21):

Not if they're canonically isomorphic

#### Reid Barton (Jul 26 2020 at 23:21):

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

#### Reid Barton (Jul 26 2020 at 23:21):

that requires LEM for example

#### Reid Barton (Jul 26 2020 at 23:22):

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 (Jul 26 2020 at 23:22):

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 (Jul 26 2020 at 23:23):

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

#### Reid Barton (Jul 26 2020 at 23:23):

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

#### Kevin Buzzard (Jul 26 2020 at 23:24):

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

#### Kevin Buzzard (Jul 26 2020 at 23:24):

like I was with localisations

#### Kevin Buzzard (Jul 26 2020 at 23:24):

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

#### Reid Barton (Jul 26 2020 at 23:25):

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 (Jul 26 2020 at 23:26):

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

#### Kevin Buzzard (Jul 26 2020 at 23:27):

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 (Jul 26 2020 at 23:30):

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 (Jul 26 2020 at 23:31):

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

#### Kevin Buzzard (Jul 26 2020 at 23:32):

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

#### Kevin Buzzard (Jul 26 2020 at 23:32):

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

#### Reid Barton (Jul 26 2020 at 23:34):

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 (Jul 26 2020 at 23:35):

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 (Jul 26 2020 at 23:36):

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

#### Reid Barton (Jul 26 2020 at 23:36):

and this is phrased in terms of prod

#### Reid Barton (Jul 26 2020 at 23:38):

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

#### Reid Barton (Jul 26 2020 at 23:39):

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

#### Reid Barton (Jul 26 2020 at 23:44):

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 (Jul 29 2020 at 23:52):

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 (Jul 30 2020 at 07:26):

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

Last updated: May 10 2021 at 08:14 UTC