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

• SemiRing.filtered_colimits.colimit F = SemiRing.of ↥(SemiRing.filtered_colimits.R F)

Instances for ↥SemiRing.filtered_colimits.colimit

• CommSemiRing.filtered_colimits.colimit_comm_semiring
• Ring.filtered_colimits.colimit_ring

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

Equations

• SemiRing.filtered_colimits.forget_preserves_filtered_colimits = category_theory.limits.comp_preserves_filtered_colimits (category_theory.forget₂ SemiRing Mon) (category_theory.forget 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.

Equations

• CommSemiRing.filtered_colimits.colimit F = CommSemiRing.of ↥(CommSemiRing.filtered_colimits.R F)

The cocone over the proposed colimit commutative semiring.

Equations

• CommSemiRing.filtered_colimits.colimit_cocone F = {X := CommSemiRing.filtered_colimits.colimit F, ι := {app := (SemiRing.filtered_colimits.colimit_cocone (F ⋙ category_theory.forget₂ CommSemiRing SemiRing)).ι.app, naturality' := _}}

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

Equations

• CommSemiRing.filtered_colimits.forget_preserves_filtered_colimits = category_theory.limits.comp_preserves_filtered_colimits (category_theory.forget₂ CommSemiRing SemiRing) (category_theory.forget 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

• Ring.filtered_colimits.colimit F = Ring.of ↥(Ring.filtered_colimits.R F)

Instances for ↥Ring.filtered_colimits.colimit

• CommRing.filtered_colimits.colimit_comm_ring

The cocone over the proposed colimit ring.

Equations

• Ring.filtered_colimits.colimit_cocone F = {X := Ring.filtered_colimits.colimit F, ι := {app := (SemiRing.filtered_colimits.colimit_cocone (F ⋙ category_theory.forget₂ Ring SemiRing)).ι.app, naturality' := _}}

The proposed colimit cocone is a colimit in Ring.

Equations

• Ring.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₂ Ring SemiRing)).desc ((category_theory.forget₂ Ring SemiRing).map_cocone t), fac' := _, uniq' := _}

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

Equations

• Ring.filtered_colimits.forget_preserves_filtered_colimits = category_theory.limits.comp_preserves_filtered_colimits (category_theory.forget₂ Ring SemiRing) (category_theory.forget 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

• CommRing.filtered_colimits.colimit F = CommRing.of ↥(CommRing.filtered_colimits.R F)

The cocone over the proposed colimit commutative ring.

Equations

• CommRing.filtered_colimits.colimit_cocone F = {X := CommRing.filtered_colimits.colimit F, ι := {app := (Ring.filtered_colimits.colimit_cocone (F ⋙ category_theory.forget₂ CommRing Ring)).ι.app, naturality' := _}}

The proposed colimit cocone is a colimit in CommRing.

Equations

• CommRing.filtered_colimits.colimit_cocone_is_colimit F = {desc := λ (t : category_theory.limits.cocone F), (Ring.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ CommRing Ring)).desc ((category_theory.forget₂ CommRing Ring).map_cocone t), fac' := _, uniq' := _}

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

Equations

• CommRing.filtered_colimits.forget_preserves_filtered_colimits = category_theory.limits.comp_preserves_filtered_colimits (category_theory.forget₂ CommRing Ring) (category_theory.forget Ring)