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.

• of :: (
• carrier : Type u

  The underlying type.

• semiring : Semiring ↑self
• )

def SemiRingCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prevents SemiRingCat.of R being printed as { carrier := R, semiring := ... } by delabStructureInstance.

@[implicit_reducible]

instance SemiRingCat.instCoeSortType : CoeSort SemiRingCat (Type u)

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

theorem SemiRingCat.Hom.ext_iff {R S : SemiRingCat} {x y : R.Hom S} : x = y ↔ x.hom' = y.hom'

@[implicit_reducible]

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

@[implicit_reducible]

instance SemiRingCat.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory SemiRingCat fun (R S : SemiRingCat) => ↑R →+* ↑S

@[reducible, inline]

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

Turn a morphism in SemiRingCat back into a RingHom.

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

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

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

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

theorem SemiRingCat.hom_ext_iff {R S : SemiRingCat} {f g : R ⟶ S} : f = g ↔ Hom.hom f = Hom.hom 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

@[implicit_reducible]

instance SemiRingCat.instInhabited : Inhabited SemiRingCat

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'.

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)

@[implicit_reducible]

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

@[implicit_reducible]

instance SemiRingCat.hasForgetToMonCat : CategoryTheory.HasForget₂ SemiRingCat MonCat

@[implicit_reducible]

instance SemiRingCat.hasForgetToAddCommMonCat : CategoryTheory.HasForget₂ SemiRingCat AddCommMonCat

@[simp]

theorem SemiRingCat.forget₂_monCat_map {R S : SemiRingCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ SemiRingCat MonCat).obj R)) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ SemiRingCat MonCat).map f)) x = (CategoryTheory.ConcreteCategory.hom f) x

@[simp]

theorem SemiRingCat.forget₂_addCommMonCat_map {R S : SemiRingCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ SemiRingCat AddCommMonCat).obj R)) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ SemiRingCat AddCommMonCat).map f)) x = (CategoryTheory.ConcreteCategory.hom f) x

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

Ring equivalences are isomorphisms in category of semirings

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

• of :: (
• carrier : Type u

  The underlying type.

• ring : Ring ↑self
• )

def RingCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prevents RingCat.of R being printed as { carrier := R, ring := ... } by delabStructureInstance.

@[implicit_reducible]

instance RingCat.instCoeSortType : CoeSort RingCat (Type u)

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_iff {R S : RingCat} {x y : R.Hom S} : x = y ↔ x.hom' = y.hom'

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

@[implicit_reducible]

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

@[implicit_reducible]

instance RingCat.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory RingCat fun (R S : RingCat) => ↑R →+* ↑S

@[reducible, inline]

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

Turn a morphism in RingCat back into a RingHom.

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

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

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

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

theorem RingCat.hom_ext_iff {R S : RingCat} {f g : R ⟶ S} : f = g ↔ Hom.hom f = Hom.hom 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

@[implicit_reducible]

instance RingCat.instInhabited : Inhabited RingCat

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.

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)

@[implicit_reducible]

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

@[implicit_reducible]

instance RingCat.hasForgetToSemiRingCat : CategoryTheory.HasForget₂ RingCat SemiRingCat

@[simp]

theorem RingCat.forget₂_map {R S : RingCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ RingCat SemiRingCat).obj R)) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ RingCat SemiRingCat).map f)) x = (CategoryTheory.ConcreteCategory.hom f) x

def RingCat.fullyFaithfulForget₂ToSemiRingCat : (CategoryTheory.forget₂ RingCat SemiRingCat).FullyFaithful

The forgetful functor from RingCat to SemiRingCat is fully faithful.

instance RingCat.instFullSemiRingCatForget₂RingHomCarrierCarrier : (CategoryTheory.forget₂ RingCat SemiRingCat).Full

@[implicit_reducible]

instance RingCat.hasForgetToAddCommGrp : CategoryTheory.HasForget₂ RingCat AddCommGrpCat

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

Ring equivalences are isomorphisms in category of rings

@[simp]

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

@[simp]

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

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

structure CommSemiRingCat : Type (u + 1)

The category of commutative semirings.

• of :: (
• carrier : Type u

  The underlying type.

• commSemiring : CommSemiring ↑self
• )

def CommSemiRingCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prevents CommSemiRingCat.of R being printed as { carrier := R, commSemiring := ... } by delabStructureInstance.

@[implicit_reducible]

instance CommSemiRingCat.instCoeSortType : CoeSort CommSemiRingCat (Type u)

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

theorem CommSemiRingCat.Hom.ext_iff {R S : CommSemiRingCat} {x y : R.Hom S} : x = y ↔ x.hom' = y.hom'

@[implicit_reducible]

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

@[implicit_reducible]

instance CommSemiRingCat.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory CommSemiRingCat fun (R S : CommSemiRingCat) => ↑R →+* ↑S

@[reducible, inline]

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

Turn a morphism in CommSemiRingCat back into a RingHom.

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

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

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

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

theorem CommSemiRingCat.hom_ext_iff {R S : CommSemiRingCat} {f g : R ⟶ S} : f = g ↔ Hom.hom f = Hom.hom 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

@[implicit_reducible]

instance CommSemiRingCat.instInhabited : Inhabited CommSemiRingCat

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'.

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)

@[implicit_reducible]

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

@[implicit_reducible]

instance CommSemiRingCat.hasForgetToSemiRingCat : CategoryTheory.HasForget₂ CommSemiRingCat SemiRingCat

def CommSemiRingCat.fullyFaithfulForget₂ToSemiRingCat : (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat).FullyFaithful

The forgetful functor from CommSemiRingCat to SemiRingCat is fully faithful.

instance CommSemiRingCat.instFullSemiRingCatForget₂RingHomCarrierCarrier : (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat).Full

@[implicit_reducible]

instance CommSemiRingCat.hasForgetToCommMonCat : CategoryTheory.HasForget₂ CommSemiRingCat CommMonCat

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

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

Ring equivalences are isomorphisms in category of commutative semirings

@[simp]

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

@[simp]

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

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

structure CommRingCat : Type (u + 1)

The category of commutative rings.

• of :: (
• carrier : Type u

  The underlying type.

• commRing : CommRing ↑self
• )

def CommRingCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prevents CommRingCat.of R being printed as { carrier := R, commRing := ... } by delabStructureInstance.

@[implicit_reducible]

instance CommRingCat.instCoeSortType : CoeSort CommRingCat (Type u)

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

theorem CommRingCat.Hom.ext_iff {R S : CommRingCat} {x y : R.Hom S} : x = y ↔ x.hom' = y.hom'

@[implicit_reducible]

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

@[implicit_reducible]

instance CommRingCat.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory CommRingCat fun (R S : CommRingCat) => ↑R →+* ↑S

@[reducible, inline]

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

The underlying ring hom.

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

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

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

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

theorem CommRingCat.hom_ext_iff {R S : CommRingCat} {f g : R ⟶ S} : f = g ↔ Hom.hom f = Hom.hom 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

@[implicit_reducible]

instance CommRingCat.instInhabited : Inhabited CommRingCat

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.

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

@[implicit_reducible]

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

@[implicit_reducible]

instance CommRingCat.hasForgetToRingCat : CategoryTheory.HasForget₂ CommRingCat RingCat

def CommRingCat.fullyFaithfulForget₂ToRingCat : (CategoryTheory.forget₂ CommRingCat RingCat).FullyFaithful

The forgetful functor from CommRingCat to RingCat is fully faithful.

instance CommRingCat.instFullRingCatForget₂RingHomCarrierCarrier : (CategoryTheory.forget₂ CommRingCat RingCat).Full

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

@[implicit_reducible]

instance CommRingCat.hasForgetToAddCommMonCat : CategoryTheory.HasForget₂ CommRingCat CommSemiRingCat

@[implicit_reducible]

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

@[simp]

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

@[simp]

theorem CommRingCat.commMon_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 equivalences are isomorphisms in category of commutative rings

@[simp]

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

@[simp]

theorem RingEquiv.toCommRingCatIso_inv {R S : Type u} [CommRing R] [CommRing S] (e : R ≃+* S) : e.toCommRingCatIso.inv = CommRingCat.ofHom ↑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.

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

Build a RingEquiv from an isomorphism in the category RingCat.

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

Build a RingEquiv from an isomorphism in the category CommSemiRingCat.

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

Build a RingEquiv from an isomorphism in the category CommRingCat.

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

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