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,
},
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