English
The colimit of a filtered diagram in SemiRingCat is equipped with a semiring structure compatible with the colimit cocone.
Русский
Колимит диаграммы в SemiRingCat снабжен структурой полускольца, совместимой с кокон-колимита.
LaTeX
$$ColimitSemiring( F )$$
Lean4
instance colimitSemiring : Semiring.{max v u} <| R.{v, u} F :=
{ (R.{v, u} F).str,
AddCommMonCat.FilteredColimits.colimitAddCommMonoid.{v, u}
(F ⋙
forget₂ SemiRingCat
AddCommMonCat.{max v
u}) with
mul_zero := fun x => by
refine Quot.inductionOn x ?_; clear x; intro x
obtain ⟨j, x⟩ := x
erw [colimit_zero_eq _ j, colimit_mul_mk_eq _ ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j)]
rw [CategoryTheory.Functor.map_id]
dsimp
rw [mul_zero x]
rfl
zero_mul := fun x => by
refine Quot.inductionOn x ?_; clear x; intro x
obtain ⟨j, x⟩ := x
erw [colimit_zero_eq _ j, colimit_mul_mk_eq _ ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j)]
rw [CategoryTheory.Functor.map_id]
dsimp
rw [zero_mul x]
rfl
left_distrib := fun x y z => by
refine Quot.induction_on₃ x y z ?_; clear x y z; intro x y z
obtain ⟨j₁, x⟩ := x; obtain ⟨j₂, y⟩ := y; obtain ⟨j₃, z⟩ := z
let k := IsFiltered.max₃ j₁ j₂ j₃
let f := IsFiltered.firstToMax₃ j₁ j₂ j₃
let g := IsFiltered.secondToMax₃ j₁ j₂ j₃
let h := IsFiltered.thirdToMax₃ j₁ j₂ j₃
erw [colimit_add_mk_eq _ ⟨j₂, _⟩ ⟨j₃, _⟩ k g h, colimit_mul_mk_eq _ ⟨j₁, _⟩ ⟨k, _⟩ k f (𝟙 k),
colimit_mul_mk_eq _ ⟨j₁, _⟩ ⟨j₂, _⟩ k f g, colimit_mul_mk_eq _ ⟨j₁, _⟩ ⟨j₃, _⟩ k f h,
colimit_add_mk_eq _ ⟨k, _⟩ ⟨k, _⟩ k (𝟙 k) (𝟙 k)]
simp only [CategoryTheory.Functor.map_id]
erw [left_distrib (F.map f x) (F.map g y) (F.map h z)]
rfl
right_distrib := fun x y z => by
refine Quot.induction_on₃ x y z ?_; clear x y z; intro x y z
obtain ⟨j₁, x⟩ := x; obtain ⟨j₂, y⟩ := y; obtain ⟨j₃, z⟩ := z
let k := IsFiltered.max₃ j₁ j₂ j₃
let f := IsFiltered.firstToMax₃ j₁ j₂ j₃
let g := IsFiltered.secondToMax₃ j₁ j₂ j₃
let h := IsFiltered.thirdToMax₃ j₁ j₂ j₃
erw [colimit_add_mk_eq _ ⟨j₁, _⟩ ⟨j₂, _⟩ k f g, colimit_mul_mk_eq _ ⟨k, _⟩ ⟨j₃, _⟩ k (𝟙 k) h,
colimit_mul_mk_eq _ ⟨j₁, _⟩ ⟨j₃, _⟩ k f h, colimit_mul_mk_eq _ ⟨j₂, _⟩ ⟨j₃, _⟩ k g h,
colimit_add_mk_eq _ ⟨k, _⟩ ⟨k, _⟩ k (𝟙 k) (𝟙 k)]
simp only [CategoryTheory.Functor.map_id]
erw [right_distrib (F.map f x) (F.map g y) (F.map h z)]
rfl }
