Ring-theoretic results in terms of categorical languages #
instance
localization_unit_isIso
(R : CommRingCat)
:
CategoryTheory.IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))
Equations
- One or more equations did not get rendered due to their size.
instance
localization_unit_isIso'
(R : CommRingCat)
:
CategoryTheory.IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))
Equations
- (_ : CategoryTheory.IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))) = (_ : 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]
:
Equations
- (_ : CategoryTheory.Epi (CommRingCat.ofHom (algebraMap R (Localization M)))) = (_ : CategoryTheory.Epi (CommRingCat.ofHom (algebraMap R (Localization M))))
instance
Localization.epi'
{R : CommRingCat}
(M : Submonoid ↑R)
:
CategoryTheory.Epi (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))
Equations
- (_ : CategoryTheory.Epi (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))) = (_ : CategoryTheory.Epi (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))
instance
CommRingCat.isLocalRingHom_comp
{R : CommRingCat}
{S : CommRingCat}
{T : CommRingCat}
(f : R ⟶ S)
(g : S ⟶ T)
[IsLocalRingHom g]
[IsLocalRingHom f]
:
Equations
- (_ : IsLocalRingHom (CategoryTheory.CategoryStruct.comp f g)) = (_ : IsLocalRingHom (RingHom.comp g f))
instance
isLocalRingHom_of_isIso
{R : CommRingCat}
{S : CommRingCat}
(f : R ⟶ S)
[CategoryTheory.IsIso f]
:
Equations
- (_ : IsLocalRingHom f) = (_ : IsLocalRingHom (CategoryTheory.asIso f).hom)