ring_hom ≃ algebra

Stream: maths

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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!