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

We introduce the bundled categories:

along with the relevant forgetful functors between them.

source

structure SemiRingCat :

Type (u + 1)

The category of semirings.

of :: (

carrier : Type u
The underlying type.
semiring : Semiring ↑self

)

Instances For

source

instance SemiRingCat.instCoeSortType :

CoeSort SemiRingCat (Type u)

Equations

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

source

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

↑{ carrier := R, semiring := inst✝ } = R

source

theorem SemiRingCat.of_carrier (R : SemiRingCat) :

{ carrier := ↑R, semiring := R.semiring } = R

source

structure SemiRingCat.Hom (R S : SemiRingCat) :

Type u

The type of morphisms in SemiRingCat.

hom' : ↑R →+* ↑S
The underlying ring hom.

Instances For

source

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

x = y

source

theorem SemiRingCat.Hom.ext_iff {R S : SemiRingCat} {x y : R.Hom S} :

x = y ↔ x.hom' = y.hom'

source

instance SemiRingCat.instCategory :

CategoryTheory.Category.{u_1, u_1 + 1} SemiRingCat

Equations

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

source

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.

source

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

Instances For

source

@[reducible, inline]

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

{ carrier := R, semiring := inst✝ } ⟶ { carrier := S, semiring := inst✝¹ }

Typecheck a RingHom as a morphism in SemiRingCat.

Equations

SemiRingCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

Instances For

source

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

Instances For

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

source

@[simp]

theorem SemiRingCat.hom_id {R : SemiRingCat} :

Hom.hom (CategoryTheory.CategoryStruct.id R) = RingHom.id ↑R

source

theorem SemiRingCat.id_apply (R : SemiRingCat) (r : ↑R) :

(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id R)) r = r

source

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

source

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)

source

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

f = g

source

theorem SemiRingCat.hom_ext_iff {R S : SemiRingCat} {f g : R ⟶ S} :

f = g ↔ Hom.hom f = Hom.hom g

source

@[simp]

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

Hom.hom (ofHom f) = f

source

@[simp]

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

ofHom (Hom.hom f) = f

source

@[simp]

theorem SemiRingCat.ofHom_id {R : Type u} [Semiring R] :

ofHom (RingHom.id R) = CategoryTheory.CategoryStruct.id { carrier := R, semiring := inst✝ }

source

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

source

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

source

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

source

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

source

instance SemiRingCat.instInhabited :

Inhabited SemiRingCat

Equations

SemiRingCat.instInhabited = { default := { carrier := PUnit.{?u.2 + 1}, semiring := CommRing.toCommSemiring.toSemiring } }

source

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

Instances For

source

theorem SemiRingCat.forget_obj {R : SemiRingCat} :

(CategoryTheory.forget SemiRingCat).obj R = ↑R

source

theorem SemiRingCat.forget_map {R S : SemiRingCat} (f : R ⟶ S) :

(CategoryTheory.forget SemiRingCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

source

instance SemiRingCat.instSemiringObjForget {R : SemiRingCat} :

Semiring ((CategoryTheory.forget SemiRingCat).obj R)

Equations

SemiRingCat.instSemiringObjForget = inferInstance

source

instance SemiRingCat.hasForgetToMonCat :

CategoryTheory.HasForget₂ SemiRingCat MonCat

Equations

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

source

instance SemiRingCat.hasForgetToAddCommMonCat :

CategoryTheory.HasForget₂ SemiRingCat AddCommMonCat

Equations

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

source

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

{ carrier := R, semiring := inst✝ } ≅ { carrier := S, semiring := inst✝¹ }

Ring equivalences are isomorphisms in category of semirings

Equations

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

Instances For

source

@[simp]

theorem RingEquiv.toSemiRingCatIso_inv {R S : Type u} [Semiring R] [Semiring S] (e : R ≃+* S) :

e.toSemiRingCatIso.inv = SemiRingCat.ofHom ↑e.symm

source

@[simp]

theorem RingEquiv.toSemiRingCatIso_hom {R S : Type u} [Semiring R] [Semiring S] (e : R ≃+* S) :

e.toSemiRingCatIso.hom = SemiRingCat.ofHom ↑e

source

instance SemiRingCat.forgetReflectIsos :

(CategoryTheory.forget SemiRingCat).ReflectsIsomorphisms

source

structure RingCat :

Type (u + 1)

The category of rings.

of :: (

carrier : Type u
The underlying type.
ring : Ring ↑self

)

Instances For

source

instance RingCat.instCoeSortType :

CoeSort RingCat (Type u)

Equations

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

source

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

↑{ carrier := R, ring := inst✝ } = R

source

theorem RingCat.of_carrier (R : RingCat) :

{ carrier := ↑R, ring := R.ring } = R

source

structure RingCat.Hom (R S : RingCat) :

Type u

The type of morphisms in RingCat.

hom' : ↑R →+* ↑S
The underlying ring hom.

Instances For

source

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

x = y

source

theorem RingCat.Hom.ext_iff {R S : RingCat} {x y : R.Hom S} :

x = y ↔ x.hom' = y.hom'

source

instance RingCat.instCategory :

CategoryTheory.Category.{u_1, u_1 + 1} RingCat

Equations

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

source

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.

source

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

Instances For

source

@[reducible, inline]

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

{ carrier := R, ring := inst✝ } ⟶ { carrier := S, ring := inst✝¹ }

Typecheck a RingHom as a morphism in RingCat.

Equations

RingCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

Instances For

source

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

Instances For

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

source

@[simp]

theorem RingCat.hom_id {R : RingCat} :

Hom.hom (CategoryTheory.CategoryStruct.id R) = RingHom.id ↑R

source

theorem RingCat.id_apply (R : RingCat) (r : ↑R) :

(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id R)) r = r

source

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

source

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)

source

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

f = g

source

theorem RingCat.hom_ext_iff {R S : RingCat} {f g : R ⟶ S} :

f = g ↔ Hom.hom f = Hom.hom g

source

@[simp]

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

Hom.hom (ofHom f) = f

source

@[simp]

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

ofHom (Hom.hom f) = f

source

@[simp]

theorem RingCat.ofHom_id {R : Type u} [Ring R] :

ofHom (RingHom.id R) = CategoryTheory.CategoryStruct.id { carrier := R, ring := inst✝ }

source

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

source

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

source

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

source

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

source

instance RingCat.instInhabited :

Inhabited RingCat

Equations

RingCat.instInhabited = { default := { carrier := PUnit.{?u.2 + 1}, ring := PUnit.commRing.toRing } }

source

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

Instances For

source

theorem RingCat.forget_obj {R : RingCat} :

(CategoryTheory.forget RingCat).obj R = ↑R

source

theorem RingCat.forget_map {R S : RingCat} (f : R ⟶ S) :

(CategoryTheory.forget RingCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

source

instance RingCat.instRingObjForget {R : RingCat} :

Ring ((CategoryTheory.forget RingCat).obj R)

Equations

RingCat.instRingObjForget = inferInstance

source

instance RingCat.hasForgetToSemiRingCat :

CategoryTheory.HasForget₂ RingCat SemiRingCat

Equations

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

source

def RingCat.fullyFaithfulForget₂ToSemiRingCat :

(CategoryTheory.forget₂ RingCat SemiRingCat).FullyFaithful

The forgetful functor from RingCat to SemiRingCat is fully faithful.

Equations

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

Instances For

source

instance RingCat.instFullSemiRingCatForget₂ :

(CategoryTheory.forget₂ RingCat SemiRingCat).Full

source

instance RingCat.hasForgetToAddCommGrp :

CategoryTheory.HasForget₂ RingCat AddCommGrpCat

Equations

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

source

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

{ carrier := R, ring := inst✝ } ≅ { carrier := S, ring := inst✝¹ }

Ring equivalences are isomorphisms in category of rings

Equations

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

Instances For

source

@[simp]

theorem RingEquiv.toRingCatIso_inv {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) :

e.toRingCatIso.inv = RingCat.ofHom ↑e.symm

source

@[simp]

theorem RingEquiv.toRingCatIso_hom {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) :

e.toRingCatIso.hom = RingCat.ofHom ↑e

source

instance RingCat.forgetReflectIsos :

(CategoryTheory.forget RingCat).ReflectsIsomorphisms

source

structure CommSemiRingCat :

Type (u + 1)

The category of commutative semirings.

of :: (

carrier : Type u
The underlying type.
commSemiring : CommSemiring ↑self

)

Instances For

source

instance CommSemiRingCat.instCoeSortType :

CoeSort CommSemiRingCat (Type u)

Equations

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

source

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

↑{ carrier := R, commSemiring := inst✝ } = R

source

theorem CommSemiRingCat.of_carrier (R : CommSemiRingCat) :

{ carrier := ↑R, commSemiring := R.commSemiring } = R

source

structure CommSemiRingCat.Hom (R S : CommSemiRingCat) :

Type u

The type of morphisms in CommSemiRingCat.

hom' : ↑R →+* ↑S
The underlying ring hom.

Instances For

source

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

x = y

source

theorem CommSemiRingCat.Hom.ext_iff {R S : CommSemiRingCat} {x y : R.Hom S} :

x = y ↔ x.hom' = y.hom'

source

instance CommSemiRingCat.instCategory :

CategoryTheory.Category.{u_1, u_1 + 1} CommSemiRingCat

Equations

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

source

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.

source

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

Instances For

source

@[reducible, inline]

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

{ carrier := R, commSemiring := inst✝ } ⟶ { carrier := S, commSemiring := inst✝¹ }

Typecheck a RingHom as a morphism in CommSemiRingCat.

Equations

CommSemiRingCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

Instances For

source

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

Instances For

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

source

@[simp]

theorem CommSemiRingCat.hom_id {R : CommSemiRingCat} :

Hom.hom (CategoryTheory.CategoryStruct.id R) = RingHom.id ↑R

source

theorem CommSemiRingCat.id_apply (R : CommSemiRingCat) (r : ↑R) :

(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id R)) r = r

source

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

source

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)

source

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

f = g

source

theorem CommSemiRingCat.hom_ext_iff {R S : CommSemiRingCat} {f g : R ⟶ S} :

f = g ↔ Hom.hom f = Hom.hom g

source

@[simp]

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

Hom.hom (ofHom f) = f

source

@[simp]

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

ofHom (Hom.hom f) = f

source

@[simp]

theorem CommSemiRingCat.ofHom_id {R : Type u} [CommSemiring R] :

ofHom (RingHom.id R) = CategoryTheory.CategoryStruct.id { carrier := R, commSemiring := inst✝ }

source

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

source

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

source

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

source

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

source

instance CommSemiRingCat.instInhabited :

Inhabited CommSemiRingCat

Equations

CommSemiRingCat.instInhabited = { default := { carrier := PUnit.{?u.2 + 1}, commSemiring := CommRing.toCommSemiring } }

source

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

Instances For

source

theorem CommSemiRingCat.forget_obj {R : CommSemiRingCat} :

(CategoryTheory.forget CommSemiRingCat).obj R = ↑R

source

theorem CommSemiRingCat.forget_map {R S : CommSemiRingCat} (f : R ⟶ S) :

(CategoryTheory.forget CommSemiRingCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

source

instance CommSemiRingCat.instCommSemiringObjForget {R : CommSemiRingCat} :

CommSemiring ((CategoryTheory.forget CommSemiRingCat).obj R)

Equations

CommSemiRingCat.instCommSemiringObjForget = inferInstance

source

instance CommSemiRingCat.hasForgetToSemiRingCat :

CategoryTheory.HasForget₂ CommSemiRingCat SemiRingCat

Equations

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

source

def CommSemiRingCat.fullyFaithfulForget₂ToSemiRingCat :

(CategoryTheory.forget₂ CommSemiRingCat SemiRingCat).FullyFaithful

The forgetful functor from CommSemiRingCat to SemiRingCat is fully faithful.

Equations

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

Instances For

source

instance CommSemiRingCat.instFullSemiRingCatForget₂ :

(CategoryTheory.forget₂ CommSemiRingCat SemiRingCat).Full

source

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.

source

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

{ carrier := R, commSemiring := inst✝ } ≅ { carrier := S, commSemiring := inst✝¹ }

Ring equivalences are isomorphisms in category of commutative semirings

Equations

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

Instances For

source

@[simp]

theorem RingEquiv.toCommSemiRingCatIso_hom {R S : Type u} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) :

e.toCommSemiRingCatIso.hom = CommSemiRingCat.ofHom ↑e

source

@[simp]

theorem RingEquiv.toCommSemiRingCatIso_inv {R S : Type u} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) :

e.toCommSemiRingCatIso.inv = CommSemiRingCat.ofHom ↑e.symm

source

instance CommSemiRingCat.forgetReflectIsos :

(CategoryTheory.forget CommSemiRingCat).ReflectsIsomorphisms

source

structure CommRingCat :

Type (u + 1)

The category of commutative rings.

of :: (

carrier : Type u
The underlying type.
commRing : CommRing ↑self

)

Instances For

source

instance CommRingCat.instCoeSortType :

CoeSort CommRingCat (Type u)

Equations

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

source

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

↑{ carrier := R, commRing := inst✝ } = R

source

theorem CommRingCat.of_carrier (R : CommRingCat) :

{ carrier := ↑R, commRing := R.commRing } = R

source

structure CommRingCat.Hom (R S : CommRingCat) :

Type u

The type of morphisms in CommRingCat.

hom' : ↑R →+* ↑S
The underlying ring hom.

Instances For

source

theorem CommRingCat.Hom.ext_iff {R S : CommRingCat} {x y : R.Hom S} :

x = y ↔ x.hom' = y.hom'

source

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

x = y

source

instance CommRingCat.instCategory :

CategoryTheory.Category.{u_1, u_1 + 1} CommRingCat

Equations

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

source

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.

source

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

Instances For

source

@[reducible, inline]

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

{ carrier := R, commRing := inst✝ } ⟶ { carrier := S, commRing := inst✝¹ }

Typecheck a RingHom as a morphism in CommRingCat.

Equations

CommRingCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

Instances For

source

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

Instances For

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

source

@[simp]

theorem CommRingCat.hom_id {R : CommRingCat} :

Hom.hom (CategoryTheory.CategoryStruct.id R) = RingHom.id ↑R

source

theorem CommRingCat.id_apply (R : CommRingCat) (r : ↑R) :

(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id R)) r = r

source

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

source

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)

source

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

f = g

source

theorem CommRingCat.hom_ext_iff {R S : CommRingCat} {f g : R ⟶ S} :

f = g ↔ Hom.hom f = Hom.hom g

source

@[simp]

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

Hom.hom (ofHom f) = f

source

@[simp]

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

ofHom (Hom.hom f) = f

source

@[simp]

theorem CommRingCat.ofHom_id {R : Type u} [CommRing R] :

ofHom (RingHom.id R) = CategoryTheory.CategoryStruct.id { carrier := R, commRing := inst✝ }

source

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

source

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

source

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

source

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

source

instance CommRingCat.instInhabited :

Inhabited CommRingCat

Equations

CommRingCat.instInhabited = { default := { carrier := PUnit.{?u.2 + 1}, commRing := PUnit.commRing } }

source

theorem CommRingCat.forget_obj {R : CommRingCat} :

(CategoryTheory.forget CommRingCat).obj R = ↑R

source

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

Instances For

source

theorem CommRingCat.forget_map {R S : CommRingCat} (f : R ⟶ S) :

(CategoryTheory.forget CommRingCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

source

instance CommRingCat.instCommRingObjForget {R : CommRingCat} :

CommRing ((CategoryTheory.forget CommRingCat).obj R)

Equations

CommRingCat.instCommRingObjForget = inferInstance

source

instance CommRingCat.hasForgetToRingCat :

CategoryTheory.HasForget₂ CommRingCat RingCat

Equations

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

source

def CommRingCat.fullyFaithfulForget₂ToRingCat :

(CategoryTheory.forget₂ CommRingCat RingCat).FullyFaithful

The forgetful functor from CommRingCat to RingCat is fully faithful.

Equations

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

Instances For

source

instance CommRingCat.instFullRingCatForget₂ :

(CategoryTheory.forget₂ CommRingCat RingCat).Full

source

@[simp]

theorem CommRingCat.forgetToRingCat_map_hom {R S : CommRingCat} (f : R ⟶ S) :

RingCat.Hom.hom ((CategoryTheory.forget₂ CommRingCat RingCat).map f) = Hom.hom f

source

@[simp]

theorem CommRingCat.forgetToRingCat_obj {R : CommRingCat} :

↑((CategoryTheory.forget₂ CommRingCat RingCat).obj R) = ↑R

source

instance CommRingCat.hasForgetToAddCommMonCat :

CategoryTheory.HasForget₂ CommRingCat CommSemiRingCat

Equations

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

source

instance CommRingCat.instHasForget₂CommMonCat :

CategoryTheory.HasForget₂ CommRingCat CommMonCat

Equations

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

source

@[simp]

theorem CommRingCat.forget₂_obj_coe (M : CommRingCat) :

↑(CategoryTheory.HasForget₂.forget₂.obj M) = ↑M

source

@[simp]

theorem CommRingCat.forget₂_map {X✝ Y✝ : CommRingCat} (f : X✝ ⟶ Y✝) :

CategoryTheory.HasForget₂.forget₂.map f = CommMonCat.ofHom ↑(Hom.hom f)

source

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

{ carrier := R, commRing := inst✝ } ≅ { carrier := S, commRing := inst✝¹ }

Ring equivalences are isomorphisms in category of commutative rings

Equations

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

Instances For

source

@[simp]

theorem RingEquiv.toCommRingCatIso_inv {R S : Type u} [CommRing R] [CommRing S] (e : R ≃+* S) :

e.toCommRingCatIso.inv = CommRingCat.ofHom ↑e.symm

source

@[simp]

theorem RingEquiv.toCommRingCatIso_hom {R S : Type u} [CommRing R] [CommRing S] (e : R ≃+* S) :

e.toCommRingCatIso.hom = CommRingCat.ofHom ↑e

source

instance CommRingCat.forgetReflectIsos :

(CategoryTheory.forget CommRingCat).ReflectsIsomorphisms

source

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) ⋯ ⋯

Instances For

source

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) ⋯ ⋯

Instances For

source

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) ⋯ ⋯

Instances For

source

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) ⋯ ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Iso.semiRingCatIsoToRingEquiv_toRingHom {R S : SemiRingCat} (e : R ≅ S) :

↑e.semiRingCatIsoToRingEquiv = SemiRingCat.Hom.hom e.hom

source

@[simp]

theorem CategoryTheory.Iso.ringCatIsoToRingEquiv_toRingHom {R S : RingCat} (e : R ≅ S) :

↑e.ringCatIsoToRingEquiv = RingCat.Hom.hom e.hom

source

@[simp]

theorem CategoryTheory.Iso.commSemiRingCatIsoToRingEquiv_toRingHom {R S : CommSemiRingCat} (e : R ≅ S) :

↑e.commSemiRingCatIsoToRingEquiv = CommSemiRingCat.Hom.hom e.hom

source

@[simp]

theorem CategoryTheory.Iso.commRingCatIsoToRingEquiv_toRingHom {R S : CommRingCat} (e : R ≅ S) :

↑e.commRingCatIsoToRingEquiv = CommRingCat.Hom.hom e.hom

source

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

source

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

Documentation

Mathlib.Algebra.Category.Ring.Basic

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

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

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