## Stream: Is there code for X?

### Topic: Making homs in CommRing

#### 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

#### 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

#### Chris Hughes (May 26 2020 at 08:05):

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

#### 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

#### 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

#### 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

#### 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.

#### 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$ with a map out of $F(GX)$

#### Mario Carneiro (May 26 2020 at 10:36):

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

#### 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

#### 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

#### 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