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]
:
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)]
:
@[instance 100]