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.

@[reducible, inline]

abbrev SemiRingCat : Type (u + 1)

The category of semirings.

Equations

• SemiRingCat = CategoryTheory.Bundled Semiring

@[reducible, inline]

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

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

Equations

• SemiRingCatMax = SemiRingCat

@[reducible, inline]

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.

Equations

• SemiRingCat.AssocRingHom M N = (M →+* N)

instance SemiRingCat.bundledHom : CategoryTheory.BundledHom SemiRingCat.AssocRingHom

Equations

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

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

Equations

• X.instSemiring = X.str

instance SemiRingCat.instFunLike {X : SemiRingCat} {Y : SemiRingCat} : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• SemiRingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike

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

Equations

• ⋯ = ⋯

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.

Equations

• SemiRingCat.of R = CategoryTheory.Bundled.of R

@[simp]

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

@[simp]

theorem SemiRingCat.coe_ringHom_id {X : SemiRingCat} : ⇑(CategoryTheory.CategoryStruct.id X) = id

@[simp]

theorem SemiRingCat.coe_id_of {X : Type u} [Semiring X] : ⇑(CategoryTheory.CategoryStruct.id (SemiRingCat.of X)) = ⇑(RingHom.id X)

@[simp]

theorem SemiRingCat.coe_comp_of {X : Type u} {Y : Type u} {Z : Type u} [Semiring X] [Semiring Y] [Semiring Z] (f : X →+* Y) (g : Y →+* Z) : ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑(g.comp f)

theorem SemiRingCat.ext_of_iff {X : Type u} {Y : Type u} [Semiring X] [Semiring Y] {f : X →+* Y} {g : X →+* Y} : f = g ↔ ∀ (x : X), f x = g x

theorem SemiRingCat.ext_of {X : Type u} {Y : Type u} [Semiring X] [Semiring Y] (f : X →+* Y) (g : X →+* Y) (h : ∀ (x : X), f x = g x) : f = g

@[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.instInhabited : Inhabited SemiRingCat

Equations

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

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

Equations

• SemiRingCat.ofHom f = f

@[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 SemiRingCat.ofHom_apply' {R : Type u} {S : Type u} [Semiring R] [Semiring S] (f : R →+* S) (x : R) : (SemiRingCat.ofHom f) x = f x

A variant of ofHom_apply that makes simpNF happy

@[simp]

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

@[simp]

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

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

Ring equivalence are isomorphisms in category of semirings

Equations

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

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

Equations

• SemiRingCat.forgetReflectIsos = ⋯

@[reducible, inline]

abbrev RingCat : Type (u + 1)

The category of rings.

Equations

• RingCat = CategoryTheory.Bundled Ring

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

Equations

• RingCat.instParentProjectionSemiringRingToSemiring = ⋯

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

Equations

• X.instRingα = X.str

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

Equations

• X.instRing = X.str

instance RingCat.instFunLike {X : RingCat} {Y : RingCat} : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• RingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike

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

Equations

• ⋯ = ⋯

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.

Equations

• RingCat.of R = CategoryTheory.Bundled.of R

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.

Equations

• RingCat.ofHom f = f

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

instance RingCat.instInhabited : Inhabited RingCat

Equations

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

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

Equations

• R.instRingα_1 = R.str

@[simp]

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

@[simp]

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

A variant of ofHom_apply that makes simpNF happy

@[simp]

theorem RingCat.coe_ringHom_id {X : RingCat} : ⇑(CategoryTheory.CategoryStruct.id X) = id

@[simp]

theorem RingCat.coe_id_of {X : Type u} [Ring X] : ⇑(CategoryTheory.CategoryStruct.id (RingCat.of X)) = ⇑(RingHom.id X)

@[simp]

theorem RingCat.coe_comp_of {X : Type u} {Y : Type u} {Z : Type u} [Ring X] [Ring Y] [Ring Z] (f : X →+* Y) (g : Y →+* Z) : ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑(g.comp f)

theorem RingCat.ext_of_iff {X : Type u} {Y : Type u} [Ring X] [Ring Y] {f : X →+* Y} {g : X →+* Y} : f = g ↔ ∀ (x : X), f x = g x

theorem RingCat.ext_of {X : Type u} {Y : Type u} [Ring X] [Ring Y] (f : X →+* Y) (g : X →+* Y) (h : ∀ (x : X), f x = g x) : f = g

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

Equations

• RingCat.hasForgetToSemiRingCat = CategoryTheory.BundledHom.forget₂ SemiRingCat.AssocRingHom @Ring.toSemiring

instance RingCat.hasForgetToAddCommGrp : CategoryTheory.HasForget₂ RingCat AddCommGrp

Equations

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

@[reducible, inline]

abbrev CommSemiRingCat : Type (u + 1)

The category of commutative semirings.

Equations

• CommSemiRingCat = CategoryTheory.Bundled CommSemiring

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

Equations

• CommSemiRingCat.instParentProjectionSemiringCommSemiringToSemiring = ⋯

instance CommSemiRingCat.instConcreteCategory : CategoryTheory.ConcreteCategory CommSemiRingCat

Equations

• CommSemiRingCat.instConcreteCategory = id inferInstance

instance CommSemiRingCat.instCoeSortType : CoeSort CommSemiRingCat (Type u_1)

Equations

• CommSemiRingCat.instCoeSortType = { coe := fun (X : CommSemiRingCat) => ↑X }

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

Equations

• X.instCommSemiringα = X.str

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

Equations

• X.instCommSemiring = X.str

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

Equations

• X.instCommSemiring' = X.str

instance CommSemiRingCat.instFunLike {X : CommSemiRingCat} {Y : CommSemiRingCat} : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• CommSemiRingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike

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

Equations

• ⋯ = ⋯

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.

Equations

• CommSemiRingCat.of R = CategoryTheory.Bundled.of R

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.

Equations

• CommSemiRingCat.ofHom f = f

@[simp]

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

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

@[simp]

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

A variant of ofHom_apply that makes simpNF happy

instance CommSemiRingCat.instInhabited : Inhabited CommSemiRingCat

Equations

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

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

Equations

• R.instCommSemiringα_1 = R.str

@[simp]

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

@[simp]

theorem CommSemiRingCat.coe_ringHom_id {X : CommSemiRingCat} : ⇑(CategoryTheory.CategoryStruct.id X) = id

@[simp]

theorem CommSemiRingCat.coe_id_of {X : Type u} [CommSemiring X] : ⇑(CategoryTheory.CategoryStruct.id (CommSemiRingCat.of X)) = ⇑(RingHom.id X)

@[simp]

theorem CommSemiRingCat.coe_comp_of {X : Type u} {Y : Type u} {Z : Type u} [CommSemiring X] [CommSemiring Y] [CommSemiring Z] (f : X →+* Y) (g : Y →+* Z) : ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑(g.comp f)

theorem CommSemiRingCat.ext_of_iff {X : Type u} {Y : Type u} [CommSemiring X] [CommSemiring Y] {f : X →+* Y} {g : X →+* Y} : f = g ↔ ∀ (x : X), f x = g x

theorem CommSemiRingCat.ext_of {X : Type u} {Y : Type u} [CommSemiring X] [CommSemiring Y] (f : X →+* Y) (g : X →+* Y) (h : ∀ (x : X), f x = g x) : f = g

instance CommSemiRingCat.hasForgetToSemiRingCat : CategoryTheory.HasForget₂ CommSemiRingCat SemiRingCat

Equations

• CommSemiRingCat.hasForgetToSemiRingCat = CategoryTheory.BundledHom.forget₂ SemiRingCat.AssocRingHom @CommSemiring.toSemiring

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.

@[simp]

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

@[simp]

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

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

Ring equivalence are isomorphisms in category of commutative semirings

Equations

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

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

Equations

• CommSemiRingCat.forgetReflectIsos = ⋯

@[reducible, inline]

abbrev CommRingCat : Type (u + 1)

The category of commutative rings.

Equations

• CommRingCat = CategoryTheory.Bundled CommRing

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

Equations

• CommRingCat.instParentProjectionRingCommRingToRing = ⋯

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

Equations

• X.instCommRing = X.str

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

Equations

• X.instCommRing' = X.str

instance CommRingCat.instFunLike {X : CommRingCat} {Y : CommRingCat} : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• CommRingCat.instFunLike = CategoryTheory.ConcreteCategory.instFunLike

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

Equations

• ⋯ = ⋯

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.id_apply (R : CommRingCat) (x : ↑R) : (CategoryTheory.CategoryStruct.id R) x = x

Specialization of ConcreteCategory.id_apply because simp can't see through the defeq.

@[simp]

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

@[simp]

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

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

Equations

• CommRingCat.of R = CategoryTheory.Bundled.of R

instance CommRingCat.instFunLike' {X : Type u_1} [CommRing X] {Y : CommRingCat} : FunLike (CommRingCat.of X ⟶ Y) X ↑Y

Equations

• CommRingCat.instFunLike' = CategoryTheory.ConcreteCategory.instFunLike

instance CommRingCat.instFunLike'' {X : CommRingCat} {Y : Type u_1} [CommRing Y] : FunLike (X ⟶ CommRingCat.of Y) (↑X) Y

Equations

• CommRingCat.instFunLike'' = CategoryTheory.ConcreteCategory.instFunLike

instance CommRingCat.instFunLike''' {X : Type u_1} {Y : Type u_1} [CommRing X] [CommRing Y] : FunLike (CommRingCat.of X ⟶ CommRingCat.of Y) X Y

Equations

• CommRingCat.instFunLike''' = CategoryTheory.ConcreteCategory.instFunLike

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.

Equations

• CommRingCat.ofHom f = f

@[simp]

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

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

@[simp]

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

A variant of ofHom_apply that makes simpNF happy

instance CommRingCat.instInhabited : Inhabited CommRingCat

Equations

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

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

Equations

• R.instCommRingα = R.str

@[simp]

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

@[simp]

theorem CommRingCat.coe_ringHom_id {X : CommRingCat} : ⇑(CategoryTheory.CategoryStruct.id X) = id

@[simp]

theorem CommRingCat.coe_id_of {X : Type u} [CommRing X] : ⇑(CategoryTheory.CategoryStruct.id (CommRingCat.of X)) = ⇑(RingHom.id X)

@[simp]

theorem CommRingCat.coe_comp_of {X : Type u} {Y : Type u} {Z : Type u} [CommRing X] [CommRing Y] [CommRing Z] (f : X →+* Y) (g : Y →+* Z) : ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑(g.comp f)

theorem CommRingCat.ext_of_iff {X : Type u} {Y : Type u} [CommRing X] [CommRing Y] {f : X →+* Y} {g : X →+* Y} : f = g ↔ ∀ (x : X), f x = g x

theorem CommRingCat.ext_of {X : Type u} {Y : Type u} [CommRing X] [CommRing Y] (f : X →+* Y) (g : X →+* Y) (h : ∀ (x : X), f x = g x) : f = g

instance CommRingCat.hasForgetToRingCat : CategoryTheory.HasForget₂ CommRingCat RingCat

Equations

• CommRingCat.hasForgetToRingCat = CategoryTheory.BundledHom.forget₂ (CategoryTheory.BundledHom.MapHom SemiRingCat.AssocRingHom @Ring.toSemiring) @CommRing.toRing

@[simp]

theorem CommRingCat.forgetToRingCat_obj (A : CommRingCat) : ↑((CategoryTheory.forget₂ CommRingCat RingCat).obj A) = ↑A

@[simp]

theorem CommRingCat.forgetToRingCat_map_apply {A : CommRingCat} {B : CommRingCat} (f : A ⟶ B) (a : ↑A) : ((CategoryTheory.forget₂ CommRingCat RingCat).map f) a = f a

instance CommRingCat.hasForgetToCommSemiRingCat : CategoryTheory.HasForget₂ CommRingCat CommSemiRingCat

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

Equations

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

instance CommRingCat.instFullCommSemiRingCatForget₂ : (CategoryTheory.forget₂ CommRingCat CommSemiRingCat).Full

Equations

• CommRingCat.instFullCommSemiRingCatForget₂ = ⋯

@[simp]

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

@[simp]

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

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.

Equations

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

@[simp]

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

@[simp]

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

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.

Equations

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

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

Build a RingEquiv from an isomorphism in the category RingCat.

Equations

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

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

Build a RingEquiv from an isomorphism in the category CommRingCat.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Iso.commRingIsoToRingEquiv_apply {X : CommRingCat} {Y : CommRingCat} (i : X ≅ Y) (x : ↑X) : i.commRingCatIsoToRingEquiv x = i.hom x

@[simp]

theorem CategoryTheory.Iso.commRingIsoToRingEquiv_symm_apply {X : CommRingCat} {Y : CommRingCat} (i : X ≅ Y) (y : ↑Y) : i.commRingCatIsoToRingEquiv.symm y = i.inv y

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.

Equations

• ringEquivIsoRingIso = { hom := fun (e : X ≃+* Y) => e.toRingCatIso, inv := fun (i : RingCat.of X ≅ RingCat.of Y) => i.ringCatIsoToRingEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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.

Equations

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

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

Equations

• RingCat.forget_reflects_isos = ⋯

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

Equations

• CommRingCat.forget_reflects_isos = ⋯

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) : g.comp f = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom f) (CommRingCat.ofHom g)

@[simp] lemmas for RingHom.comp and categorical identities.

@[simp]

theorem RingHom.comp_id_semiringCat {G : SemiRingCat} {H : Type u} [Semiring H] (f : ↑G →+* H) : f.comp (CategoryTheory.CategoryStruct.id G) = f

@[simp]

theorem RingHom.id_semiringCat_comp {G : Type u} [Semiring G] {H : SemiRingCat} (f : G →+* ↑H) : RingHom.comp (CategoryTheory.CategoryStruct.id H) f = f

@[simp]

theorem RingHom.comp_id_commSemiringCat {G : CommSemiRingCat} {H : Type u} [CommSemiring H] (f : ↑G →+* H) : f.comp (CategoryTheory.CategoryStruct.id G) = f

@[simp]

theorem RingHom.id_commSemiringCat_comp {G : Type u} [CommSemiring G] {H : CommSemiRingCat} (f : G →+* ↑H) : RingHom.comp (CategoryTheory.CategoryStruct.id H) f = f

@[simp]

theorem RingHom.comp_id_ringCat {G : RingCat} {H : Type u} [Ring H] (f : ↑G →+* H) : f.comp (CategoryTheory.CategoryStruct.id G) = f

@[simp]

theorem RingHom.id_ringCat_comp {G : Type u} [Ring G] {H : RingCat} (f : G →+* ↑H) : RingHom.comp (CategoryTheory.CategoryStruct.id H) f = f

@[simp]

theorem RingHom.comp_id_commRingCat {G : CommRingCat} {H : Type u} [CommRing H] (f : ↑G →+* H) : f.comp (CategoryTheory.CategoryStruct.id G) = f

@[simp]

theorem RingHom.id_commRingCat_comp {G : Type u} [CommRing G] {H : CommRingCat} (f : G →+* ↑H) : RingHom.comp (CategoryTheory.CategoryStruct.id H) f = f