Ring-theoretic results in terms of categorical languages

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))

@[deprecated CommRingCat.isLocalHom_comp (since := "2024-10-10")]

theorem CommRingCat.isLocalRingHom_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))

Alias of CommRingCat.isLocalHom_comp.

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

@[deprecated isLocalHom_of_iso (since := "2024-10-10")]

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

Alias of isLocalHom_of_iso.

@[instance 100]

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

@[deprecated isLocalHom_of_isIso (since := "2024-10-10")]

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

Alias of isLocalHom_of_isIso.