The forgetful functor from (commutative) (semi-) rings preserves filtered colimits. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend to preserve filtered colimits.
In this file, we start with a small filtered category J
and a functor F : J ⥤ SemiRing
.
We show that the colimit of F ⋙ forget₂ SemiRing Mon
(in Mon
) carries the structure of a
semiring, thereby showing that the forgetful functor forget₂ SemiRing Mon
preserves filtered
colimits. In particular, this implies that forget SemiRing
preserves filtered colimits.
Similarly for CommSemiRing
, Ring
and CommRing
.
The colimit of F ⋙ forget₂ SemiRing Mon
in the category Mon
.
In the following, we will show that this has the structure of a semiring.
Equations
- SemiRing.filtered_colimits.colimit_semiring F = {add := add_comm_monoid.add (AddCommMon.filtered_colimits.colimit_add_comm_monoid (F ⋙ category_theory.forget₂ SemiRing AddCommMon)), add_assoc := _, zero := add_comm_monoid.zero (AddCommMon.filtered_colimits.colimit_add_comm_monoid (F ⋙ category_theory.forget₂ SemiRing AddCommMon)), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (AddCommMon.filtered_colimits.colimit_add_comm_monoid (F ⋙ category_theory.forget₂ SemiRing AddCommMon)), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := monoid.mul (SemiRing.filtered_colimits.R F).monoid, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := monoid.one (SemiRing.filtered_colimits.R F).monoid, one_mul := _, mul_one := _, nat_cast := non_assoc_semiring.nat_cast._default monoid.one add_comm_monoid.add _ add_comm_monoid.zero _ _ add_comm_monoid.nsmul _ _, nat_cast_zero := _, nat_cast_succ := _, npow := monoid.npow (SemiRing.filtered_colimits.R F).monoid, npow_zero' := _, npow_succ' := _}
The bundled semiring giving the filtered colimit of a diagram.
Equations
Instances for ↥SemiRing.filtered_colimits.colimit
The cocone over the proposed colimit semiring.
Equations
- SemiRing.filtered_colimits.colimit_cocone F = {X := SemiRing.filtered_colimits.colimit F _inst_2, ι := {app := λ (j : J), {to_fun := ((Mon.filtered_colimits.colimit_cocone (F ⋙ category_theory.forget₂ SemiRing Mon)).ι.app j).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, naturality' := _}}
The proposed colimit cocone is a colimit in SemiRing
.
Equations
- SemiRing.filtered_colimits.colimit_cocone_is_colimit F = {desc := λ (t : category_theory.limits.cocone F), {to_fun := ((Mon.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ SemiRing Mon)).desc ((category_theory.forget₂ SemiRing Mon).map_cocone t)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, fac' := _, uniq' := _}
Equations
- SemiRing.filtered_colimits.forget₂_Mon_preserves_filtered_colimits = {preserves_filtered_colimits := λ (J : Type u) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), {preserves_colimit := λ (F : J ⥤ SemiRing), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (SemiRing.filtered_colimits.colimit_cocone_is_colimit F) (Mon.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ SemiRing Mon))}}
The colimit of F ⋙ forget₂ CommSemiRing SemiRing
in the category SemiRing
.
In the following, we will show that this has the structure of a commutative semiring.
Equations
- CommSemiRing.filtered_colimits.colimit_comm_semiring F = {add := semiring.add (CommSemiRing.filtered_colimits.R F).semiring, add_assoc := _, zero := semiring.zero (CommSemiRing.filtered_colimits.R F).semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul (CommSemiRing.filtered_colimits.R F).semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul (CommSemiRing.filtered_colimits.R F).semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one (CommSemiRing.filtered_colimits.R F).semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast (CommSemiRing.filtered_colimits.R F).semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow (CommSemiRing.filtered_colimits.R F).semiring, npow_zero' := _, npow_succ' := _, mul_comm := _}
The bundled commutative semiring giving the filtered colimit of a diagram.
The cocone over the proposed colimit commutative semiring.
Equations
The proposed colimit cocone is a colimit in CommSemiRing
.
Equations
- CommSemiRing.filtered_colimits.colimit_cocone_is_colimit F = {desc := λ (t : category_theory.limits.cocone F), (SemiRing.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ CommSemiRing SemiRing)).desc ((category_theory.forget₂ CommSemiRing SemiRing).map_cocone t), fac' := _, uniq' := _}
Equations
- CommSemiRing.filtered_colimits.forget₂_SemiRing_preserves_filtered_colimits = {preserves_filtered_colimits := λ (J : Type u) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), {preserves_colimit := λ (F : J ⥤ CommSemiRing), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (CommSemiRing.filtered_colimits.colimit_cocone_is_colimit F) (SemiRing.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ CommSemiRing SemiRing))}}
The colimit of F ⋙ forget₂ Ring SemiRing
in the category SemiRing
.
In the following, we will show that this has the structure of a ring.
Equations
- Ring.filtered_colimits.colimit_ring F = {add := semiring.add (Ring.filtered_colimits.R F).semiring, add_assoc := _, zero := semiring.zero (Ring.filtered_colimits.R F).semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul (Ring.filtered_colimits.R F).semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (AddCommGroup.filtered_colimits.colimit_add_comm_group (F ⋙ category_theory.forget₂ Ring AddCommGroup)), sub := add_comm_group.sub (AddCommGroup.filtered_colimits.colimit_add_comm_group (F ⋙ category_theory.forget₂ Ring AddCommGroup)), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (AddCommGroup.filtered_colimits.colimit_add_comm_group (F ⋙ category_theory.forget₂ Ring AddCommGroup)), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_comm_group_with_one.int_cast._default semiring.nat_cast semiring.add _ semiring.zero _ _ semiring.nsmul _ _ semiring.one _ _ add_comm_group.neg add_comm_group.sub _ add_comm_group.zsmul _ _ _ _, nat_cast := semiring.nat_cast (Ring.filtered_colimits.R F).semiring, one := semiring.one (Ring.filtered_colimits.R F).semiring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := semiring.mul (Ring.filtered_colimits.R F).semiring, mul_assoc := _, one_mul := _, mul_one := _, npow := semiring.npow (Ring.filtered_colimits.R F).semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
The bundled ring giving the filtered colimit of a diagram.
Equations
Instances for ↥Ring.filtered_colimits.colimit
The cocone over the proposed colimit ring.
Equations
The proposed colimit cocone is a colimit in Ring
.
Equations
Equations
- Ring.filtered_colimits.forget₂_SemiRing_preserves_filtered_colimits = {preserves_filtered_colimits := λ (J : Type u) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), {preserves_colimit := λ (F : J ⥤ Ring), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (Ring.filtered_colimits.colimit_cocone_is_colimit F) (SemiRing.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ Ring SemiRing))}}
The colimit of F ⋙ forget₂ CommRing Ring
in the category Ring
.
In the following, we will show that this has the structure of a commutative ring.
Equations
- CommRing.filtered_colimits.colimit_comm_ring F = {add := ring.add (CommRing.filtered_colimits.R F).ring, add_assoc := _, zero := ring.zero (CommRing.filtered_colimits.R F).ring, zero_add := _, add_zero := _, nsmul := ring.nsmul (CommRing.filtered_colimits.R F).ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (CommRing.filtered_colimits.R F).ring, sub := ring.sub (CommRing.filtered_colimits.R F).ring, sub_eq_add_neg := _, zsmul := ring.zsmul (CommRing.filtered_colimits.R F).ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (CommRing.filtered_colimits.R F).ring, nat_cast := ring.nat_cast (CommRing.filtered_colimits.R F).ring, one := ring.one (CommRing.filtered_colimits.R F).ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul (CommRing.filtered_colimits.R F).ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow (CommRing.filtered_colimits.R F).ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
The bundled commutative ring giving the filtered colimit of a diagram.
Equations
The cocone over the proposed colimit commutative ring.
Equations
The proposed colimit cocone is a colimit in CommRing
.
Equations
Equations
- CommRing.filtered_colimits.forget₂_Ring_preserves_filtered_colimits = {preserves_filtered_colimits := λ (J : Type u) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), {preserves_colimit := λ (F : J ⥤ CommRing), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (CommRing.filtered_colimits.colimit_cocone_is_colimit F) (Ring.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ CommRing Ring))}}