# Documentation

Mathlib.Algebra.Category.Ring.Basic

# Category instances for Semiring, Ring, CommSemiring, and CommRing. #

We introduce the bundled categories:

• SemiRingCat
• RingCat
• CommSemiRingCat
• CommRingCat along with the relevant forgetful functors between them.
def SemiRingCat :
Type (u + 1)

The category of semirings.

Instances For
@[inline, reducible]
abbrev SemiRingCatMax :
Type ((max u1 u2) + 1)

An alias for Semiring.{max u v}, to deal around unification issues.

Instances For
@[inline, reducible]
abbrev SemiRingCat.AssocRingHom (M : Type u_1) (N : Type u_2) [] [] :
Type (max u_1 u_2)

RingHom doesn't actually assume associativity. This alias is needed to make the category theory machinery work. We use the same trick in MonCat.AssocMonoidHom.

Instances For
Instances For
theorem SemiRingCat.coe_comp {X : SemiRingCat} {Y : SemiRingCat} {Z : SemiRingCat} {f : X Y} {g : Y Z} :
= g f
@[simp]
theorem SemiRingCat.forget_map {X : SemiRingCat} {Y : SemiRingCat} (f : X Y) :
().map f = f
theorem SemiRingCat.ext {X : SemiRingCat} {Y : SemiRingCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
f = g

Construct a bundled SemiRing from the underlying type and typeclass.

Instances For
@[simp]
theorem SemiRingCat.coe_of (R : Type u) [] :
↑() = R
@[simp]
theorem SemiRingCat.RingEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+* Y) :
e = e
def SemiRingCat.ofHom {R : Type u} {S : Type u} [] [] (f : R →+* S) :

Typecheck a RingHom as a morphism in SemiRingCat.

Instances For
@[simp]
theorem SemiRingCat.ofHom_apply {R : Type u} {S : Type u} [] [] (f : R →+* S) (x : R) :
↑() x = f x
@[simp]
theorem RingEquiv.toSemiRingCatIso_hom {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+* Y) :
@[simp]
theorem RingEquiv.toSemiRingCatIso_inv {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+* Y) :
def RingEquiv.toSemiRingCatIso {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+* Y) :

Ring equivalence are isomorphisms in category of semirings

Instances For
def RingCat :
Type (u + 1)

The category of rings.

Instances For
instance RingCat.instRing (X : RingCat) :
Ring X
instance RingCat.instRing' (X : RingCat) :
Ring (().obj X)
instance RingCat.instRingHomClass {X : RingCat} {Y : RingCat} :
RingHomClass (X Y) X Y
theorem RingCat.coe_comp {X : RingCat} {Y : RingCat} {Z : RingCat} {f : X Y} {g : Y Z} :
= g f
@[simp]
theorem RingCat.forget_map {X : RingCat} {Y : RingCat} (f : X Y) :
().map f = f
theorem RingCat.ext {X : RingCat} {Y : RingCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
f = g
def RingCat.of (R : Type u) [Ring R] :

Construct a bundled RingCat from the underlying type and typeclass.

Instances For
def RingCat.ofHom {R : Type u} {S : Type u} [Ring R] [Ring S] (f : R →+* S) :

Typecheck a RingHom as a morphism in RingCat.

Instances For
@[simp]
theorem RingCat.coe_of (R : Type u) [Ring R] :
↑() = R
@[simp]
theorem RingCat.RingEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [Ring X] [Ring Y] (e : X ≃+* Y) :
e = e
def CommSemiRingCat :
Type (u + 1)

The category of commutative semirings.

Instances For
Instances For
theorem CommSemiRingCat.coe_comp {X : CommSemiRingCat} {Y : CommSemiRingCat} {Z : CommSemiRingCat} {f : X Y} {g : Y Z} :
= g f
@[simp]
theorem CommSemiRingCat.forget_map {X : CommSemiRingCat} {Y : CommSemiRingCat} (f : X Y) :
= f
theorem CommSemiRingCat.ext {X : CommSemiRingCat} {Y : CommSemiRingCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
f = g

Construct a bundled CommSemiRingCat from the underlying type and typeclass.

Instances For
def CommSemiRingCat.ofHom {R : Type u} {S : Type u} [] [] (f : R →+* S) :

Typecheck a RingHom as a morphism in CommSemiRingCat.

Instances For
@[simp]
theorem CommSemiRingCat.RingEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+* Y) :
e = e
@[simp]
theorem CommSemiRingCat.coe_of (R : Type u) [] :
↑() = R

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

@[simp]
theorem RingEquiv.toCommSemiRingCatIso_inv {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+* Y) :
@[simp]
theorem RingEquiv.toCommSemiRingCatIso_hom {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+* Y) :
def RingEquiv.toCommSemiRingCatIso {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+* Y) :

Ring equivalence are isomorphisms in category of commutative semirings

Instances For
def CommRingCat :
Type (u + 1)

The category of commutative rings.

Instances For
Instances For
theorem CommRingCat.coe_comp {X : CommRingCat} {Y : CommRingCat} {Z : CommRingCat} {f : X Y} {g : Y Z} :
= g f
@[simp]
theorem CommRingCat.forget_map {X : CommRingCat} {Y : CommRingCat} (f : X Y) :
().map f = f
theorem CommRingCat.ext {X : CommRingCat} {Y : CommRingCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
f = g

Construct a bundled CommRingCat from the underlying type and typeclass.

Instances For
def CommRingCat.ofHom {R : Type u} {S : Type u} [] [] (f : R →+* S) :

Typecheck a RingHom as a morphism in CommRingCat.

Instances For
@[simp]
theorem CommRingCat.RingEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [] [] (e : X ≃+* Y) :
e = e
@[simp]
theorem CommRingCat.coe_of (R : Type u) [] :
↑() = R

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

@[simp]
theorem RingEquiv.toRingCatIso_inv {X : Type u} {Y : Type u} [Ring X] [Ring Y] (e : X ≃+* Y) :
@[simp]
theorem RingEquiv.toRingCatIso_hom {X : Type u} {Y : Type u} [Ring X] [Ring Y] (e : X ≃+* Y) :
def RingEquiv.toRingCatIso {X : Type u} {Y : Type u} [Ring X] [Ring Y] (e : X ≃+* Y) :

Build an isomorphism in the category RingCat from a RingEquiv between RingCats.

Instances For
@[simp]
theorem RingEquiv.toCommRingCatIso_hom {X : Type u} {Y : Type u} [] [] (e : X ≃+* Y) :
@[simp]
theorem RingEquiv.toCommRingCatIso_inv {X : Type u} {Y : Type u} [] [] (e : X ≃+* Y) :
def RingEquiv.toCommRingCatIso {X : Type u} {Y : Type u} [] [] (e : X ≃+* Y) :

Build an isomorphism in the category CommRingCat from a RingEquiv between CommRingCats.

Instances For

Build a RingEquiv from an isomorphism in the category RingCat.

Instances For

Build a RingEquiv from an isomorphism in the category CommRingCat.

Instances For
def ringEquivIsoRingIso {X : Type u} {Y : Type u} [Ring X] [Ring Y] :
X ≃+* Y

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

Instances For
def ringEquivIsoCommRingIso {X : Type u} {Y : Type u} [] [] :
X ≃+* Y

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

Instances For
theorem CommRingCat.comp_eq_ring_hom_comp {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R S) (g : S T) :
theorem CommRingCat.ringHom_comp_eq_comp {R : Type u_1} {S : Type u_1} {T : Type u_1} [] [] [] (f : R →+* S) (g : S →+* T) :