mathlib3 documentation

algebra.category.Ring.limits

The category of (commutative) rings has all limits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Further, these limits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.

def library_note.change elaboration strategy with `by apply` :

Some definitions may be extremely slow to elaborate, when the target type to be constructed is complicated and when the type of the term given in the definition is also complicated and does not obviously match the target type. In this case, instead of just giving the term, prefixing it with by apply may speed up things considerably as the types are not elaborated in the same order.

@[protected, instance]

def SemiRing.semiring_obj {J : Type v} [category_theory.small_category J] (F : J ⥤ SemiRing) (j : J) :

semiring ((F ⋙ category_theory.forget SemiRing).obj j)

Equations

SemiRing.semiring_obj F j = id (F.obj j).semiring

def SemiRing.sections_subsemiring {J : Type v} [category_theory.small_category J] (F : J ⥤ SemiRing) :

subsemiring (Π (j : J), ↥(F.obj j))

The flat sections of a functor into SemiRing form a subsemiring of all sections.

Equations

SemiRing.sections_subsemiring F = {carrier := (F ⋙ category_theory.forget SemiRing).sections, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _}

@[protected, instance]

def SemiRing.limit_semiring {J : Type v} [category_theory.small_category J] (F : J ⥤ SemiRing) :

semiring (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget SemiRing)).X

Equations

SemiRing.limit_semiring F = (SemiRing.sections_subsemiring F).to_semiring

def SemiRing.limit_π_ring_hom {J : Type v} [category_theory.small_category J] (F : J ⥤ SemiRing) (j : J) :

(category_theory.limits.types.limit_cone (F ⋙ category_theory.forget SemiRing)).X →+* (F ⋙ category_theory.forget SemiRing).obj j

limit.π (F ⋙ forget SemiRing) j as a ring_hom.

Equations

SemiRing.limit_π_ring_hom F j = {to_fun := (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget SemiRing)).π.app j, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

def SemiRing.has_limits.limit_cone {J : Type v} [category_theory.small_category J] (F : J ⥤ SemiRing) :

category_theory.limits.cone F

Construction of a limit cone in SemiRing. (Internal use only; use the limits API.)

Equations

SemiRing.has_limits.limit_cone F = {X := SemiRing.of (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget SemiRing)).X (SemiRing.limit_semiring F), π := {app := SemiRing.limit_π_ring_hom F, naturality' := _}}

def SemiRing.has_limits.limit_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ SemiRing) :

category_theory.limits.is_limit (SemiRing.has_limits.limit_cone F)

Witness that the limit cone in SemiRing is a limit cone. (Internal use only; use the limits API.)

Equations

SemiRing.has_limits.limit_cone_is_limit F = category_theory.limits.is_limit.of_faithful (category_theory.forget SemiRing) (category_theory.limits.types.limit_cone_is_limit (F ⋙ category_theory.forget SemiRing)) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget SemiRing).map_cone s).X), ⟨λ (j : J), ((category_theory.forget SemiRing).map_cone s).π.app j v, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}) _

@[protected, instance, irreducible]

def SemiRing.has_limits_of_size :

category_theory.limits.has_limits_of_size SemiRing

The category of rings has all limits.

@[protected, instance]

def SemiRing.has_limits :

category_theory.limits.has_limits SemiRing

noncomputable def SemiRing.forget₂_AddCommMon_preserves_limits_aux {J : Type v} [category_theory.small_category J] (F : J ⥤ SemiRing) :

category_theory.limits.is_limit ((category_theory.forget₂ SemiRing AddCommMon).map_cone (SemiRing.has_limits.limit_cone F))

An auxiliary declaration to speed up typechecking.

Equations

SemiRing.forget₂_AddCommMon_preserves_limits_aux F = AddCommMon.limit_cone_is_limit (F ⋙ category_theory.forget₂ SemiRing AddCommMon)

@[protected, instance]

noncomputable def SemiRing.forget₂_AddCommMon_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget₂ SemiRing AddCommMon)

The forgetful functor from semirings to additive commutative monoids preserves all limits.

Equations

SemiRing.forget₂_AddCommMon_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ SemiRing), category_theory.limits.preserves_limit_of_preserves_limit_cone (SemiRing.has_limits.limit_cone_is_limit F) (SemiRing.forget₂_AddCommMon_preserves_limits_aux F)}}

@[protected, instance]

noncomputable def SemiRing.forget₂_AddCommMon_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget₂ SemiRing AddCommMon)

Equations

SemiRing.forget₂_AddCommMon_preserves_limits = SemiRing.forget₂_AddCommMon_preserves_limits_of_size

def SemiRing.forget₂_Mon_preserves_limits_aux {J : Type v} [category_theory.small_category J] (F : J ⥤ SemiRing) :

category_theory.limits.is_limit ((category_theory.forget₂ SemiRing Mon).map_cone (SemiRing.has_limits.limit_cone F))

An auxiliary declaration to speed up typechecking.

Equations

SemiRing.forget₂_Mon_preserves_limits_aux F = Mon.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ SemiRing Mon)

@[protected, instance]

def SemiRing.forget₂_Mon_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget₂ SemiRing Mon)

The forgetful functor from semirings to monoids preserves all limits.

Equations

SemiRing.forget₂_Mon_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ SemiRing), category_theory.limits.preserves_limit_of_preserves_limit_cone (SemiRing.has_limits.limit_cone_is_limit F) (SemiRing.forget₂_Mon_preserves_limits_aux F)}}

@[protected, instance]

def SemiRing.forget₂_Mon_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget₂ SemiRing Mon)

Equations

SemiRing.forget₂_Mon_preserves_limits = SemiRing.forget₂_Mon_preserves_limits_of_size

@[protected, instance]

def SemiRing.forget_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget SemiRing)

The forgetful functor from semirings to types preserves all limits.

Equations

SemiRing.forget_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ SemiRing), category_theory.limits.preserves_limit_of_preserves_limit_cone (SemiRing.has_limits.limit_cone_is_limit F) (category_theory.limits.types.limit_cone_is_limit (F ⋙ category_theory.forget SemiRing))}}

@[protected, instance]

def SemiRing.forget_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget SemiRing)

Equations

SemiRing.forget_preserves_limits = SemiRing.forget_preserves_limits_of_size

@[protected, instance]

def CommSemiRing.comm_semiring_obj {J : Type v} [category_theory.small_category J] (F : J ⥤ CommSemiRing) (j : J) :

comm_semiring ((F ⋙ category_theory.forget CommSemiRing).obj j)

Equations

CommSemiRing.comm_semiring_obj F j = id (F.obj j).comm_semiring

@[protected, instance]

def CommSemiRing.limit_comm_semiring {J : Type v} [category_theory.small_category J] (F : J ⥤ CommSemiRing) :

comm_semiring (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget CommSemiRing)).X

Equations

CommSemiRing.limit_comm_semiring F = (SemiRing.sections_subsemiring (F ⋙ category_theory.forget₂ CommSemiRing SemiRing)).to_comm_semiring

@[protected, instance]

noncomputable def CommSemiRing.category_theory.forget₂.category_theory.creates_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ CommSemiRing) :

category_theory.creates_limit F (category_theory.forget₂ CommSemiRing SemiRing)

We show that the forgetful functor CommSemiRing ⥤ SemiRing creates limits.

All we need to do is notice that the limit point has a comm_semiring instance available, and then reuse the existing limit.

Equations

CommSemiRing.category_theory.forget₂.category_theory.creates_limit F = category_theory.creates_limit_of_reflects_iso (λ (c' : category_theory.limits.cone (F ⋙ category_theory.forget₂ CommSemiRing SemiRing)) (t : category_theory.limits.is_limit c'), {to_liftable_cone := {lifted_cone := {X := CommSemiRing.of (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget CommSemiRing)).X (CommSemiRing.limit_comm_semiring F), π := {app := λ (Y : J), (SemiRing.has_limits.limit_cone (F ⋙ category_theory.forget₂ CommSemiRing SemiRing)).π.app Y, naturality' := _}}, valid_lift := (SemiRing.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ CommSemiRing SemiRing)).unique_up_to_iso t}, makes_limit := category_theory.limits.is_limit.of_faithful (category_theory.forget₂ CommSemiRing SemiRing) (SemiRing.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ CommSemiRing SemiRing)) (λ (s : category_theory.limits.cone F), (SemiRing.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ CommSemiRing SemiRing)).lift ((category_theory.forget₂ CommSemiRing SemiRing).map_cone s)) _})

noncomputable def CommSemiRing.limit_cone {J : Type v} [category_theory.small_category J] (F : J ⥤ CommSemiRing) :

category_theory.limits.cone F

A choice of limit cone for a functor into CommSemiRing. (Generally, you'll just want to use limit F.)

Equations

CommSemiRing.limit_cone F = category_theory.lift_limit (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ CommSemiRing SemiRing))

noncomputable def CommSemiRing.limit_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ CommSemiRing) :

category_theory.limits.is_limit (CommSemiRing.limit_cone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations

CommSemiRing.limit_cone_is_limit F = category_theory.lifted_limit_is_limit (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ CommSemiRing SemiRing))

@[protected, instance, irreducible]

def CommSemiRing.has_limits_of_size :

category_theory.limits.has_limits_of_size CommSemiRing

The category of rings has all limits.

@[protected, instance]

def CommSemiRing.has_limits :

category_theory.limits.has_limits CommSemiRing

@[protected, instance]

noncomputable def CommSemiRing.forget₂_SemiRing_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget₂ CommSemiRing SemiRing)

The forgetful functor from rings to semirings preserves all limits.

Equations

CommSemiRing.forget₂_SemiRing_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ CommSemiRing), category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ CommSemiRing SemiRing)}}

@[protected, instance]

noncomputable def CommSemiRing.forget₂_SemiRing_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget₂ CommSemiRing SemiRing)

Equations

CommSemiRing.forget₂_SemiRing_preserves_limits = CommSemiRing.forget₂_SemiRing_preserves_limits_of_size

@[protected, instance]

noncomputable def CommSemiRing.forget_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget CommSemiRing)

The forgetful functor from rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations

CommSemiRing.forget_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ CommSemiRing), category_theory.limits.comp_preserves_limit (category_theory.forget₂ CommSemiRing SemiRing) (category_theory.forget SemiRing)}}

@[protected, instance]

noncomputable def CommSemiRing.forget_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget CommSemiRing)

Equations

CommSemiRing.forget_preserves_limits = CommSemiRing.forget_preserves_limits_of_size

@[protected, instance]

def Ring.ring_obj {J : Type v} [category_theory.small_category J] (F : J ⥤ Ring) (j : J) :

ring ((F ⋙ category_theory.forget Ring).obj j)

Equations

Ring.ring_obj F j = id (F.obj j).ring

def Ring.sections_subring {J : Type v} [category_theory.small_category J] (F : J ⥤ Ring) :

subring (Π (j : J), ↥(F.obj j))

The flat sections of a functor into Ring form a subring of all sections.

Equations

Ring.sections_subring F = {carrier := (F ⋙ category_theory.forget Ring).sections, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, neg_mem' := _}

@[protected, instance]

def Ring.limit_ring {J : Type v} [category_theory.small_category J] (F : J ⥤ Ring) :

ring (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget Ring)).X

Equations

Ring.limit_ring F = (Ring.sections_subring F).to_ring

@[protected, instance]

noncomputable def Ring.category_theory.forget₂.category_theory.creates_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ Ring) :

category_theory.creates_limit F (category_theory.forget₂ Ring SemiRing)

We show that the forgetful functor CommRing ⥤ Ring creates limits.

All we need to do is notice that the limit point has a ring instance available, and then reuse the existing limit.

Equations

Ring.category_theory.forget₂.category_theory.creates_limit F = category_theory.creates_limit_of_reflects_iso (λ (c' : category_theory.limits.cone (F ⋙ category_theory.forget₂ Ring SemiRing)) (t : category_theory.limits.is_limit c'), {to_liftable_cone := {lifted_cone := {X := Ring.of (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget Ring)).X (Ring.limit_ring F), π := {app := λ (Y : J), (SemiRing.has_limits.limit_cone (F ⋙ category_theory.forget₂ Ring SemiRing)).π.app Y, naturality' := _}}, valid_lift := (SemiRing.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ Ring SemiRing)).unique_up_to_iso t}, makes_limit := category_theory.limits.is_limit.of_faithful (category_theory.forget₂ Ring SemiRing) (SemiRing.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ Ring SemiRing)) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget SemiRing).map_cone ((category_theory.forget₂ Ring SemiRing).map_cone s)).X), ⟨λ (j : J), ((category_theory.forget SemiRing).map_cone ((category_theory.forget₂ Ring SemiRing).map_cone s)).π.app j v, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}) _})

noncomputable def Ring.limit_cone {J : Type v} [category_theory.small_category J] (F : J ⥤ Ring) :

category_theory.limits.cone F

A choice of limit cone for a functor into Ring. (Generally, you'll just want to use limit F.)

Equations

Ring.limit_cone F = category_theory.lift_limit (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ Ring SemiRing))

noncomputable def Ring.limit_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ Ring) :

category_theory.limits.is_limit (Ring.limit_cone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations

Ring.limit_cone_is_limit F = category_theory.lifted_limit_is_limit (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ Ring SemiRing))

@[protected, instance, irreducible]

def Ring.has_limits_of_size :

category_theory.limits.has_limits_of_size Ring

The category of rings has all limits.

@[protected, instance]

def Ring.has_limits :

category_theory.limits.has_limits Ring

@[protected, instance]

noncomputable def Ring.forget₂_SemiRing_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget₂ Ring SemiRing)

The forgetful functor from rings to semirings preserves all limits.

Equations

Ring.forget₂_SemiRing_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ Ring), category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ Ring SemiRing)}}

@[protected, instance]

noncomputable def Ring.forget₂_SemiRing_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget₂ Ring SemiRing)

Equations

Ring.forget₂_SemiRing_preserves_limits = Ring.forget₂_SemiRing_preserves_limits_of_size

noncomputable def Ring.forget₂_AddCommGroup_preserves_limits_aux {J : Type v} [category_theory.small_category J] (F : J ⥤ Ring) :

category_theory.limits.is_limit ((category_theory.forget₂ Ring AddCommGroup).map_cone (Ring.limit_cone F))

An auxiliary declaration to speed up typechecking.

Equations

Ring.forget₂_AddCommGroup_preserves_limits_aux F = AddCommGroup.limit_cone_is_limit (F ⋙ category_theory.forget₂ Ring AddCommGroup)

@[protected, instance]

noncomputable def Ring.forget₂_AddCommGroup_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget₂ Ring AddCommGroup)

The forgetful functor from rings to additive commutative groups preserves all limits.

Equations

Ring.forget₂_AddCommGroup_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ Ring), category_theory.limits.preserves_limit_of_preserves_limit_cone (Ring.limit_cone_is_limit F) (Ring.forget₂_AddCommGroup_preserves_limits_aux F)}}

@[protected, instance]

noncomputable def Ring.forget₂_AddCommGroup_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget₂ Ring AddCommGroup)

Equations

Ring.forget₂_AddCommGroup_preserves_limits = Ring.forget₂_AddCommGroup_preserves_limits_of_size

@[protected, instance]

noncomputable def Ring.forget_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget Ring)

The forgetful functor from rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations

Ring.forget_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ Ring), category_theory.limits.comp_preserves_limit (category_theory.forget₂ Ring SemiRing) (category_theory.forget SemiRing)}}

@[protected, instance]

noncomputable def Ring.forget_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget Ring)

Equations

Ring.forget_preserves_limits = Ring.forget_preserves_limits_of_size

@[protected, instance]

def CommRing.comm_ring_obj {J : Type v} [category_theory.small_category J] (F : J ⥤ CommRing) (j : J) :

comm_ring ((F ⋙ category_theory.forget CommRing).obj j)

Equations

CommRing.comm_ring_obj F j = id (F.obj j).comm_ring

@[protected, instance]

def CommRing.limit_comm_ring {J : Type v} [category_theory.small_category J] (F : J ⥤ CommRing) :

comm_ring (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget CommRing)).X

Equations

CommRing.limit_comm_ring F = (Ring.sections_subring (F ⋙ category_theory.forget₂ CommRing Ring)).to_comm_ring

@[protected, instance]

noncomputable def CommRing.category_theory.forget₂.category_theory.creates_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ CommRing) :

category_theory.creates_limit F (category_theory.forget₂ CommRing Ring)

We show that the forgetful functor CommRing ⥤ Ring creates limits.

All we need to do is notice that the limit point has a comm_ring instance available, and then reuse the existing limit.

Equations

CommRing.category_theory.forget₂.category_theory.creates_limit F = category_theory.creates_limit_of_reflects_iso (λ (c' : category_theory.limits.cone (F ⋙ category_theory.forget₂ CommRing Ring)) (t : category_theory.limits.is_limit c'), {to_liftable_cone := {lifted_cone := {X := CommRing.of (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget CommRing)).X (CommRing.limit_comm_ring F), π := {app := λ (Y : J), (SemiRing.has_limits.limit_cone (F ⋙ category_theory.forget₂ CommRing Ring ⋙ category_theory.forget₂ Ring SemiRing)).π.app Y, naturality' := _}}, valid_lift := (Ring.limit_cone_is_limit (F ⋙ category_theory.forget₂ CommRing Ring)).unique_up_to_iso t}, makes_limit := category_theory.limits.is_limit.of_faithful (category_theory.forget₂ CommRing Ring) (Ring.limit_cone_is_limit (F ⋙ category_theory.forget₂ CommRing Ring)) (λ (s : category_theory.limits.cone F), (Ring.limit_cone_is_limit (F ⋙ category_theory.forget₂ CommRing Ring)).lift ((category_theory.forget₂ CommRing Ring).map_cone s)) _})

noncomputable def CommRing.limit_cone {J : Type v} [category_theory.small_category J] (F : J ⥤ CommRing) :

category_theory.limits.cone F

A choice of limit cone for a functor into CommRing. (Generally, you'll just want to use limit F.)

Equations

CommRing.limit_cone F = category_theory.lift_limit (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ CommRing Ring))

noncomputable def CommRing.limit_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ CommRing) :

category_theory.limits.is_limit (CommRing.limit_cone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations

CommRing.limit_cone_is_limit F = category_theory.lifted_limit_is_limit (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ CommRing Ring))

@[protected, instance, irreducible]

def CommRing.has_limits_of_size :

category_theory.limits.has_limits_of_size CommRing

The category of commutative rings has all limits.

@[protected, instance]

def CommRing.has_limits :

category_theory.limits.has_limits CommRing

@[protected, instance]

noncomputable def CommRing.forget₂_Ring_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget₂ CommRing Ring)

The forgetful functor from commutative rings to rings preserves all limits. (That is, the underlying rings could have been computed instead as limits in the category of rings.)

Equations

CommRing.forget₂_Ring_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ CommRing), category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ CommRing Ring)}}

@[protected, instance]

noncomputable def CommRing.forget₂_Ring_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget₂ CommRing Ring)

Equations

CommRing.forget₂_Ring_preserves_limits = CommRing.forget₂_Ring_preserves_limits_of_size

noncomputable def CommRing.forget₂_CommSemiRing_preserves_limits_aux {J : Type v} [category_theory.small_category J] (F : J ⥤ CommRing) :

category_theory.limits.is_limit ((category_theory.forget₂ CommRing CommSemiRing).map_cone (CommRing.limit_cone F))

An auxiliary declaration to speed up typechecking.

Equations

CommRing.forget₂_CommSemiRing_preserves_limits_aux F = CommSemiRing.limit_cone_is_limit (F ⋙ category_theory.forget₂ CommRing CommSemiRing)

@[protected, instance]

noncomputable def CommRing.forget₂_CommSemiRing_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget₂ CommRing CommSemiRing)

The forgetful functor from commutative rings to commutative semirings preserves all limits. (That is, the underlying commutative semirings could have been computed instead as limits in the category of commutative semirings.)

Equations

CommRing.forget₂_CommSemiRing_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ CommRing), category_theory.limits.preserves_limit_of_preserves_limit_cone (CommRing.limit_cone_is_limit F) (CommRing.forget₂_CommSemiRing_preserves_limits_aux F)}}

@[protected, instance]

noncomputable def CommRing.forget₂_CommSemiRing_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget₂ CommRing CommSemiRing)

Equations

CommRing.forget₂_CommSemiRing_preserves_limits = CommRing.forget₂_CommSemiRing_preserves_limits_of_size

@[protected, instance]

noncomputable def CommRing.forget_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget CommRing)

The forgetful functor from commutative rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations

CommRing.forget_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ CommRing), category_theory.limits.comp_preserves_limit (category_theory.forget₂ CommRing Ring) (category_theory.forget Ring)}}

@[protected, instance]

noncomputable def CommRing.forget_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget CommRing)

Equations

CommRing.forget_preserves_limits = CommRing.forget_preserves_limits_of_size