# mathlib3documentation

algebra.category.Ring.basic

# Category instances for semiring, ring, comm_semiring, and comm_ring. #

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

We introduce the bundled categories:

• SemiRing
• Ring
• CommSemiRing
• CommRing along with the relevant forgetful functors between them.
def SemiRing  :
Type (u+1)

The category of semirings.

Equations
Instances for SemiRing
@[reducible]
def SemiRing.assoc_ring_hom (M : Type u_1) (N : Type u_2) [semiring M] [semiring N] :
Type (max u_1 u_2)

ring_hom doesn't actually assume associativity. This alias is needed to make the category theory machinery work. We use the same trick in category_theory.Mon.assoc_monoid_hom.

@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
def SemiRing.of (R : Type u) [semiring R] :

Construct a bundled SemiRing from the underlying type and typeclass.

Equations
def SemiRing.of_hom {R S : Type u} [semiring R] [semiring S] (f : R →+* S) :

Typecheck a ring_hom as a morphism in SemiRing.

Equations
@[simp]
theorem SemiRing.of_hom_apply {R S : Type u} [semiring R] [semiring S] (f : R →+* S) (x : R) :
x = f x
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem SemiRing.coe_of (R : Type u) [semiring R] :
@[protected, instance]
Equations
@[protected, instance]
Equations
def Ring  :
Type (u+1)

The category of rings.

Equations
Instances for Ring
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def Ring.has_coe_to_sort  :
(Type u_1)
def Ring.of (R : Type u) [ring R] :

Construct a bundled Ring from the underlying type and typeclass.

Equations
def Ring.of_hom {R S : Type u} [ring R] [ring S] (f : R →+* S) :

Typecheck a ring_hom as a morphism in Ring.

Equations
• = f
@[simp]
theorem Ring.of_hom_apply {R S : Type u} [ring R] [ring S] (f : R →+* S) (x : R) :
@[protected, instance]
Equations
@[protected, instance]
def Ring.ring (R : Ring) :
Equations
@[simp]
theorem Ring.coe_of (R : Type u) [ring R] :
@[protected, instance]
Equations
@[protected, instance]
Equations
def CommSemiRing  :
Type (u+1)

The category of commutative semirings.

Equations
Instances for CommSemiRing
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations

Construct a bundled CommSemiRing from the underlying type and typeclass.

Equations
def CommSemiRing.of_hom {R S : Type u} (f : R →+* S) :

Typecheck a ring_hom as a morphism in CommSemiRing.

Equations
@[simp]
theorem CommSemiRing.of_hom_apply {R S : Type u} (f : R →+* S) (x : R) :
x = f x
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem CommSemiRing.coe_of (R : Type u)  :
= R
@[protected, instance]
Equations
@[protected, instance]

The forgetful functor from commutative rings to (multiplicative) commutative monoids.

Equations
def CommRing  :
Type (u+1)

The category of commutative rings.

Equations
Instances for CommRing
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
def CommRing.of (R : Type u) [comm_ring R] :

Construct a bundled CommRing from the underlying type and typeclass.

Equations
def CommRing.of_hom {R S : Type u} [comm_ring R] [comm_ring S] (f : R →+* S) :

Typecheck a ring_hom as a morphism in CommRing.

Equations
Instances for CommRing.of_hom
@[simp]
theorem CommRing.of_hom_apply {R S : Type u} [comm_ring R] [comm_ring S] (f : R →+* S) (x : R) :
x = f x
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem CommRing.coe_of (R : Type u) [comm_ring R] :
@[protected, instance]
Equations
@[protected, instance]

The forgetful functor from commutative rings to (multiplicative) commutative monoids.

Equations
@[protected, instance]
Equations
def ring_equiv.to_Ring_iso {X Y : Type u} [ring X] [ring Y] (e : X ≃+* Y) :

Build an isomorphism in the category Ring from a ring_equiv between rings.

Equations
@[simp]
theorem ring_equiv.to_Ring_iso_inv {X Y : Type u} [ring X] [ring Y] (e : X ≃+* Y) :
@[simp]
theorem ring_equiv.to_Ring_iso_hom {X Y : Type u} [ring X] [ring Y] (e : X ≃+* Y) :
@[simp]
theorem ring_equiv.to_CommRing_iso_hom {X Y : Type u} [comm_ring X] [comm_ring Y] (e : X ≃+* Y) :
def ring_equiv.to_CommRing_iso {X Y : Type u} [comm_ring X] [comm_ring Y] (e : X ≃+* Y) :

Build an isomorphism in the category CommRing from a ring_equiv between comm_rings.

Equations
@[simp]
theorem ring_equiv.to_CommRing_iso_inv {X Y : Type u} [comm_ring X] [comm_ring Y] (e : X ≃+* Y) :

Build a ring_equiv from an isomorphism in the category Ring.

Equations

Build a ring_equiv from an isomorphism in the category CommRing.

Equations
def ring_equiv_iso_Ring_iso {X Y : Type u} [ring X] [ring Y] :

Ring equivalences between rings are the same as (isomorphic to) isomorphisms in Ring.

Equations

Ring equivalences between comm_rings are the same as (isomorphic to) isomorphisms in CommRing.

Equations
@[protected, instance]
@[protected, instance]
theorem CommRing.comp_eq_ring_hom_comp {R S T : CommRing} (f : R S) (g : S T) :
f g =
theorem CommRing.ring_hom_comp_eq_comp {R S T : Type u_1} [comm_ring R] [comm_ring S] [comm_ring T] (f : R →+* S) (g : S →+* T) :
g.comp f =