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.

@[inline, reducible]

abbrev SemiRingCatMax : Type ((max u1 u2) + 1)

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

@[inline, reducible]

abbrev SemiRingCat.AssocRingHom (M : Type u_1) (N : Type u_2) [Semiring M] [Semiring N] : 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.

instance SemiRingCat.bundledHom : CategoryTheory.BundledHom SemiRingCat.AssocRingHom

instance SemiRingCat.instConcreteCategorySemiRingCatInstSemiRingCatLargeCategory : CategoryTheory.ConcreteCategory SemiRingCat

instance SemiRingCat.instCoeSortSemiRingCatType : CoeSort SemiRingCat (Type u_1)

def SemiRingCat.forget_obj_eq_coe (R : SemiRingCat) : Prop

instance SemiRingCat.instSemiring (X : SemiRingCat) : Semiring ↑X

instance SemiRingCat.instSemiring' (X : SemiRingCat) : Semiring ((CategoryTheory.forget SemiRingCat).obj X)

instance SemiRingCat.instRingHomClass {X : SemiRingCat} {Y : SemiRingCat} : RingHomClass (X ⟶ Y) ↑X ↑Y

theorem SemiRingCat.coe_id {X : SemiRingCat} : ↑(CategoryTheory.CategoryStruct.id X) = id

theorem SemiRingCat.coe_comp {X : SemiRingCat} {Y : SemiRingCat} {Z : SemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : ↑(CategoryTheory.CategoryStruct.comp f g) = ↑g ∘ ↑f

@[simp]

theorem SemiRingCat.forget_map {X : SemiRingCat} {Y : SemiRingCat} (f : X ⟶ Y) : (CategoryTheory.forget SemiRingCat).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

def SemiRingCat.of (R : Type u) [Semiring R] : SemiRingCat

Construct a bundled SemiRing from the underlying type and typeclass.

@[simp]

theorem SemiRingCat.coe_of (R : Type u) [Semiring R] : ↑(SemiRingCat.of R) = R

@[simp]

theorem SemiRingCat.RingEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [Semiring X] [Semiring Y] (e : X ≃+* Y) : ↑↑e = ↑e

instance SemiRingCat.instInhabitedSemiRingCat : Inhabited SemiRingCat

instance SemiRingCat.hasForgetToMonCat : CategoryTheory.HasForget₂ SemiRingCat MonCat

instance SemiRingCat.hasForgetToAddCommMonCat : CategoryTheory.HasForget₂ SemiRingCat AddCommMonCat

def SemiRingCat.ofHom {R : Type u} {S : Type u} [Semiring R] [Semiring S] (f : R →+* S) : SemiRingCat.of R ⟶ SemiRingCat.of S

Typecheck a RingHom as a morphism in SemiRingCat.

@[simp]

theorem SemiRingCat.ofHom_apply {R : Type u} {S : Type u} [Semiring R] [Semiring S] (f : R →+* S) (x : R) : ↑(SemiRingCat.ofHom f) x = ↑f x

@[simp]

theorem RingEquiv.toSemiRingCatIso_hom {X : Type u_1} {Y : Type u_1} [Semiring X] [Semiring Y] (e : X ≃+* Y) : (RingEquiv.toSemiRingCatIso e).hom = RingEquiv.toRingHom e

@[simp]

theorem RingEquiv.toSemiRingCatIso_inv {X : Type u_1} {Y : Type u_1} [Semiring X] [Semiring Y] (e : X ≃+* Y) : (RingEquiv.toSemiRingCatIso e).inv = RingEquiv.toRingHom (RingEquiv.symm e)

def RingEquiv.toSemiRingCatIso {X : Type u_1} {Y : Type u_1} [Semiring X] [Semiring Y] (e : X ≃+* Y) : SemiRingCat.of X ≅ SemiRingCat.of Y

Ring equivalence are isomorphisms in category of semirings

instance SemiRingCat.forgetReflectIsos : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget SemiRingCat)

def RingCat : Type (u + 1)

The category of rings.

instance RingCat.instParentProjectionTypeSemiringRingToSemiring : CategoryTheory.BundledHom.ParentProjection @Ring.toSemiring

instance RingCat.instConcreteCategoryRingCatInstRingCatLargeCategory : CategoryTheory.ConcreteCategory RingCat

instance RingCat.instCoeSortRingCatType : CoeSort RingCat (Type u_1)

instance RingCat.instRingα (X : RingCat) : Ring ↑X

def RingCat.forget_obj_eq_coe (R : RingCat) : Prop

instance RingCat.instRing (X : RingCat) : Ring ↑X

instance RingCat.instRing' (X : RingCat) : Ring ((CategoryTheory.forget RingCat).obj X)

instance RingCat.instRingHomClass {X : RingCat} {Y : RingCat} : RingHomClass (X ⟶ Y) ↑X ↑Y

theorem RingCat.coe_id {X : RingCat} : ↑(CategoryTheory.CategoryStruct.id X) = id

theorem RingCat.coe_comp {X : RingCat} {Y : RingCat} {Z : RingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : ↑(CategoryTheory.CategoryStruct.comp f g) = ↑g ∘ ↑f

@[simp]

theorem RingCat.forget_map {X : RingCat} {Y : RingCat} (f : X ⟶ Y) : (CategoryTheory.forget RingCat).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] : RingCat

Construct a bundled RingCat from the underlying type and typeclass.

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

Typecheck a RingHom as a morphism in RingCat.

instance RingCat.instInhabitedRingCat : Inhabited RingCat

instance RingCat.instRingα_1 (R : RingCat) : Ring ↑R

@[simp]

theorem RingCat.coe_of (R : Type u) [Ring R] : ↑(RingCat.of 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

instance RingCat.hasForgetToSemiRingCat : CategoryTheory.HasForget₂ RingCat SemiRingCat

instance RingCat.hasForgetToAddCommGroupCat : CategoryTheory.HasForget₂ RingCat AddCommGroupCat

def CommSemiRingCat : Type (u + 1)

The category of commutative semirings.

instance CommSemiRingCat.instParentProjectionTypeSemiringCommSemiringToSemiring : CategoryTheory.BundledHom.ParentProjection @CommSemiring.toSemiring

instance CommSemiRingCat.instConcreteCategoryCommSemiRingCatInstCommSemiRingCatLargeCategory : CategoryTheory.ConcreteCategory CommSemiRingCat

instance CommSemiRingCat.instCoeSortCommSemiRingCatType : CoeSort CommSemiRingCat (Type u_1)

instance CommSemiRingCat.instCommSemiringα (X : CommSemiRingCat) : CommSemiring ↑X

def CommSemiRingCat.forget_obj_eq_coe (R : CommSemiRingCat) : Prop

instance CommSemiRingCat.instCommSemiring (X : CommSemiRingCat) : CommSemiring ↑X

instance CommSemiRingCat.instCommSemiring' (X : CommSemiRingCat) : CommSemiring ((CategoryTheory.forget CommSemiRingCat).obj X)

instance CommSemiRingCat.instRingHomClass {X : CommSemiRingCat} {Y : CommSemiRingCat} : RingHomClass (X ⟶ Y) ↑X ↑Y

theorem CommSemiRingCat.coe_id {X : CommSemiRingCat} : ↑(CategoryTheory.CategoryStruct.id X) = id

theorem CommSemiRingCat.coe_comp {X : CommSemiRingCat} {Y : CommSemiRingCat} {Z : CommSemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : ↑(CategoryTheory.CategoryStruct.comp f g) = ↑g ∘ ↑f

@[simp]

theorem CommSemiRingCat.forget_map {X : CommSemiRingCat} {Y : CommSemiRingCat} (f : X ⟶ Y) : (CategoryTheory.forget CommSemiRingCat).map f = ↑f

theorem CommSemiRingCat.ext {X : CommSemiRingCat} {Y : CommSemiRingCat} {f : X ⟶ Y} {g : X ⟶ Y} (w : ∀ (x : ↑X), ↑f x = ↑g x) : f = g

def CommSemiRingCat.of (R : Type u) [CommSemiring R] : CommSemiRingCat

Construct a bundled CommSemiRingCat from the underlying type and typeclass.

def CommSemiRingCat.ofHom {R : Type u} {S : Type u} [CommSemiring R] [CommSemiring S] (f : R →+* S) : CommSemiRingCat.of R ⟶ CommSemiRingCat.of S

Typecheck a RingHom as a morphism in CommSemiRingCat.

@[simp]

theorem CommSemiRingCat.RingEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) : ↑↑e = ↑e

instance CommSemiRingCat.instInhabitedCommSemiRingCat : Inhabited CommSemiRingCat

instance CommSemiRingCat.instCommSemiringα_1 (R : CommSemiRingCat) : CommSemiring ↑R

@[simp]

theorem CommSemiRingCat.coe_of (R : Type u) [CommSemiring R] : ↑(CommSemiRingCat.of R) = R

instance CommSemiRingCat.hasForgetToSemiRingCat : CategoryTheory.HasForget₂ CommSemiRingCat SemiRingCat

instance CommSemiRingCat.hasForgetToCommMonCat : CategoryTheory.HasForget₂ CommSemiRingCat CommMonCat

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

@[simp]

theorem RingEquiv.toCommSemiRingCatIso_inv {X : Type u_1} {Y : Type u_1} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) : (RingEquiv.toCommSemiRingCatIso e).inv = RingEquiv.toRingHom (RingEquiv.symm e)

@[simp]

theorem RingEquiv.toCommSemiRingCatIso_hom {X : Type u_1} {Y : Type u_1} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) : (RingEquiv.toCommSemiRingCatIso e).hom = RingEquiv.toRingHom e

def RingEquiv.toCommSemiRingCatIso {X : Type u_1} {Y : Type u_1} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) : SemiRingCat.of X ≅ SemiRingCat.of Y

Ring equivalence are isomorphisms in category of commutative semirings

instance CommSemiRingCat.forgetReflectIsos : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget CommSemiRingCat)

def CommRingCat : Type (u + 1)

The category of commutative rings.

instance CommRingCat.instParentProjectionTypeRingCommRingToRing : CategoryTheory.BundledHom.ParentProjection @CommRing.toRing

instance CommRingCat.instConcreteCategoryCommRingCatInstCommRingCatLargeCategory : CategoryTheory.ConcreteCategory CommRingCat

instance CommRingCat.instCoeSortCommRingCatType : CoeSort CommRingCat (Type u_1)

def CommRingCat.forget_obj_eq_coe (R : CommRingCat) : Prop

instance CommRingCat.instCommRing (X : CommRingCat) : CommRing ↑X

instance CommRingCat.instCommRing' (X : CommRingCat) : CommRing ((CategoryTheory.forget CommRingCat).obj X)

instance CommRingCat.instRingHomClass {X : CommRingCat} {Y : CommRingCat} : RingHomClass (X ⟶ Y) ↑X ↑Y

theorem CommRingCat.coe_id {X : CommRingCat} : ↑(CategoryTheory.CategoryStruct.id X) = id

theorem CommRingCat.coe_comp {X : CommRingCat} {Y : CommRingCat} {Z : CommRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : ↑(CategoryTheory.CategoryStruct.comp f g) = ↑g ∘ ↑f

@[simp]

theorem CommRingCat.forget_map {X : CommRingCat} {Y : CommRingCat} (f : X ⟶ Y) : (CategoryTheory.forget CommRingCat).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

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

Construct a bundled CommRingCat from the underlying type and typeclass.

def CommRingCat.ofHom {R : Type u} {S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : CommRingCat.of R ⟶ CommRingCat.of S

Typecheck a RingHom as a morphism in CommRingCat.

@[simp]

theorem CommRingCat.RingEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [CommRing X] [CommRing Y] (e : X ≃+* Y) : ↑↑e = ↑e

instance CommRingCat.instInhabitedCommRingCat : Inhabited CommRingCat

instance CommRingCat.instCommRingα (R : CommRingCat) : CommRing ↑R

@[simp]

theorem CommRingCat.coe_of (R : Type u) [CommRing R] : ↑(CommRingCat.of R) = R

instance CommRingCat.hasForgetToRingCat : CategoryTheory.HasForget₂ CommRingCat RingCat

instance CommRingCat.hasForgetToCommSemiRingCat : CategoryTheory.HasForget₂ CommRingCat CommSemiRingCat

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

instance CommRingCat.instFullCommRingCatInstCommRingCatLargeCategoryCommSemiRingCatInstCommSemiRingCatLargeCategoryForget₂InstConcreteCategoryCommRingCatInstCommRingCatLargeCategoryInstConcreteCategoryCommSemiRingCatInstCommSemiRingCatLargeCategoryHasForgetToCommSemiRingCat : CategoryTheory.Full (CategoryTheory.forget₂ CommRingCat CommSemiRingCat)

@[simp]

theorem RingEquiv.toRingCatIso_inv {X : Type u} {Y : Type u} [Ring X] [Ring Y] (e : X ≃+* Y) : (RingEquiv.toRingCatIso e).inv = RingEquiv.toRingHom (RingEquiv.symm e)

@[simp]

theorem RingEquiv.toRingCatIso_hom {X : Type u} {Y : Type u} [Ring X] [Ring Y] (e : X ≃+* Y) : (RingEquiv.toRingCatIso e).hom = RingEquiv.toRingHom e

def RingEquiv.toRingCatIso {X : Type u} {Y : Type u} [Ring X] [Ring Y] (e : X ≃+* Y) : RingCat.of X ≅ RingCat.of Y

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

@[simp]

theorem RingEquiv.toCommRingCatIso_hom {X : Type u} {Y : Type u} [CommRing X] [CommRing Y] (e : X ≃+* Y) : (RingEquiv.toCommRingCatIso e).hom = RingEquiv.toRingHom e

@[simp]

theorem RingEquiv.toCommRingCatIso_inv {X : Type u} {Y : Type u} [CommRing X] [CommRing Y] (e : X ≃+* Y) : (RingEquiv.toCommRingCatIso e).inv = RingEquiv.toRingHom (RingEquiv.symm e)

def RingEquiv.toCommRingCatIso {X : Type u} {Y : Type u} [CommRing X] [CommRing Y] (e : X ≃+* Y) : CommRingCat.of X ≅ CommRingCat.of Y

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

def CategoryTheory.Iso.ringCatIsoToRingEquiv {X : RingCat} {Y : RingCat} (i : X ≅ Y) : ↑X ≃+* ↑Y

Build a RingEquiv from an isomorphism in the category RingCat.

def CategoryTheory.Iso.commRingCatIsoToRingEquiv {X : CommRingCat} {Y : CommRingCat} (i : X ≅ Y) : ↑X ≃+* ↑Y

Build a RingEquiv from an isomorphism in the category CommRingCat.

@[simp]

theorem CategoryTheory.Iso.commRingIsoToRingEquiv_toRingHom {X : CommRingCat} {Y : CommRingCat} (i : X ≅ Y) : RingEquiv.toRingHom (CategoryTheory.Iso.commRingCatIsoToRingEquiv i) = i.hom

@[simp]

theorem CategoryTheory.Iso.commRingIsoToRingEquiv_symm_toRingHom {X : CommRingCat} {Y : CommRingCat} (i : X ≅ Y) : RingEquiv.toRingHom (RingEquiv.symm (CategoryTheory.Iso.commRingCatIsoToRingEquiv i)) = i.inv

def ringEquivIsoRingIso {X : Type u} {Y : Type u} [Ring X] [Ring Y] : X ≃+* Y ≅ RingCat.of X ≅ RingCat.of Y

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

def ringEquivIsoCommRingIso {X : Type u} {Y : Type u} [CommRing X] [CommRing Y] : X ≃+* Y ≅ CommRingCat.of X ≅ CommRingCat.of Y

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

instance RingCat.forget_reflects_isos : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget RingCat)

instance CommRingCat.forget_reflects_isos : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget CommRingCat)

theorem CommRingCat.comp_eq_ring_hom_comp {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) : CategoryTheory.CategoryStruct.comp f g = RingHom.comp g f

theorem CommRingCat.ringHom_comp_eq_comp {R : Type u_1} {S : Type u_1} {T : Type u_1} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) : RingHom.comp g f = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom f) (CommRingCat.ofHom g)