mathlib3 documentation

algebra.category.Ring.instances

Ring-theoretic results in terms of categorical languages #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[protected, instance]
def localization_unit_is_iso (R : CommRing) :
category_theory.is_iso (CommRing.of_hom (algebra_map ↥R (localization.away 1)))
source
@[protected, instance]
def localization_unit_is_iso' (R : CommRing) :
category_theory.is_iso (CommRing.of_hom (algebra_map ↥R (localization.away 1)))
source
theorem is_localization.epi {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_1) [comm_ring S] [algebra R S] [is_localization M S] :
category_theory.epi (CommRing.of_hom (algebra_map R S))
source
@[protected, instance]
def localization.epi {R : Type u_1} [comm_ring R] (M : submonoid R) :
category_theory.epi (CommRing.of_hom (algebra_map R (localization M)))
source
@[protected, instance]
def localization.epi' {R : CommRing} (M : submonoid ↥R) :
category_theory.epi (CommRing.of_hom (algebra_map ↥R (localization M)))
source
@[protected, instance]
def CommRing.is_local_ring_hom_comp {R S T : CommRing} (f : R ⟶ S) (g : S ⟶ T) [is_local_ring_hom g] [is_local_ring_hom f] :
is_local_ring_hom (f ≫ g)
source
theorem is_local_ring_hom_of_iso {R S : CommRing} (f : R ≅ S) :
is_local_ring_hom f.hom
source
@[protected, instance]
def is_local_ring_hom_of_is_iso {R S : CommRing} (f : R ⟶ S) [category_theory.is_iso f] :
is_local_ring_hom f