# Zulip Chat Archive

## Stream: maths

### Topic: ring_hom ≃ algebra

#### Kevin Buzzard (Mar 21 2020 at 18:26):

In my cosy maths world where all rings are commutative, `ring_hom`

and `algebra`

are the same. So how come the mathlib people decided that one of these is better off as a class, and the other one as a structure?

import ring_theory.algebra example (R : Type*) [comm_ring R] (A : Type*) [comm_ring A] : ring_hom R A ≃ algebra R A := { to_fun := λ f, { smul := λ r a, f r * a, to_fun := f, hom := by apply_instance, commutes' := λ _ _, mul_comm _ _, smul_def' := λ _ _, rfl }, inv_fun := λ h, by letI := h; exact { to_fun := h.to_fun, map_one' := algebra.map_one R A, map_mul' := algebra.map_mul A, map_zero' := algebra.map_zero R A, map_add' := algebra.map_add A }, left_inv := begin intro f, ext x, refl, end, right_inv := begin intro h, cases h, dsimp, congr', cases h__to_has_scalar, congr', ext r a, exact (h_smul_def' r a).symm, end }

#### Chris Hughes (Mar 21 2020 at 18:38):

It will be to do with the module structure induced by the ring hom.

#### Kevin Buzzard (Mar 21 2020 at 18:54):

If I am talking about $A$ as an $R$-algebra then it might well be the case that I will soon want to talk about $A$ as an $R$-module. But if I'm just talking about a ring homomorphism then there's less of a chance? Maybe this is true but I'm still a bit confused as to how the way I'm thinking about something should dictate how it is implemented internally.

#### Johan Commelin (Mar 21 2020 at 19:05):

I think it's a difference in emphasis. Do you want to take one ring hom and make it "the canonical ring hom" from A to B? Then B is an A-algebra. But if you just want to talk about the map, but it's nothing special, then you use ring_hom.

#### Kevin Buzzard (Mar 21 2020 at 19:06):

Aah you're right: with the algebra structure you're kind of promising that this is the only ring hom from R to A that you'll ever be interested in. Very nice!

Last updated: May 06 2021 at 18:20 UTC