Bijective Ring Homorphism an Isomorphism

Stream: maths

[Jordan Brown]

Does mathlib have the theorem showing that a bijective ring homomorphism is an isomorphism? It seems to be missing from the data.equiv.ring, is there somewhere else I should look?

[Matt Earnshaw]

import algebra.category.CommRing.basic
#check ring_equiv.to_Ring_iso

[Thomas Browning]

But there you're already assuming that you have a ring equivalence (rather than a bijective ring homomorphism)

[Matt Earnshaw]

oops

[Adam Topaz]

You can combine src#equiv.of_bijective to get this easily.

[Adam Topaz]

import data.equiv.basic
import data.equiv.ring

variables {A : Type*} [ring A]
variables {B : Type*} [ring B]

noncomputable def ring_equiv_of_bij_hom (f : A →+* B) (h : function.bijective f) : A ≃+* B :=
{ map_mul' := by apply ring_hom.map_mul,
  map_add' := by apply ring_hom.map_add,
  ..show A ≃ B, by exact equiv.of_bijective _ h }

There might be a better way. Or mathlib might already have something like this.

[Johan Commelin]

Can't you golf that to

noncomputable def ring_equiv_of_bij_hom (f : A →+* B) (h : function.bijective f) : A ≃+* B :=
{ .. f, .. equiv.of_bijective _ h }