Working with bundled categories

Stream: general

[Klaus Mattis]

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]

Not answering the question but #backticks and #mwe

[Yaël Dillies]

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

[Klaus Mattis]

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]

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]

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

[Reid Barton]

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]

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

[Andrew Yang]

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]

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.