← Copula mathematical handbook

Ring-theoretic results in terms of categorical language

instance localization_unit_isIso (R : CommRingCat) : CategoryTheory.IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))

instance localization_unit_isIso' (R : CommRingCat) : CategoryTheory.IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))

theorem IsLocalization.epi {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_1) [CommRing S] [Algebra R S] [IsLocalization M S] : CategoryTheory.Epi (CommRingCat.ofHom (algebraMap R S))

instance Localization.epi {R : Type u_1} [CommRing R] (M : Submonoid R) : CategoryTheory.Epi (CommRingCat.ofHom (algebraMap R (Localization M)))

instance Localization.epi' {R : CommRingCat} (M : Submonoid ↑R) : CategoryTheory.Epi (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))

instance CommRingCat.isLocalHom_comp {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [IsLocalHom (Hom.hom g)] [IsLocalHom (Hom.hom f)] : IsLocalHom (Hom.hom (CategoryTheory.CategoryStruct.comp f g))

theorem isLocalHom_of_iso {R S : CommRingCat} (f : R ≅ S) : IsLocalHom (CommRingCat.Hom.hom f.hom)

@[instance 100]

instance isLocalHom_of_isIso {R S : CommRingCat} (f : R ⟶ S) [CategoryTheory.IsIso f] : IsLocalHom (CommRingCat.Hom.hom f)