English
The cone with apex at the product of the M-sequence and legs given by Pi maps provides a limit cone for the sequential product, i.e., the tower of products forms a limit diagram with apex ∏ M.
Русский
Конус с вершиной в произведении последовательности M и ножками, задаваемыми отображениями Pi, образует предел для последовательного произведения; башня произведений образует предел.
LaTeX
$$$\\text{cone } f: \\; \\text{pt} = \\prod^\\circ M, \\; \\pi_n = \\text{…}$ (limit cone)$$
Lean4
/-- The cone over the tower
```
⋯ → ∏_{n < m} M n × ∏_{n ≥ m} N n → ⋯ → ∏ N
```
with cone point `∏ M`. This is a limit cone, see `CategoryTheory.Limits.SequentialProduct.isLimit`.
-/
noncomputable def cone : Cone (Functor.ofOpSequence (functorMap f))
where
pt := ∏ᶜ M
π :=
by
refine
NatTrans.ofOpSequence
(fun n ↦
Limits.Pi.map fun m ↦
if h : m < n then eqToHom (functorObj_eq_pos h).symm else f m ≫ eqToHom (functorObj_eq_neg h).symm)
(fun n ↦ ?_)
apply Limits.Pi.hom_ext
intro m
simp only [Functor.const_obj_obj, Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.const_obj_map,
Category.id_comp, limMap_π, Discrete.functor_obj_eq_as, Discrete.natTrans_app,
Functor.ofOpSequence_map_homOfLE_succ, functorMap, Category.assoc, limMap_π_assoc]
split
· simp [dif_pos (by omega : m < n + 1)]
· split
all_goals simp
