# Zulip Chat Archive

## 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: Dec 20 2023 at 11:08 UTC