[GOAL]
R : CommRingCat
⊢ IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))
[PROOFSTEP]
cases R
[GOAL]
case mk
α✝ : Type ?u.2107
str✝ : CommRing α✝
⊢ IsIso (CommRingCat.ofHom (algebraMap (↑(Bundled.mk α✝)) (Localization.Away 1)))
[PROOFSTEP]
exact localization_unit_isIso _
[GOAL]
R : CommRingCat
M : Submonoid ↑R
⊢ Epi (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))
[PROOFSTEP]
rcases R with ⟨α, str⟩
[GOAL]
case mk
α : Type ?u.6171
str : CommRing α
M : Submonoid ↑(Bundled.mk α)
⊢ Epi (CommRingCat.ofHom (algebraMap (↑(Bundled.mk α)) (Localization M)))
[PROOFSTEP]
exact IsLocalization.epi M _
[GOAL]
R S : CommRingCat
f : R ≅ S
a : ↑R
ha : IsUnit (↑f.hom a)
⊢ IsUnit a
[PROOFSTEP]
convert f.inv.isUnit_map ha
[GOAL]
case h.e'_3
R S : CommRingCat
f : R ≅ S
a : ↑R
ha : IsUnit (↑f.hom a)
⊢ a = ↑f.inv (↑f.hom a)
[PROOFSTEP]
exact (RingHom.congr_fun f.hom_inv_id _).symm
