Category instances for Semiring, Ring, CommSemiring, and CommRing.

We introduce the bundled categories:

• SemiRingCat
• RingCat
• CommSemiRingCat
• CommRingCat along with the relevant forgetful functors between them.

def SemiRingCat : Type (u + 1)

The category of semirings.

Equations

• SemiRingCat = CategoryTheory.Bundled Semiring

@[inline, reducible]

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

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

Equations

• SemiRingCatMax = SemiRingCat

@[inline, reducible]

abbrev SemiRingCat.AssocRingHom (M : Type u_1) (N : Type u_2) [Semiring M] [Semiring N] : Type (max u_1 u_2)

RingHom doesn't actually assume associativity. This alias is needed to make the category theory machinery work. We use the same trick in MonCat.AssocMonoidHom.

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.instConcreteCategorySemiRingCatInstSemiRingCatLargeCategory : CategoryTheory.ConcreteCategory SemiRingCat

Equations

• SemiRingCat.instConcreteCategorySemiRingCatInstSemiRingCatLargeCategory = id inferInstance

instance SemiRingCat.instCoeSortSemiRingCatType : CoeSort SemiRingCat (Type u_1)

Equations

• SemiRingCat.instCoeSortSemiRingCatType = { coe := fun (X : SemiRingCat) => ↑X }

def SemiRingCat.forget_obj_eq_coe (R : SemiRingCat) : Prop

Equations

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

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

Equations

• SemiRingCat.instSemiring X = X.str

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

Equations

• SemiRingCat.instSemiring' X = 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

• (_ : RingHomClass (X ⟶ Y) ↑X ↑Y) = (_ : RingHomClass (↑X →+* ↑Y) ↑X ↑Y)

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

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

@[simp]

theorem SemiRingCat.forget_map {X : SemiRingCat} {Y : SemiRingCat} (f : X ⟶ Y) : (CategoryTheory.forget SemiRingCat).toPrefunctor.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.RingEquiv_coe_eq {X : Type u_1} {Y : Type u_1} [Semiring X] [Semiring Y] (e : X ≃+* Y) : ⇑↑e = ⇑e

instance SemiRingCat.instInhabitedSemiRingCat : Inhabited SemiRingCat

Equations

• SemiRingCat.instInhabitedSemiRingCat = { default := SemiRingCat.of PUnit.{u_1 + 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 RingEquiv.toSemiRingCatIso_hom {X : Type u_1} {Y : Type u_1} [Semiring X] [Semiring Y] (e : X ≃+* Y) : (RingEquiv.toSemiRingCatIso e).hom = RingEquiv.toRingHom e

@[simp]

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

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

Ring equivalence are isomorphisms in category of semirings

Equations

• RingEquiv.toSemiRingCatIso e = CategoryTheory.Iso.mk (RingEquiv.toRingHom e) (RingEquiv.toRingHom (RingEquiv.symm e))

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

Equations

• SemiRingCat.forgetReflectIsos = (_ : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget SemiRingCat))

def RingCat : Type (u + 1)

The category of rings.

Equations

• RingCat = CategoryTheory.Bundled Ring

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

Equations

• RingCat.instParentProjectionTypeSemiringRingToSemiring = (_ : CategoryTheory.BundledHom.ParentProjection @Ring.toSemiring)

instance RingCat.instConcreteCategoryRingCatInstRingCatLargeCategory : CategoryTheory.ConcreteCategory RingCat

Equations

• RingCat.instConcreteCategoryRingCatInstRingCatLargeCategory = id inferInstance

instance RingCat.instCoeSortRingCatType : CoeSort RingCat (Type u_1)

Equations

• RingCat.instCoeSortRingCatType = { coe := fun (X : RingCat) => ↑X }

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

Equations

• RingCat.instRingα X = X.str

def RingCat.forget_obj_eq_coe (R : RingCat) : Prop

Equations

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

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

Equations

• RingCat.instRing X = X.str

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

Equations

• RingCat.instRing' X = 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

• (_ : RingHomClass (X ⟶ Y) ↑X ↑Y) = (_ : RingHomClass (↑X →+* ↑Y) ↑X ↑Y)

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

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

@[simp]

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

instance RingCat.instInhabitedRingCat : Inhabited RingCat

Equations

• RingCat.instInhabitedRingCat = { default := RingCat.of PUnit.{u_1 + 1} }

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

Equations

• RingCat.instRingα_1 R = R.str

@[simp]

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

@[simp]

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

instance RingCat.hasForgetToSemiRingCat : CategoryTheory.HasForget₂ RingCat SemiRingCat

Equations

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

instance RingCat.hasForgetToAddCommGroupCat : CategoryTheory.HasForget₂ RingCat AddCommGroupCat

Equations

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

def CommSemiRingCat : Type (u + 1)

The category of commutative semirings.

Equations

• CommSemiRingCat = CategoryTheory.Bundled CommSemiring

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

Equations

• CommSemiRingCat.instParentProjectionTypeSemiringCommSemiringToSemiring = (_ : CategoryTheory.BundledHom.ParentProjection @CommSemiring.toSemiring)

instance CommSemiRingCat.instConcreteCategoryCommSemiRingCatInstCommSemiRingCatLargeCategory : CategoryTheory.ConcreteCategory CommSemiRingCat

Equations

• CommSemiRingCat.instConcreteCategoryCommSemiRingCatInstCommSemiRingCatLargeCategory = id inferInstance

instance CommSemiRingCat.instCoeSortCommSemiRingCatType : CoeSort CommSemiRingCat (Type u_1)

Equations

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

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

Equations

• CommSemiRingCat.instCommSemiringα X = X.str

def CommSemiRingCat.forget_obj_eq_coe (R : CommSemiRingCat) : Prop

Equations

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

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

Equations

• CommSemiRingCat.instCommSemiring X = X.str

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

Equations

• CommSemiRingCat.instCommSemiring' X = 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

• (_ : RingHomClass (X ⟶ Y) ↑X ↑Y) = (_ : RingHomClass (↑X →+* ↑Y) ↑X ↑Y)

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

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

@[simp]

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

instance CommSemiRingCat.instInhabitedCommSemiRingCat : Inhabited CommSemiRingCat

Equations

• CommSemiRingCat.instInhabitedCommSemiRingCat = { default := CommSemiRingCat.of PUnit.{u_1 + 1} }

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

Equations

• CommSemiRingCat.instCommSemiringα_1 R = R.str

@[simp]

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

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_inv {X : Type u_1} {Y : Type u_1} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) : (RingEquiv.toCommSemiRingCatIso e).inv = RingEquiv.toRingHom (RingEquiv.symm e)

@[simp]

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

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

Ring equivalence are isomorphisms in category of commutative semirings

Equations

• RingEquiv.toCommSemiRingCatIso e = CategoryTheory.Iso.mk (RingEquiv.toRingHom e) (RingEquiv.toRingHom (RingEquiv.symm e))

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

Equations

• CommSemiRingCat.forgetReflectIsos = (_ : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget CommSemiRingCat))

def CommRingCat : Type (u + 1)

The category of commutative rings.

Equations

• CommRingCat = CategoryTheory.Bundled CommRing

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

Equations

• CommRingCat.instParentProjectionTypeRingCommRingToRing = (_ : CategoryTheory.BundledHom.ParentProjection @CommRing.toRing)

instance CommRingCat.instConcreteCategoryCommRingCatInstCommRingCatLargeCategory : CategoryTheory.ConcreteCategory CommRingCat

Equations

• CommRingCat.instConcreteCategoryCommRingCatInstCommRingCatLargeCategory = id inferInstance

instance CommRingCat.instCoeSortCommRingCatType : CoeSort CommRingCat (Type u_1)

Equations

• CommRingCat.instCoeSortCommRingCatType = { coe := fun (X : CommRingCat) => ↑X }

def CommRingCat.forget_obj_eq_coe (R : CommRingCat) : Prop

Equations

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

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

Equations

• CommRingCat.instCommRing X = X.str

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

Equations

• CommRingCat.instCommRing' X = 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

• (_ : RingHomClass (X ⟶ Y) ↑X ↑Y) = (_ : RingHomClass (↑X →+* ↑Y) ↑X ↑Y)

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

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

@[simp]

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

instance CommRingCat.instInhabitedCommRingCat : Inhabited CommRingCat

Equations

• CommRingCat.instInhabitedCommRingCat = { default := CommRingCat.of PUnit.{u_1 + 1} }

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

Equations

• CommRingCat.instCommRingα R = R.str

@[simp]

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

instance CommRingCat.hasForgetToRingCat : CategoryTheory.HasForget₂ CommRingCat RingCat

Equations

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

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.instFullCommRingCatInstCommRingCatLargeCategoryCommSemiRingCatInstCommSemiRingCatLargeCategoryForget₂InstConcreteCategoryCommRingCatInstCommRingCatLargeCategoryInstConcreteCategoryCommSemiRingCatInstCommSemiRingCatLargeCategoryHasForgetToCommSemiRingCat : CategoryTheory.Full (CategoryTheory.forget₂ CommRingCat CommSemiRingCat)

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

• RingEquiv.toRingCatIso e = CategoryTheory.Iso.mk (RingEquiv.toRingHom e) (RingEquiv.toRingHom (RingEquiv.symm e))

@[simp]

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

@[simp]

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

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

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

Equations

• RingEquiv.toCommRingCatIso e = CategoryTheory.Iso.mk (RingEquiv.toRingHom e) (RingEquiv.toRingHom (RingEquiv.symm e))

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

Build a RingEquiv from an isomorphism in the category RingCat.

Equations

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

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

Build a RingEquiv from an isomorphism in the category CommRingCat.

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

• ringEquivIsoRingIso = CategoryTheory.Iso.mk (fun (e : X ≃+* Y) => RingEquiv.toRingCatIso e) fun (i : RingCat.of X ≅ RingCat.of Y) => CategoryTheory.Iso.ringCatIsoToRingEquiv i

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.ReflectsIsomorphisms (CategoryTheory.forget RingCat)

Equations

• RingCat.forget_reflects_isos = (_ : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget RingCat))

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

Equations

• CommRingCat.forget_reflects_isos = (_ : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget CommRingCat))

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

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