English
The colimit M F carries a natural Monoid structure, with multiplication defined by colimitMul and unit by colimit_one; associativity and unit laws hold.
Русский
Коллимит M F естественным образом имеет структуру моноида: умножение задаётся через colimitMul, единица — через colimit_one; выполняются ассоциативность и тождественные законы.
LaTeX
$$$\text{Monoid}(M F) \quad$ with $\cdot$ defined by $\text{colimitMul}$ and $1$ by $\text{colimit_one}$; \\ (a\cdot b)\cdot c = a\cdot (b\cdot c),\quad 1\cdot a = a = a\cdot 1.$$$
Lean4
@[to_additive]
noncomputable instance colimitMonoid : Monoid (M.{v, u} F) :=
{ colimitMulOneClass F with
mul_assoc := fun x y z => by
obtain ⟨j₁, x₁, rfl⟩ := x.mk_surjective
obtain ⟨j₂, y₂, rfl⟩ := y.mk_surjective
obtain ⟨j₃, z₃, rfl⟩ := z.mk_surjective
obtain ⟨j, f₁, f₂, f₃, x, y, z, h₁, h₂, h₃⟩ :
∃ (j : J) (f₁ : j₁ ⟶ j) (f₂ : j₂ ⟶ j) (f₃ : j₃ ⟶ j) (x y z : F.obj j),
F.map f₁ x₁ = x ∧ F.map f₂ y₂ = y ∧ F.map f₃ z₃ = z :=
⟨IsFiltered.max₃ j₁ j₂ j₃, IsFiltered.firstToMax₃ _ _ _, IsFiltered.secondToMax₃ _ _ _,
IsFiltered.thirdToMax₃ _ _ _, _, _, _, rfl, rfl, rfl⟩
simp only [← M.map_mk F f₁, ← M.map_mk F f₂, ← M.map_mk F f₃, h₁, h₂, h₃, colimit_mul_mk_eq', mul_assoc] }
