mathlib documentation

algebra.category.CommRing.basic

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

We introduce the bundled categories:

def SemiRing  :
Type (u+1)

The category of semirings.

Equations
@[instance]

Equations
def SemiRing.of (R : Type u) [semiring R] :

Construct a bundled SemiRing from the underlying type and typeclass.

Equations
@[instance]

Equations
@[simp]
theorem SemiRing.coe_of (R : Type u) [semiring R] :

@[instance]

Equations
def Ring  :
Type (u+1)

The category of rings.

Equations
def Ring.of (R : Type u) [ring R] :

Construct a bundled Ring from the underlying type and typeclass.

Equations
@[instance]
def Ring.ring (R : Ring) :

Equations
@[simp]
theorem Ring.coe_of (R : Type u) [ring R] :

@[instance]

Equations
def CommSemiRing  :
Type (u+1)

The category of commutative semirings.

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

Construct a bundled CommSemiRing from the underlying type and typeclass.

Equations
@[simp]
theorem CommSemiRing.coe_of (R : Type u) [comm_semiring R] :

@[instance]

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

Equations
def CommRing  :
Type (u+1)

The category of commutative rings.

Equations
def CommRing.of (R : Type u) [comm_ring R] :

Construct a bundled CommRing from the underlying type and typeclass.

Equations
@[instance]

Equations
@[simp]
theorem CommRing.coe_of (R : Type u) [comm_ring R] :

@[instance]

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

Equations
def ring_equiv.to_Ring_iso {X Y : Type u} [ring X] [ring Y] :
X ≃+* Y(Ring.of X Ring.of 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] :

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