Making homs in CommRing

Stream: Is there code for X?

[Chris Hughes]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Chris Hughes]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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