# mathlibdocumentation

algebra.category.CommRing.basic

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

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
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.

@[instance]
Equations
@[instance]
@[instance]
@[instance]
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
@[instance]
Equations
@[instance]
Equations
@[simp]
theorem SemiRing.coe_of (R : Type u) [semiring R] :
@[instance]
Equations
@[instance]
Equations
def Ring  :
Type (u+1)

The category of rings.

Equations
@[instance]
Equations
@[instance]
@[instance]
@[instance]
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
@[instance]
Equations
@[instance]
def Ring.ring (R : Ring) :
Equations
@[simp]
theorem Ring.coe_of (R : Type u) [ring R] :
@[instance]
Equations
@[instance]
Equations
def CommSemiRing  :
Type (u+1)

The category of commutative semirings.

Equations
@[instance]
@[instance]
def CommSemiRing.of (R : Type u)  :

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
@[instance]
Equations
@[instance]
Equations
@[simp]
theorem CommSemiRing.coe_of (R : Type u)  :
= R
@[instance]
Equations
@[instance]

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

Equations
def CommRing  :
Type (u+1)

The category of commutative rings.

Equations
@[instance]
Equations
@[instance]
@[instance]
@[instance]
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
@[instance]
Equations
@[instance]
Equations
@[simp]
theorem CommRing.coe_of (R : Type u) [comm_ring R] :
@[instance]
Equations
@[instance]

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

Equations
@[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
def ring_equiv_iso_CommRing_iso {X Y : Type u} [comm_ring X] [comm_ring Y] :
X ≃+* Y

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

Equations