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.

structure SemiRingCat : Type (u + 1)

The category of semirings.

• carrier : Type u

  The underlying type.

• semiring : Semiring ↑self

instance SemiRingCat.instCoeSortType : CoeSort SemiRingCat (Type u)

Equations

• SemiRingCat.instCoeSortType = { coe := SemiRingCat.carrier }

@[reducible, inline]

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

The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses. This is the preferred way to construct a term of SemiRingCat.

Equations

• SemiRingCat.of R = SemiRingCat.mk✝ R

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

theorem SemiRingCat.of_carrier (R : SemiRingCat) : of ↑R = R

structure SemiRingCat.Hom (R : SemiRingCat) (S : SemiRingCat) : Type (max u_1 u_2)

The type of morphisms in SemiRingCat.

• hom : ↑R →+* ↑S

  The underlying ring hom.

theorem SemiRingCat.Hom.ext {R : SemiRingCat} {S : SemiRingCat} {x y : R.Hom S} (hom : x.hom = y.hom) : x = y

instance SemiRingCat.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} SemiRingCat

Equations

• SemiRingCat.instCategory = CategoryTheory.Category.mk @SemiRingCat.instCategory.proof_1 @SemiRingCat.instCategory.proof_2 @SemiRingCat.instCategory.proof_3

instance SemiRingCat.instCoeFunHomForallCarrier {R S : SemiRingCat} : CoeFun (R ⟶ S) fun (x : R ⟶ S) => ↑R → ↑S

Equations

• SemiRingCat.instCoeFunHomForallCarrier = { coe := fun (f : R ⟶ S) => ⇑f.hom }

@[simp]

theorem SemiRingCat.hom_id {R : SemiRingCat} : (CategoryTheory.CategoryStruct.id R).hom = RingHom.id ↑R

theorem SemiRingCat.id_apply (R : SemiRingCat) (r : ↑R) : (CategoryTheory.CategoryStruct.id R).hom r = r

@[simp]

theorem SemiRingCat.hom_comp {R S T : SemiRingCat} (f : R ⟶ S) (g : S ⟶ T) : (CategoryTheory.CategoryStruct.comp f g).hom = g.hom.comp f.hom

theorem SemiRingCat.comp_apply {R S T : SemiRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : ↑R) : (CategoryTheory.CategoryStruct.comp f g).hom r = g.hom (f.hom r)

theorem SemiRingCat.hom_ext {R S : SemiRingCat} {f g : R ⟶ S} (hf : f.hom = g.hom) : f = g

@[reducible, inline]

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

Typecheck a RingHom as a morphism in SemiRingCat.

Equations

• SemiRingCat.ofHom f = { hom := f }

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

@[simp]

theorem SemiRingCat.ofHom_hom {R S : SemiRingCat} (f : R ⟶ S) : ofHom f.hom = f

@[simp]

theorem SemiRingCat.ofHom_id {R : Type u} [Semiring R] : ofHom (RingHom.id R) = CategoryTheory.CategoryStruct.id (of R)

@[simp]

theorem SemiRingCat.ofHom_comp {R S T : Type u} [Semiring R] [Semiring S] [Semiring T] (f : R →+* S) (g : S →+* T) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

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

@[simp]

theorem SemiRingCat.inv_hom_apply {R S : SemiRingCat} (e : R ≅ S) (r : ↑R) : e.inv.hom (e.hom.hom r) = r

@[simp]

theorem SemiRingCat.hom_inv_apply {R S : SemiRingCat} (e : R ≅ S) (s : ↑S) : e.hom.hom (e.inv.hom s) = s

instance SemiRingCat.instInhabited : Inhabited SemiRingCat

Equations

• SemiRingCat.instInhabited = { default := SemiRingCat.of PUnit.{?u.3 + 1} }

instance SemiRingCat.instHasForget : CategoryTheory.HasForget SemiRingCat

Equations

• One or more equations did not get rendered due to their size.

def SemiRingCat.forget_obj_eq_coe (R R' : SemiRingCat) : Prop

This unification hint helps with problems of the form (forget ?C).obj R =?= carrier R'.

Equations

• R.forget_obj_eq_coe R' = (R = R' → (CategoryTheory.forget SemiRingCat).obj R = ↑R')

theorem SemiRingCat.forget_obj {R : SemiRingCat} : (CategoryTheory.forget SemiRingCat).obj R = ↑R

theorem SemiRingCat.forget_map {R S : SemiRingCat} (f : R ⟶ S) : (CategoryTheory.forget SemiRingCat).map f = ⇑f.hom

instance SemiRingCat.instSemiringObjForget {R : SemiRingCat} : Semiring ((CategoryTheory.forget SemiRingCat).obj R)

Equations

• SemiRingCat.instSemiringObjForget = inferInstance

instance SemiRingCat.hasForgetToMonCat : CategoryTheory.HasForget₂ SemiRingCat MonCat

Equations

• One or more equations did not get rendered due to their size.

instance SemiRingCat.hasForgetToAddCommMonCat : CategoryTheory.HasForget₂ SemiRingCat AddCommMonCat

Equations

• One or more equations did not get rendered due to their size.

def RingEquiv.toSemiRingCatIso {R S : Type u} [Semiring R] [Semiring S] (e : R ≃+* S) : SemiRingCat.of R ≅ SemiRingCat.of S

Ring equivalence are isomorphisms in category of semirings

Equations

• e.toSemiRingCatIso = { hom := { hom := ↑e }, inv := { hom := ↑e.symm }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem RingEquiv.toSemiRingCatIso_inv_hom {R S : Type u} [Semiring R] [Semiring S] (e : R ≃+* S) : e.toSemiRingCatIso.inv.hom = ↑e.symm

@[simp]

theorem RingEquiv.toSemiRingCatIso_hom_hom {R S : Type u} [Semiring R] [Semiring S] (e : R ≃+* S) : e.toSemiRingCatIso.hom.hom = ↑e

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

structure RingCat : Type (u + 1)

The category of semirings.

• carrier : Type u

  The underlying type.

• ring : Ring ↑self

instance RingCat.instCoeSortType : CoeSort RingCat (Type u)

Equations

• RingCat.instCoeSortType = { coe := RingCat.carrier }

@[reducible, inline]

abbrev RingCat.of (R : Type u) [Ring R] : RingCat

The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses. This is the preferred way to construct a term of RingCat.

Equations

• RingCat.of R = RingCat.mk✝ R

theorem RingCat.coe_of (R : Type u) [Ring R] : ↑(of R) = R

theorem RingCat.of_carrier (R : RingCat) : of ↑R = R

structure RingCat.Hom (R : RingCat) (S : RingCat) : Type (max u_1 u_2)

The type of morphisms in RingCat.

• hom : ↑R →+* ↑S

  The underlying ring hom.

theorem RingCat.Hom.ext {R : RingCat} {S : RingCat} {x y : R.Hom S} (hom : x.hom = y.hom) : x = y

instance RingCat.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} RingCat

Equations

• RingCat.instCategory = CategoryTheory.Category.mk @RingCat.instCategory.proof_1 @RingCat.instCategory.proof_2 @RingCat.instCategory.proof_3

instance RingCat.instCoeFunHomForallCarrier {R S : RingCat} : CoeFun (R ⟶ S) fun (x : R ⟶ S) => ↑R → ↑S

Equations

• RingCat.instCoeFunHomForallCarrier = { coe := fun (f : R ⟶ S) => ⇑f.hom }

@[simp]

theorem RingCat.hom_id {R : RingCat} : (CategoryTheory.CategoryStruct.id R).hom = RingHom.id ↑R

theorem RingCat.id_apply (R : RingCat) (r : ↑R) : (CategoryTheory.CategoryStruct.id R).hom r = r

@[simp]

theorem RingCat.hom_comp {R S T : RingCat} (f : R ⟶ S) (g : S ⟶ T) : (CategoryTheory.CategoryStruct.comp f g).hom = g.hom.comp f.hom

theorem RingCat.comp_apply {R S T : RingCat} (f : R ⟶ S) (g : S ⟶ T) (r : ↑R) : (CategoryTheory.CategoryStruct.comp f g).hom r = g.hom (f.hom r)

theorem RingCat.hom_ext {R S : RingCat} {f g : R ⟶ S} (hf : f.hom = g.hom) : f = g

@[reducible, inline]

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

Typecheck a RingHom as a morphism in RingCat.

Equations

• RingCat.ofHom f = { hom := f }

theorem RingCat.hom_ofHom {R S : Type u} [Ring R] [Ring S] (f : R →+* S) : (ofHom f).hom = f

@[simp]

theorem RingCat.ofHom_hom {R S : RingCat} (f : R ⟶ S) : ofHom f.hom = f

@[simp]

theorem RingCat.ofHom_id {R : Type u} [Ring R] : ofHom (RingHom.id R) = CategoryTheory.CategoryStruct.id (of R)

@[simp]

theorem RingCat.ofHom_comp {R S T : Type u} [Ring R] [Ring S] [Ring T] (f : R →+* S) (g : S →+* T) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem RingCat.ofHom_apply {R S : Type u} [Ring R] [Ring S] (f : R →+* S) (r : R) : (ofHom f).hom r = f r

@[simp]

theorem RingCat.inv_hom_apply {R S : RingCat} (e : R ≅ S) (r : ↑R) : e.inv.hom (e.hom.hom r) = r

@[simp]

theorem RingCat.hom_inv_apply {R S : RingCat} (e : R ≅ S) (s : ↑S) : e.hom.hom (e.inv.hom s) = s

instance RingCat.instInhabited : Inhabited RingCat

Equations

• RingCat.instInhabited = { default := RingCat.of PUnit.{?u.3 + 1} }

instance RingCat.instHasForget : CategoryTheory.HasForget RingCat

Equations

• One or more equations did not get rendered due to their size.

def RingCat.forget_obj_eq_coe (R R' : RingCat) : Prop

This unification hint helps with problems of the form (forget ?C).obj R =?= carrier R'.

An example where this is needed is in applying PresheafOfModules.Sheafify.app_eq_of_isLocallyInjective.

Equations

• R.forget_obj_eq_coe R' = (R = R' → (CategoryTheory.forget RingCat).obj R = ↑R')

theorem RingCat.forget_obj {R : RingCat} : (CategoryTheory.forget RingCat).obj R = ↑R

theorem RingCat.forget_map {R S : RingCat} (f : R ⟶ S) : (CategoryTheory.forget RingCat).map f = ⇑f.hom

instance RingCat.instRingObjForget {R : RingCat} : Ring ((CategoryTheory.forget RingCat).obj R)

Equations

• RingCat.instRingObjForget = inferInstance

instance RingCat.hasForgetToSemiRingCat : CategoryTheory.HasForget₂ RingCat SemiRingCat

Equations

• One or more equations did not get rendered due to their size.

instance RingCat.hasForgetToAddCommGrp : CategoryTheory.HasForget₂ RingCat AddCommGrp

Equations

• One or more equations did not get rendered due to their size.

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

Ring equivalence are isomorphisms in category of semirings

Equations

• e.toRingCatIso = { hom := { hom := ↑e }, inv := { hom := ↑e.symm }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem RingEquiv.toRingCatIso_hom_hom {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : e.toRingCatIso.hom.hom = ↑e

@[simp]

theorem RingEquiv.toRingCatIso_inv_hom {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : e.toRingCatIso.inv.hom = ↑e.symm

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

structure CommSemiRingCat : Type (u + 1)

The category of semirings.

• carrier : Type u

  The underlying type.

• commSemiring : CommSemiring ↑self

instance CommSemiRingCat.instCoeSortType : CoeSort CommSemiRingCat (Type u)

Equations

• CommSemiRingCat.instCoeSortType = { coe := CommSemiRingCat.carrier }

@[reducible, inline]

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

The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses. This is the preferred way to construct a term of CommSemiRingCat.

Equations

• CommSemiRingCat.of R = CommSemiRingCat.mk✝ R

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

theorem CommSemiRingCat.of_carrier (R : CommSemiRingCat) : of ↑R = R

structure CommSemiRingCat.Hom (R : CommSemiRingCat) (S : CommSemiRingCat) : Type (max u_1 u_2)

The type of morphisms in CommSemiRingCat.

• hom : ↑R →+* ↑S

  The underlying ring hom.

theorem CommSemiRingCat.Hom.ext {R : CommSemiRingCat} {S : CommSemiRingCat} {x y : R.Hom S} (hom : x.hom = y.hom) : x = y

instance CommSemiRingCat.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} CommSemiRingCat

Equations

• CommSemiRingCat.instCategory = CategoryTheory.Category.mk @CommSemiRingCat.instCategory.proof_1 @CommSemiRingCat.instCategory.proof_2 @CommSemiRingCat.instCategory.proof_3

instance CommSemiRingCat.instCoeFunHomForallCarrier {R S : CommSemiRingCat} : CoeFun (R ⟶ S) fun (x : R ⟶ S) => ↑R → ↑S

Equations

• CommSemiRingCat.instCoeFunHomForallCarrier = { coe := fun (f : R ⟶ S) => ⇑f.hom }

@[simp]

theorem CommSemiRingCat.hom_id {R : CommSemiRingCat} : (CategoryTheory.CategoryStruct.id R).hom = RingHom.id ↑R

theorem CommSemiRingCat.id_apply (R : CommSemiRingCat) (r : ↑R) : (CategoryTheory.CategoryStruct.id R).hom r = r

@[simp]

theorem CommSemiRingCat.hom_comp {R S T : CommSemiRingCat} (f : R ⟶ S) (g : S ⟶ T) : (CategoryTheory.CategoryStruct.comp f g).hom = g.hom.comp f.hom

theorem CommSemiRingCat.comp_apply {R S T : CommSemiRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : ↑R) : (CategoryTheory.CategoryStruct.comp f g).hom r = g.hom (f.hom r)

theorem CommSemiRingCat.hom_ext {R S : CommSemiRingCat} {f g : R ⟶ S} (hf : f.hom = g.hom) : f = g

@[reducible, inline]

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

Typecheck a RingHom as a morphism in CommSemiRingCat.

Equations

• CommSemiRingCat.ofHom f = { hom := f }

theorem CommSemiRingCat.hom_ofHom {R S : Type u} [CommSemiring R] [CommSemiring S] (f : R →+* S) : (ofHom f).hom = f

@[simp]

theorem CommSemiRingCat.ofHom_hom {R S : CommSemiRingCat} (f : R ⟶ S) : ofHom f.hom = f

@[simp]

theorem CommSemiRingCat.ofHom_id {R : Type u} [CommSemiring R] : ofHom (RingHom.id R) = CategoryTheory.CategoryStruct.id (of R)

@[simp]

theorem CommSemiRingCat.ofHom_comp {R S T : Type u} [CommSemiring R] [CommSemiring S] [CommSemiring T] (f : R →+* S) (g : S →+* T) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem CommSemiRingCat.ofHom_apply {R S : Type u} [CommSemiring R] [CommSemiring S] (f : R →+* S) (r : R) : (ofHom f).hom r = f r

@[simp]

theorem CommSemiRingCat.inv_hom_apply {R S : CommSemiRingCat} (e : R ≅ S) (r : ↑R) : e.inv.hom (e.hom.hom r) = r

@[simp]

theorem CommSemiRingCat.hom_inv_apply {R S : CommSemiRingCat} (e : R ≅ S) (s : ↑S) : e.hom.hom (e.inv.hom s) = s

instance CommSemiRingCat.instInhabited : Inhabited CommSemiRingCat

Equations

• CommSemiRingCat.instInhabited = { default := CommSemiRingCat.of PUnit.{?u.3 + 1} }

instance CommSemiRingCat.instHasForget : CategoryTheory.HasForget CommSemiRingCat

Equations

• One or more equations did not get rendered due to their size.

def CommSemiRingCat.forget_obj_eq_coe (R R' : CommSemiRingCat) : Prop

This unification hint helps with problems of the form (forget ?C).obj R =?= carrier R'.

Equations

• R.forget_obj_eq_coe R' = (R = R' → (CategoryTheory.forget CommSemiRingCat).obj R = ↑R')

theorem CommSemiRingCat.forget_obj {R : CommSemiRingCat} : (CategoryTheory.forget CommSemiRingCat).obj R = ↑R

theorem CommSemiRingCat.forget_map {R S : CommSemiRingCat} (f : R ⟶ S) : (CategoryTheory.forget CommSemiRingCat).map f = ⇑f.hom

instance CommSemiRingCat.instCommSemiringObjForget {R : CommSemiRingCat} : CommSemiring ((CategoryTheory.forget CommSemiRingCat).obj R)

Equations

• CommSemiRingCat.instCommSemiringObjForget = inferInstance

instance CommSemiRingCat.hasForgetToSemiRingCat : CategoryTheory.HasForget₂ CommSemiRingCat SemiRingCat

Equations

• One or more equations did not get rendered due to their size.

instance CommSemiRingCat.hasForgetToCommMonCat : CategoryTheory.HasForget₂ CommSemiRingCat CommMonCat

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

Equations

• One or more equations did not get rendered due to their size.

def RingEquiv.toCommSemiRingCatIso {R S : Type u} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) : CommSemiRingCat.of R ≅ CommSemiRingCat.of S

Ring equivalence are isomorphisms in category of semirings

Equations

• e.toCommSemiRingCatIso = { hom := { hom := ↑e }, inv := { hom := ↑e.symm }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem RingEquiv.toCommSemiRingCatIso_hom_hom {R S : Type u} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) : e.toCommSemiRingCatIso.hom.hom = ↑e

@[simp]

theorem RingEquiv.toCommSemiRingCatIso_inv_hom {R S : Type u} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) : e.toCommSemiRingCatIso.inv.hom = ↑e.symm

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

structure CommRingCat : Type (u + 1)

The category of semirings.

• carrier : Type u

  The underlying type.

• commRing : CommRing ↑self

instance CommRingCat.instCoeSortType : CoeSort CommRingCat (Type u)

Equations

• CommRingCat.instCoeSortType = { coe := CommRingCat.carrier }

@[reducible, inline]

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

The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses. This is the preferred way to construct a term of CommRingCat.

Equations

• CommRingCat.of R = CommRingCat.mk✝ R

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

theorem CommRingCat.of_carrier (R : CommRingCat) : of ↑R = R

structure CommRingCat.Hom (R : CommRingCat) (S : CommRingCat) : Type (max u_1 u_2)

The type of morphisms in CommRingCat.

• hom : ↑R →+* ↑S

  The underlying ring hom.

theorem CommRingCat.Hom.ext {R : CommRingCat} {S : CommRingCat} {x y : R.Hom S} (hom : x.hom = y.hom) : x = y

instance CommRingCat.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} CommRingCat

Equations

• CommRingCat.instCategory = CategoryTheory.Category.mk @CommRingCat.instCategory.proof_1 @CommRingCat.instCategory.proof_2 @CommRingCat.instCategory.proof_3

instance CommRingCat.instCoeFunHomForallCarrier {R S : CommRingCat} : CoeFun (R ⟶ S) fun (x : R ⟶ S) => ↑R → ↑S

Equations

• CommRingCat.instCoeFunHomForallCarrier = { coe := fun (f : R ⟶ S) => ⇑f.hom }

@[simp]

theorem CommRingCat.hom_id {R : CommRingCat} : (CategoryTheory.CategoryStruct.id R).hom = RingHom.id ↑R

theorem CommRingCat.id_apply (R : CommRingCat) (r : ↑R) : (CategoryTheory.CategoryStruct.id R).hom r = r

@[simp]

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

theorem CommRingCat.comp_apply {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : ↑R) : (CategoryTheory.CategoryStruct.comp f g).hom r = g.hom (f.hom r)

theorem CommRingCat.hom_ext {R S : CommRingCat} {f g : R ⟶ S} (hf : f.hom = g.hom) : f = g

@[reducible, inline]

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

Typecheck a RingHom as a morphism in CommRingCat.

Equations

• CommRingCat.ofHom f = { hom := f }

theorem CommRingCat.hom_ofHom {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : (ofHom f).hom = f

@[simp]

theorem CommRingCat.ofHom_hom {R S : CommRingCat} (f : R ⟶ S) : ofHom f.hom = f

@[simp]

theorem CommRingCat.ofHom_id {R : Type u} [CommRing R] : ofHom (RingHom.id R) = CategoryTheory.CategoryStruct.id (of R)

@[simp]

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

theorem CommRingCat.ofHom_apply {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (r : R) : (ofHom f).hom r = f r

@[simp]

theorem CommRingCat.inv_hom_apply {R S : CommRingCat} (e : R ≅ S) (r : ↑R) : e.inv.hom (e.hom.hom r) = r

@[simp]

theorem CommRingCat.hom_inv_apply {R S : CommRingCat} (e : R ≅ S) (s : ↑S) : e.hom.hom (e.inv.hom s) = s

instance CommRingCat.instInhabited : Inhabited CommRingCat

Equations

• CommRingCat.instInhabited = { default := CommRingCat.of PUnit.{?u.3 + 1} }

instance CommRingCat.instHasForget : CategoryTheory.HasForget CommRingCat

Equations

• One or more equations did not get rendered due to their size.

theorem CommRingCat.forget_obj {R : CommRingCat} : (CategoryTheory.forget CommRingCat).obj R = ↑R

def CommRingCat.forget_obj_eq_coe (R R' : CommRingCat) : Prop

This unification hint helps with problems of the form (forget ?C).obj R =?= carrier R'.

An example where this is needed is in applying TopCat.Presheaf.restrictOpen to commutative rings.

Equations

• R.forget_obj_eq_coe R' = (R = R' → (CategoryTheory.forget CommRingCat).obj R = ↑R')

theorem CommRingCat.forget_map {R S : CommRingCat} (f : R ⟶ S) : (CategoryTheory.forget CommRingCat).map f = ⇑f.hom

instance CommRingCat.instCommRingObjForget {R : CommRingCat} : CommRing ((CategoryTheory.forget CommRingCat).obj R)

Equations

• CommRingCat.instCommRingObjForget = inferInstance

instance CommRingCat.hasForgetToRingCat : CategoryTheory.HasForget₂ CommRingCat RingCat

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommRingCat.forgetToRingCat_map_hom {R S : CommRingCat} (f : R ⟶ S) : ((CategoryTheory.forget₂ CommRingCat RingCat).map f).hom = f.hom

@[simp]

theorem CommRingCat.forgetToRingCat_obj {R : CommRingCat} : ↑((CategoryTheory.forget₂ CommRingCat RingCat).obj R) = ↑R

instance CommRingCat.hasForgetToAddCommMonCat : CategoryTheory.HasForget₂ CommRingCat CommSemiRingCat

Equations

• One or more equations did not get rendered due to their size.

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

Ring equivalence are isomorphisms in category of semirings

Equations

• e.toCommRingCatIso = { hom := { hom := ↑e }, inv := { hom := ↑e.symm }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem RingEquiv.toCommRingCatIso_hom_hom {R S : Type u} [CommRing R] [CommRing S] (e : R ≃+* S) : e.toCommRingCatIso.hom.hom = ↑e

@[simp]

theorem RingEquiv.toCommRingCatIso_inv_hom {R S : Type u} [CommRing R] [CommRing S] (e : R ≃+* S) : e.toCommRingCatIso.inv.hom = ↑e.symm

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

def CategoryTheory.Iso.semiRingCatIsoToRingEquiv {R S : SemiRingCat} (e : R ≅ S) : ↑R ≃+* ↑S

Build a RingEquiv from an isomorphism in the category SemiRingCat.

Equations

• e.semiRingCatIsoToRingEquiv = RingEquiv.ofHomInv e.hom.hom e.inv.hom ⋯ ⋯

def CategoryTheory.Iso.ringCatIsoToRingEquiv {R S : RingCat} (e : R ≅ S) : ↑R ≃+* ↑S

Build a RingEquiv from an isomorphism in the category RingCat.

Equations

• e.ringCatIsoToRingEquiv = RingEquiv.ofHomInv e.hom.hom e.inv.hom ⋯ ⋯

def CategoryTheory.Iso.commSemiRingCatIsoToRingEquiv {R S : CommSemiRingCat} (e : R ≅ S) : ↑R ≃+* ↑S

Build a RingEquiv from an isomorphism in the category CommSemiRingCat.

Equations

• e.commSemiRingCatIsoToRingEquiv = RingEquiv.ofHomInv e.hom.hom e.inv.hom ⋯ ⋯

def CategoryTheory.Iso.commRingCatIsoToRingEquiv {R S : CommRingCat} (e : R ≅ S) : ↑R ≃+* ↑S

Build a RingEquiv from an isomorphism in the category CommRingCat.

Equations

• e.commRingCatIsoToRingEquiv = RingEquiv.ofHomInv e.hom.hom e.inv.hom ⋯ ⋯

@[simp]

theorem CategoryTheory.Iso.semiRingCatIsoToRingEquiv_toRingHom {R S : SemiRingCat} (e : R ≅ S) : ↑e.semiRingCatIsoToRingEquiv = e.hom.hom

@[simp]

theorem CategoryTheory.Iso.ringCatIsoToRingEquiv_toRingHom {R S : RingCat} (e : R ≅ S) : ↑e.ringCatIsoToRingEquiv = e.hom.hom

@[simp]

theorem CategoryTheory.Iso.commSemiRingCatIsoToRingEquiv_toRingHom {R S : CommSemiRingCat} (e : R ≅ S) : ↑e.commSemiRingCatIsoToRingEquiv = e.hom.hom

@[simp]

theorem CategoryTheory.Iso.commRingCatIsoToRingEquiv_toRingHom {R S : CommRingCat} (e : R ≅ S) : ↑e.commRingCatIsoToRingEquiv = e.hom.hom

@[reducible, inline]

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

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

Equations

• SemiRingCatMax = SemiRingCat

@[reducible, inline]

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

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

Equations

• RingCatMax = RingCat

@[reducible, inline]

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

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

Equations

• CommSemiRingCatMax = CommSemiRingCat

@[reducible, inline]

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

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

Equations

• CommRingCatMax = CommRingCat

theorem RingCat.forget_map_apply {R S : RingCat} (f : R ⟶ S) (x : (CategoryTheory.forget RingCat).obj R) : f x = f.hom x

theorem CommRingCat.forget_map_apply {R S : CommRingCat} (f : R ⟶ S) (x : (CategoryTheory.forget CommRingCat).obj R) : f x = f.hom x