English
Continuation of the Finset-based colimit cocone construction, detailing the structure of the cocone and its universal property.
Русский
Продолжение конструирования колимитного конуса на основе конечных множеств, детализация свойств косины и универсального свойства.
LaTeX
$$Continuation of liftToFinsetColimitCocone$$
Lean4
/-- If `C` has finite coproducts and filtered colimits, we can construct arbitrary coproducts by
taking the colimit of the diagram formed by the coproducts of finite sets over the indexing type. -/
@[simps!]
def liftToFinsetColimitCocone [HasColimitsOfShape (Finset (Discrete α)) C] (F : Discrete α ⥤ C) : ColimitCocone F
where
cocone :=
{ pt := colimit (liftToFinsetObj F)
ι :=
Discrete.natTrans fun j =>
Sigma.ι (fun x : ({ j } : Finset (Discrete α)) => F.obj x) ⟨j, by simp⟩ ≫
colimit.ι (liftToFinsetObj F) { j } }
isColimit :=
{ desc := fun s =>
colimit.desc (liftToFinsetObj F)
{ pt := s.pt
ι := { app := fun _ => Sigma.desc fun x => s.ι.app x } }
uniq := fun s m h => by
apply colimit.hom_ext
rintro t
dsimp [liftToFinsetObj]
apply colimit.hom_ext
rintro ⟨⟨j, hj⟩⟩
convert h j using 1
· simp [← colimit.w (liftToFinsetObj F) ⟨⟨Finset.singleton_subset_iff.2 hj⟩⟩]
rfl
· simp }
