Zulip Chat Archive

Stream: maths

Topic: monoid objects again


view this post on Zulip 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?

view this post on Zulip Scott Morrison (Jul 26 2020 at 01:03):

What goes wrong?

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 26 2020 at 01:05):

ah!

view this post on Zulip Scott Morrison (Jul 26 2020 at 01:05):

Mon_in should not be a class.

view this post on Zulip Scott Morrison (Jul 26 2020 at 01:05):

Let's just make it a fully bundled object.

view this post on Zulip Scott Morrison (Jul 26 2020 at 01:06):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 26 2020 at 01:15):

what's the relationship between monoidal_category and symmetric_monoidal_category?

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 26 2020 at 01:17):

oh!

view this post on Zulip Scott Morrison (Jul 26 2020 at 01:17):

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

view this post on Zulip Reid Barton (Jul 26 2020 at 01:17):

You don't want both classes as variables then

view this post on Zulip Scott Morrison (Jul 26 2020 at 01:18):

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

view this post on Zulip Matt Earnshaw (Jul 26 2020 at 01:18):

aha

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 26 2020 at 01:18):

What would you suggest for this Reid?

view this post on Zulip 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. :-)

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Scott Morrison (Jul 26 2020 at 01:46):

Just let me know!

view this post on Zulip Adam Topaz (Jul 26 2020 at 01:47):

What's this about [[ ]]?

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jul 26 2020 at 01:48):

Oh that would be nice!

view this post on Zulip 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].

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jul 26 2020 at 01:49):

Have we considered just making [] do this?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Matt Earnshaw (Jul 26 2020 at 02:10):

well that seems a bit more concise :-)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?)

view this post on Zulip 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.

view this post on Zulip 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. :-)

view this post on Zulip 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.

view this post on Zulip Matt Earnshaw (Jul 26 2020 at 02:27):

now working here, with shameless inspiration

view this post on Zulip Scott Morrison (Jul 26 2020 at 12:42):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 26 2020 at 22:11):

IMO, this approach is not really sustainable.

view this post on Zulip Reid Barton (Jul 26 2020 at 22:13):

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

view this post on Zulip 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"?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jul 26 2020 at 22:55):

The one in category_theory.monoidal.types.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 23:17):

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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 23:17):

What do we have that this system doesn't?

view this post on Zulip Reid Barton (Jul 26 2020 at 23:17):

I would argue that you do have to do some work

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 23:18):

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

view this post on Zulip Reid Barton (Jul 26 2020 at 23:19):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 23:21):

Not if they're canonically isomorphic

view this post on Zulip Reid Barton (Jul 26 2020 at 23:21):

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

view this post on Zulip Reid Barton (Jul 26 2020 at 23:21):

that requires LEM for example

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 26 2020 at 23:23):

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

view this post on Zulip Reid Barton (Jul 26 2020 at 23:23):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 23:24):

like I was with localisations

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 23:24):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)"

view this post on Zulip Reid Barton (Jul 26 2020 at 23:30):

Anyways these are not facts of a formal nature I have in mind. For example ×Y- \times Y preserves colimits if YY is locally compact--obviously it can't be too formal because it has the condition "YY 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 23:32):

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

view this post on Zulip Reid Barton (Jul 26 2020 at 23:34):

The situation in homotopy theory is particularly striking because the fact that ×[0,1]- \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][0, 1] and its prod with other spaces

view this post on Zulip 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]×[0,1][0,1]×[0,1][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

view this post on Zulip Reid Barton (Jul 26 2020 at 23:36):

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

view this post on Zulip Reid Barton (Jul 26 2020 at 23:36):

and this is phrased in terms of prod

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 26 2020 at 23:39):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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