Documentation

Mathlib.Algebra.Category.Ring.Instances

Ring-theoretic results in terms of categorical languages #

source
instance localization_unit_isIso (R : CommRingCat) :
CategoryTheory.IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))
Equations
  • ⋯ = ⋯
source
instance localization_unit_isIso' (R : CommRingCat) :
CategoryTheory.IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))
Equations
  • ⋯ = ⋯
source
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))
source
instance Localization.epi {R : Type u_1} [CommRing R] (M : Submonoid R) :
CategoryTheory.Epi (CommRingCat.ofHom (algebraMap R (Localization M)))
Equations
  • ⋯ = ⋯
source
instance Localization.epi' {R : CommRingCat} (M : Submonoid ↑R) :
CategoryTheory.Epi (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))
Equations
  • ⋯ = ⋯
source
@[instance 50]
instance instIsLocalHomαCommRingHomCommRingCatOf {R : Type u_1} [CommRing R] {S : CommRingCat} (f : CommRingCat.of R ⟶ S) [IsLocalHom f] :
IsLocalHom f
Equations
  • ⋯ = ⋯
source
@[instance 50]
instance instIsLocalHomαCommRingHomCommRingCatOf_1 {R : CommRingCat} {S : Type u_1} [CommRing S] (f : R ⟶ CommRingCat.of S) [IsLocalHom f] :
IsLocalHom f
Equations
  • ⋯ = ⋯
source
@[instance 50]
instance instIsLocalHomHomCommRingCatOfOfαCommRing {R : Type u} {S : Type u} [CommRing R] [CommRing S] (f : CommRingCat.of R ⟶ CommRingCat.of S) [IsLocalHom f] :
IsLocalHom f
Equations
  • ⋯ = ⋯
source
instance instIsLocalHomαCommRingRingHomOfHomCommRingCat {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) [IsLocalHom f] :
IsLocalHom f
Equations
  • ⋯ = ⋯
source
theorem CommRingCat.isLocalHom_comp {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [IsLocalHom g] [IsLocalHom f] :
IsLocalHom (CategoryTheory.CategoryStruct.comp f g)
source
@[deprecated CommRingCat.isLocalHom_comp]
theorem CommRingCat.isLocalRingHom_comp {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [IsLocalHom g] [IsLocalHom f] :
IsLocalHom (CategoryTheory.CategoryStruct.comp f g)

Alias of CommRingCat.isLocalHom_comp.

source
theorem isLocalHom_of_iso {R : CommRingCat} {S : CommRingCat} (f : R ≅ S) :
IsLocalHom f.hom
source
@[deprecated isLocalHom_of_iso]
theorem isLocalRingHom_of_iso {R : CommRingCat} {S : CommRingCat} (f : R ≅ S) :
IsLocalHom f.hom

Alias of isLocalHom_of_iso.

source
theorem isLocalHom_of_isIso {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) [CategoryTheory.IsIso f] :
IsLocalHom f
source
@[deprecated isLocalHom_of_isIso]
theorem isLocalRingHom_of_isIso {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) [CategoryTheory.IsIso f] :
IsLocalHom f

Alias of isLocalHom_of_isIso.