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 S : SemiRingCat) : Type u

The type of morphisms in SemiRingCat.

• hom' : ↑R →+* ↑S

  The underlying ring hom.

theorem SemiRingCat.Hom.ext {R 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.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory SemiRingCat fun (R S : SemiRingCat) => ↑R →+* ↑S

Equations

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

@[reducible, inline]

abbrev SemiRingCat.Hom.hom {R S : SemiRingCat} (f : R.Hom S) : ↑R →+* ↑S

Turn a morphism in SemiRingCat back into a RingHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[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 = CategoryTheory.ConcreteCategory.ofHom f

def SemiRingCat.Hom.Simps.hom (R S : SemiRingCat) (f : R.Hom S) : ↑R →+* ↑S

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• SemiRingCat.Hom.Simps.hom R S f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem SemiRingCat.ofHom_hom {R S : SemiRingCat} (f : R ⟶ S) : ofHom (Hom.hom f) = 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) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) r = f r

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

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

instance SemiRingCat.instInhabited : Inhabited SemiRingCat

Equations

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

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 = ⇑(CategoryTheory.ConcreteCategory.hom f)

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 := SemiRingCat.ofHom ↑e, inv := SemiRingCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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

structure RingCat : Type (u + 1)

The category of rings.

• 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 S : RingCat) : Type u

The type of morphisms in RingCat.

• hom' : ↑R →+* ↑S

  The underlying ring hom.

theorem RingCat.Hom.ext {R 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.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory RingCat fun (R S : RingCat) => ↑R →+* ↑S

Equations

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

@[reducible, inline]

abbrev RingCat.Hom.hom {R S : RingCat} (f : R.Hom S) : ↑R →+* ↑S

Turn a morphism in RingCat back into a RingHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[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 = CategoryTheory.ConcreteCategory.ofHom f

def RingCat.Hom.Simps.hom (R S : RingCat) (f : R.Hom S) : ↑R →+* ↑S

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• RingCat.Hom.Simps.hom R S f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem RingCat.ofHom_hom {R S : RingCat} (f : R ⟶ S) : ofHom (Hom.hom f) = 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) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) r = f r

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

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

instance RingCat.instInhabited : Inhabited RingCat

Equations

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

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 = ⇑(CategoryTheory.ConcreteCategory.hom f)

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 := RingCat.ofHom ↑e, inv := RingCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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

structure CommSemiRingCat : Type (u + 1)

The category of commutative 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 S : CommSemiRingCat) : Type u

The type of morphisms in CommSemiRingCat.

• hom' : ↑R →+* ↑S

  The underlying ring hom.

theorem CommSemiRingCat.Hom.ext {R 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.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory CommSemiRingCat fun (R S : CommSemiRingCat) => ↑R →+* ↑S

Equations

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

@[reducible, inline]

abbrev CommSemiRingCat.Hom.hom {R S : CommSemiRingCat} (f : R.Hom S) : ↑R →+* ↑S

Turn a morphism in CommSemiRingCat back into a RingHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[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 = CategoryTheory.ConcreteCategory.ofHom f

def CommSemiRingCat.Hom.Simps.hom (R S : CommSemiRingCat) (f : R.Hom S) : ↑R →+* ↑S

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• CommSemiRingCat.Hom.Simps.hom R S f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem CommSemiRingCat.ofHom_hom {R S : CommSemiRingCat} (f : R ⟶ S) : ofHom (Hom.hom f) = 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) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) r = f r

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

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

instance CommSemiRingCat.instInhabited : Inhabited CommSemiRingCat

Equations

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

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 = ⇑(CategoryTheory.ConcreteCategory.hom f)

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 := CommSemiRingCat.ofHom ↑e, inv := CommSemiRingCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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

structure CommRingCat : Type (u + 1)

The category of commutative rings.

• 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 S : CommRingCat) : Type u

The type of morphisms in CommRingCat.

• hom' : ↑R →+* ↑S

  The underlying ring hom.

theorem CommRingCat.Hom.ext {R 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.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory CommRingCat fun (R S : CommRingCat) => ↑R →+* ↑S

Equations

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

@[reducible, inline]

abbrev CommRingCat.Hom.hom {R S : CommRingCat} (f : R.Hom S) : ↑R →+* ↑S

The underlying ring hom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[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 = CategoryTheory.ConcreteCategory.ofHom f

def CommRingCat.Hom.Simps.hom (R S : CommRingCat) (f : R.Hom S) : ↑R →+* ↑S

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• CommRingCat.Hom.Simps.hom R S f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem CommRingCat.ofHom_hom {R S : CommRingCat} (f : R ⟶ S) : ofHom (Hom.hom f) = 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) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) r = f r

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

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

instance CommRingCat.instInhabited : Inhabited CommRingCat

Equations

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

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 = ⇑(CategoryTheory.ConcreteCategory.hom f)

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) : RingCat.Hom.hom ((CategoryTheory.forget₂ CommRingCat RingCat).map f) = Hom.hom f

@[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.

instance CommRingCat.instHasForget₂CommMonCat : CategoryTheory.HasForget₂ CommRingCat CommMonCat

Equations

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

@[simp]

theorem CommRingCat.instHasForget₂CommMonCat_forget₂_map {X✝ Y✝ : CommRingCat} (f : X✝ ⟶ Y✝) : CategoryTheory.HasForget₂.forget₂.map f = CommMonCat.ofHom ↑(Hom.hom f)

@[simp]

theorem CommRingCat.instHasForget₂CommMonCat_forget₂_obj_coe (M : CommRingCat) : ↑(CategoryTheory.HasForget₂.forget₂.obj M) = ↑M

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 := CommRingCat.ofHom ↑e, inv := CommRingCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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 (SemiRingCat.Hom.hom e.hom) (SemiRingCat.Hom.hom e.inv) ⋯ ⋯

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 (RingCat.Hom.hom e.hom) (RingCat.Hom.hom e.inv) ⋯ ⋯

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 (CommSemiRingCat.Hom.hom e.hom) (CommSemiRingCat.Hom.hom e.inv) ⋯ ⋯

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 (CommRingCat.Hom.hom e.hom) (CommRingCat.Hom.hom e.inv) ⋯ ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Iso.commRingCatIsoToRingEquiv_toRingHom {R S : CommRingCat} (e : R ≅ S) : ↑e.commRingCatIsoToRingEquiv = CommRingCat.Hom.hom e.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) : (CategoryTheory.forget RingCat).map f x = (CategoryTheory.ConcreteCategory.hom f) x

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