Ring-theoretic results in terms of categorical languages

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance CommRingCat.isLocalRingHom_comp {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [IsLocalRingHom g] [IsLocalRingHom f] : IsLocalRingHom (CategoryTheory.CategoryStruct.comp f g)

Equations

• ⋯ = ⋯

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

@[instance 100]

instance isLocalRingHom_of_isIso {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) [CategoryTheory.IsIso f] : IsLocalRingHom f

Equations

• ⋯ = ⋯