## Stream: general

### Topic: Working with bundled categories

#### Klaus Mattis (Jan 22 2022 at 09:52):

I'm a little bit puzzled, since I don't quite get how one would work with those bundled categories,
epcifically on how to convert between morphisms in the category and morphisms on the underlying objects.
Say I have

(A B C : Type) [comm_ring A][comm_ring B] [comm_ring C] (f : A ->+* B) (g : B ->+* C) (h : A ->+* C),

and I know that there is an equality CommRing.of_hom h = CommRing.of_hom f \gg CommRing.of g.

How do I get a proposition of type h = ring_hom.comp g f from the equality in the bundled category?

#### Kevin Buzzard (Jan 22 2022 at 09:54):

Not answering the question but #backticks and #mwe

#### Yaël Dillies (Jan 22 2022 at 09:57):

Sounds like you need that CommRing.of_hom is injective and that it distributes with composition.

#### Klaus Mattis (Jan 22 2022 at 10:12):

Ok, my mwe would be:

import algebra.category.CommRing

variables {A B C : Type} [comm_ring A] [comm_ring B] [comm_ring C] (f : A →+* B) (g : B →+* C) (h : A →+* C)

lemma comp_in_bundled_cat_imp_comp : (CommRing.of_hom f ≫ CommRing.of_hom g = CommRing.of_hom h) → (ring_hom.comp g f = h) := sorry


@Yaël Dillies yeah this sounds right. But I did not find anything in the library. I assume that this would be needed everywhere where one works with those bundled categories, so it should be out there somewhere?

#### Reid Barton (Jan 22 2022 at 11:16):

I think CommRing.of_hom f ≫ CommRing.of_hom g = CommRing.of_hom h and ring_hom.comp g f = h are definitionally equal, unless I'm very confused (possible).

#### Kevin Buzzard (Jan 22 2022 at 11:18):

I know that this sort of thing was part of Scott's design principles.

#### Reid Barton (Jan 22 2022 at 11:21):

By the way, if you are talking about a bunch of variable rings, I would usually start from (A B C : CommRing) (f : A ⟶ B) (g : B ⟶ C) (h : A ⟶ C) instead for a couple reasons, not least that it's ~50% shorter

#### Reid Barton (Jan 22 2022 at 11:21):

You would still probably need to make this kind of conversion at some point, though.

#### Andrew Yang (Jan 22 2022 at 11:38):

CommRing.of_hom f is by definition equal to f, and f ≫ g is by definition ring_hom.comp g f.
So regarding your original question, a type ascription should do. And for your mwe,

import algebra.category.CommRing

variables {A B C : Type} [comm_ring A] [comm_ring B] [comm_ring C] (f : A →+* B) (g : B →+* C) (h : A →+* C)

lemma comp_in_bundled_cat_imp_comp : (CommRing.of_hom f ≫ CommRing.of_hom g = CommRing.of_hom h) → (ring_hom.comp g f = h) :=  id


#### Klaus Mattis (Jan 22 2022 at 12:14):

Sometimes it can be that easy, thanks @Andrew Yang :)
I thought I tried this at some point, possibly a lot of my confusion comes from the fact
that ring_hom.comp and ∘ are different things.

Last updated: Aug 03 2023 at 10:10 UTC