The category of (commutative) rings has all limits
Further, these limits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.
@[instance]
def
SemiRing.semiring_obj
{J : Type u}
[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 u}
[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.
@[instance]
Equations
def
SemiRing.limit_π_ring_hom
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ SemiRing)
(j : J) :
limit.π (F ⋙ forget SemiRing) j as a ring_hom.
Equations
- SemiRing.limit_π_ring_hom F j = {to_fun := category_theory.limits.limit.π (F ⋙ category_theory.forget SemiRing) j, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
def
SemiRing.has_limits.limit
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ SemiRing) :
Construction of a limit cone in SemiRing.
(Internal use only; use the limits API.)
Equations
- SemiRing.has_limits.limit F = {X := SemiRing.of (category_theory.limits.limit (F ⋙ category_theory.forget SemiRing)) (SemiRing.limit_semiring F), π := {app := SemiRing.limit_π_ring_hom F, naturality' := _}}
def
SemiRing.has_limits.limit_is_limit
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ SemiRing) :
Witness that the limit cone in SemiRing is a limit cone.
(Internal use only; use the limits API.)
Equations
- SemiRing.has_limits.limit_is_limit F = category_theory.limits.is_limit.of_faithful (category_theory.forget SemiRing) (category_theory.limits.limit.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' := _}) _
@[instance]
The category of rings has all limits.
Equations
- SemiRing.has_limits = {has_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ SemiRing), {cone := SemiRing.has_limits.limit F, is_limit := SemiRing.has_limits.limit_is_limit F}}}
def
SemiRing.forget₂_AddCommMon_preserves_limits_aux
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ SemiRing) :
An auxiliary declaration to speed up typechecking.
@[instance]
The forgetful functor from semirings to additive commutative monoids preserves all limits.
Equations
- SemiRing.forget₂_AddCommMon_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ SemiRing), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (SemiRing.forget₂_AddCommMon_preserves_limits_aux F)}}
def
SemiRing.forget₂_Mon_preserves_limits_aux
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ SemiRing) :
An auxiliary declaration to speed up typechecking.
@[instance]
The forgetful functor from semirings to monoids preserves all limits.
Equations
- SemiRing.forget₂_Mon_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ SemiRing), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (SemiRing.forget₂_Mon_preserves_limits_aux F)}}
@[instance]
The forgetful functor from semirings to types preserves all limits.
Equations
- SemiRing.forget_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ SemiRing), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget SemiRing))}}
@[instance]
def
CommSemiRing.comm_semiring_obj
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ CommSemiRing)
(j : J) :
Equations
- CommSemiRing.comm_semiring_obj F j = id (F.obj j).comm_semiring
@[instance]
def
CommSemiRing.limit_comm_semiring
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ CommSemiRing) :
@[instance]
def
CommSemiRing.category_theory.creates_limit
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ CommSemiRing) :
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.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.limit (F ⋙ category_theory.forget CommSemiRing)) (CommSemiRing.limit_comm_semiring F), π := {app := SemiRing.limit_π_ring_hom (F ⋙ category_theory.forget₂ CommSemiRing SemiRing), naturality' := _}}, valid_lift := (category_theory.limits.limit.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) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ CommSemiRing SemiRing)) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget SemiRing).map_cone ((category_theory.forget₂ CommSemiRing SemiRing).map_cone s)).X), ⟨λ (j : J), ((category_theory.forget SemiRing).map_cone ((category_theory.forget₂ CommSemiRing SemiRing).map_cone s)).π.app j v, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}) _})
@[instance]
The category of rings has all limits.
Equations
- CommSemiRing.has_limits = {has_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ CommSemiRing), category_theory.has_limit_of_created F (category_theory.forget₂ CommSemiRing SemiRing)}}
@[instance]
The forgetful functor from rings to semirings preserves all limits.
Equations
@[instance]
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 = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ CommSemiRing), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget CommSemiRing))}}
@[instance]
def
Ring.ring_obj
{J : Type u}
[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
@[instance]
Equations
- _ = _
@[instance]
Equations
- _ = _
@[instance]
Equations
@[instance]
Equations
@[instance]
def
Ring.category_theory.creates_limit
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Ring) :
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.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.limit (F ⋙ category_theory.forget Ring)) (Ring.limit_ring F), π := {app := SemiRing.limit_π_ring_hom (F ⋙ category_theory.forget₂ Ring SemiRing), naturality' := _}}, valid_lift := (category_theory.limits.limit.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) (category_theory.limits.limit.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' := _}) _})
@[instance]
The category of rings has all limits.
Equations
- Ring.has_limits = {has_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ Ring), category_theory.has_limit_of_created F (category_theory.forget₂ Ring SemiRing)}}
@[instance]
The forgetful functor from rings to semirings preserves all limits.
Equations
- Ring.forget₂_SemiRing_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ Ring), category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ Ring SemiRing)}}
def
Ring.forget₂_AddCommGroup_preserves_limits_aux
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Ring) :
An auxiliary declaration to speed up typechecking.
@[instance]
The forgetful functor from rings to additive commutative groups preserves all limits.
Equations
- Ring.forget₂_AddCommGroup_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ Ring), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (Ring.forget₂_AddCommGroup_preserves_limits_aux F)}}
@[instance]
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 = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ Ring), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget Ring))}}
@[instance]
def
CommRing.comm_ring_obj
{J : Type u}
[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
@[instance]
Equations
@[instance]
def
CommRing.category_theory.creates_limit
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ CommRing) :
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.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.limit (F ⋙ category_theory.forget CommRing)) (CommRing.limit_comm_ring F), π := {app := SemiRing.limit_π_ring_hom (F ⋙ category_theory.forget₂ CommRing Ring ⋙ category_theory.forget₂ Ring SemiRing), naturality' := _}}, valid_lift := (category_theory.limits.limit.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) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ CommRing Ring)) (λ (s : category_theory.limits.cone F), ((λ (s : category_theory.limits.cone (F ⋙ category_theory.forget₂ CommRing Ring)), ((λ (c' : category_theory.limits.cone ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing)) (t : category_theory.limits.is_limit c'), {to_liftable_cone := {lifted_cone := {X := Ring.of (category_theory.limits.limit ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget Ring)) (Ring.limit_ring (F ⋙ category_theory.forget₂ CommRing Ring)), π := {app := SemiRing.limit_π_ring_hom ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing), naturality' := _}}, valid_lift := (category_theory.limits.limit.is_limit ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing)).unique_up_to_iso t}, makes_limit := category_theory.limits.is_limit.of_faithful (category_theory.forget₂ Ring SemiRing) (category_theory.limits.limit.is_limit ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing)) (λ (s : category_theory.limits.cone (F ⋙ category_theory.forget₂ CommRing Ring)), {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' := _}) _}) ((category_theory.forget₂ Ring SemiRing).map_cone (category_theory.lift_limit (category_theory.limits.limit.is_limit ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing)))) ((category_theory.limits.limit.is_limit ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing)).of_iso_limit (category_theory.lifted_limit_maps_to_original (category_theory.limits.limit.is_limit ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing))).symm)).makes_limit.lift_cone_morphism s ≫ (category_theory.as_iso (((λ (c' : category_theory.limits.cone ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing)) (t : category_theory.limits.is_limit c'), {to_liftable_cone := {lifted_cone := {X := Ring.of (category_theory.limits.limit ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget Ring)) (Ring.limit_ring (F ⋙ category_theory.forget₂ CommRing Ring)), π := {app := SemiRing.limit_π_ring_hom ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing), naturality' := _}}, valid_lift := (category_theory.limits.limit.is_limit ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing)).unique_up_to_iso t}, makes_limit := category_theory.limits.is_limit.of_faithful (category_theory.forget₂ Ring SemiRing) (category_theory.limits.limit.is_limit ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing)) (λ (s : category_theory.limits.cone (F ⋙ category_theory.forget₂ CommRing Ring)), {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' := _}) _}) ((category_theory.forget₂ Ring SemiRing).map_cone (category_theory.lift_limit (category_theory.limits.limit.is_limit ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing)))) ((category_theory.limits.limit.is_limit ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing)).of_iso_limit (category_theory.lifted_limit_maps_to_original (category_theory.limits.limit.is_limit ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing))).symm)).makes_limit.lift_cone_morphism (category_theory.lift_limit (category_theory.limits.limit.is_limit ((F ⋙ category_theory.forget₂ CommRing Ring) ⋙ category_theory.forget₂ Ring SemiRing))))).symm.hom) ((category_theory.forget₂ CommRing Ring).map_cone s)).hom) _})
@[instance]
The category of commutative rings has all limits.
Equations
- CommRing.has_limits = {has_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ CommRing), category_theory.has_limit_of_created F (category_theory.forget₂ CommRing Ring)}}
@[instance]
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 = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ CommRing), category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ CommRing Ring)}}
@[instance]
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 = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ CommRing), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget CommRing))}}