English
The cone constructed from finite subproducts is a limit cone; i.e., it satisfies the universal property of a limit with projection maps given by Pi.lift.
Русский
Умноженная на конечные подмножества конус образует предел; т.е. удовлетворяет универсальному свойству предела с отображениями проекций, заданными Pi.lift.
LaTeX
$$$$ \text{isLimitFiniteSubproductsCone}(f): \mathrm{IsLimit}(\mathrm{finiteSubproductsCone}\ f). $$$$
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 liftToFinsetLimitCone [HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C] (F : Discrete α ⥤ C) : LimitCone F
where
cone :=
{ pt := limit (liftToFinsetObj F)
π :=
Discrete.natTrans fun j =>
limit.π (liftToFinsetObj F) ⟨{ j }⟩ ≫ Pi.π _ (⟨j, by simp⟩ : ({ j } : Finset (Discrete α))) }
isLimit :=
{ lift := fun s =>
limit.lift (liftToFinsetObj F)
{ pt := s.pt
π := { app := fun _ => Pi.lift fun x => s.π.app x } }
uniq := fun s m h => by
apply limit.hom_ext
rintro t
dsimp [liftToFinsetObj]
apply limit.hom_ext
rintro ⟨⟨j, hj⟩⟩
convert h j using 1
· simp [← limit.w (liftToFinsetObj F) ⟨⟨⟨Finset.singleton_subset_iff.2 hj⟩⟩⟩]
rfl
· simp }
