Zulip Chat Archive

Stream: Is there code for X?

Topic: Making homs in CommRing


view this post on Zulip Chris Hughes (May 26 2020 at 07:42):

I can't work out how to do this.

import algebra.category.CommRing.basic

open category_theory

example : Ring.of   Ring.of  := sorry

view this post on Zulip Markus Himmel (May 26 2020 at 07:50):

import algebra.category.CommRing.basic

open category_theory

def something :  →+*  := sorry

example : Ring.of   Ring.of  := something

seems to work just fine for me

view this post on Zulip Chris Hughes (May 26 2020 at 08:05):

Ah, I didn't realise that the definition was just ring_hom

view this post on Zulip Kevin Buzzard (May 26 2020 at 09:57):

There are layers and layers in category theory, that's one reason it's so hard to use

view this post on Zulip Kevin Buzzard (May 26 2020 at 09:58):

Using the interface is fine if you have access to examples, and making it can be very hard

view this post on Zulip Chris Hughes (May 26 2020 at 10:08):

I feel like there's quite a lot of erw in category_theory. You have to know how things unfold

view this post on Zulip Reid Barton (May 26 2020 at 10:34):

The erws are mainly to deal with definitional equalities like (F >>> G).obj X = G.obj (F.obj X) appearing in implicit arguments of things like composition, I think.

view this post on Zulip Reid Barton (May 26 2020 at 10:35):

The alternative to knowing how (F >>> G).obj unfolds would be not being able to compose a map into (FG)X(FG)X with a map out of F(GX)F(GX)

view this post on Zulip Mario Carneiro (May 26 2020 at 10:36):

it's fine, you just right whisker with the associator (or something...)

view this post on Zulip Reid Barton (May 26 2020 at 10:38):

right, this is sort of like pretending that Cat isn't actually a strict 2-category, but only a bicategory

view this post on Zulip Reid Barton (May 26 2020 at 10:39):

In math people usually do the reverse (suppress all the coherence morphisms when computing in a bicategory), because it's so dreadful to write them out

view this post on Zulip Reid Barton (May 26 2020 at 10:40):

The other issue at hand here is a questionable behavior of simp (which we now at least understand thanks to Gabriel) which causes it to take syntactic matching very seriously


Last updated: May 19 2021 at 03:22 UTC