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
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def SemiRing.of (R : Type u) [semiring R] :

Construct a bundled SemiRing from the underlying type and typeclass.

Equations
@[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
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def Ring.of (R : Type u) [ring R] :

Construct a bundled Ring from the underlying type and typeclass.

Equations
@[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
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def CommSemiRing.of (R : Type u)  :

Construct a bundled CommSemiRing from the underlying type and typeclass.

Equations
@[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
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def CommRing.of (R : Type u) [comm_ring R] :

Construct a bundled CommRing from the underlying type and typeclass.

Equations
@[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
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
@[protected, instance]
@[protected, instance]