Lean4
/-- Given a cocone `t` of `F`, the induced monoid homomorphism from the colimit to the cocone point.
As a function, this is simply given by the induced map of the corresponding cocone in `Type`.
The only thing left to see is that it is a monoid homomorphism.
-/
@[to_additive /-- Given a cocone `t` of `F`, the induced additive monoid homomorphism from the colimit
to the cocone point. As a function, this is simply given by the induced map of the
corresponding cocone in `Type`. The only thing left to see is that it is an additive monoid
homomorphism. -/
]
noncomputable def colimitDesc (t : Cocone F) : colimit.{v, u} F ⟶ t.pt :=
ofHom
{ toFun :=
(F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
map_one' := by
rw [colimit_one_eq F IsFiltered.nonempty.some]
exact MonoidHom.map_one _
map_mul' x
y := by
obtain ⟨i, x, rfl⟩ := x.mk_surjective
obtain ⟨j, y, rfl⟩ := y.mk_surjective
rw [colimit_mul_mk_eq F ⟨i, x⟩ ⟨j, y⟩ (max' i j) (IsFiltered.leftToMax i j) (IsFiltered.rightToMax i j)]
dsimp
rw [MonoidHom.map_mul, t.w_apply, t.w_apply]
rfl }
