Zulip Chat Archive

Stream: maths

Topic: Bijective Ring Homorphism an Isomorphism


Jordan Brown (Jul 29 2020 at 22:50):

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 (Jul 29 2020 at 23:59):

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

Thomas Browning (Jul 30 2020 at 00:05):

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

Matt Earnshaw (Jul 30 2020 at 00:13):

oops

Adam Topaz (Jul 30 2020 at 00:46):

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

Adam Topaz (Jul 30 2020 at 00:51):

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 (Jul 30 2020 at 03:55):

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 }

Last updated: Dec 20 2023 at 11:08 UTC