English
The cone constructed from the sequential product is a limit cone for the tower of products, providing a universal property characterizing the limit of the diagram of products with tail substitutions.
Русский
Конус, построенный из последовательного произведения, является пределом для башенной схемы произведений, удовлетворяя универсальному свойству предела диаграммы произведений с хвостовыми заменами.
LaTeX
$$$\\text{IsLimit}(\\text{cone } f)$$$
Lean4
/-- The cone over the tower
```
⋯ → ∏_{n < m} M n × ∏_{n ≥ m} N n → ⋯ → ∏ N
```
with cone point `∏ M` is indeed a limit cone.
-/
noncomputable def isLimit : IsLimit (cone f)
where
lift
s :=
Pi.lift fun m ↦
s.π.app ⟨m + 1⟩ ≫ Pi.π (fun i ↦ if _ : i < m + 1 then M i else N i) m ≫ eqToHom (dif_pos (by omega : m < m + 1))
fac
s := by
intro ⟨n⟩
apply Pi.hom_ext
intro m
by_cases h : m < n
· simp only [Category.assoc, cone_π_app_comp_Pi_π_pos f _ _ h]
simp only [dite_eq_ite, Functor.ofOpSequence_obj, limit.lift_π_assoc, Fan.mk_pt, Discrete.functor_obj_eq_as,
Fan.mk_π_app, Category.assoc, eqToHom_trans]
have hh : m + 1 ≤ n := by omega
rw [← s.w (homOfLE hh).op]
simp only [Functor.const_obj_obj, Functor.ofOpSequence_obj, homOfLE_leOfHom, Category.assoc]
congr
induction hh using Nat.leRec with
| refl => simp
| @le_succ_of_le n hh
ih =>
have : homOfLE (Nat.le_succ_of_le hh) = homOfLE hh ≫ homOfLE (Nat.le_succ n) := by simp
rw [this, op_comp, Functor.map_comp]
simp only [Functor.ofOpSequence_obj, Nat.succ_eq_add_one, homOfLE_leOfHom,
Functor.ofOpSequence_map_homOfLE_succ, Category.assoc]
have h₁ : (if _ : m < m + 1 then M m else N m) = if _ : m < n then M m else N m := by
rw [dif_pos (by omega), dif_pos (by omega)]
have h₂ : (if _ : m < n then M m else N m) = if _ : m < n + 1 then M m else N m := by
rw [dif_pos h, dif_pos (by omega)]
rw [← eqToHom_trans h₁ h₂]
slice_lhs 2 4 => rw [ih (by omega)]
simp only [functorMap, dite_eq_ite, Pi.π, limMap_π_assoc, Discrete.functor_obj_eq_as, Discrete.natTrans_app]
split_ifs
rw [dif_pos (by omega)]
simp
· simp only [Category.assoc]
rw [cone_π_app_comp_Pi_π_neg f _ _ h]
simp only [dite_eq_ite, Functor.ofOpSequence_obj, limit.lift_π_assoc, Fan.mk_pt, Discrete.functor_obj_eq_as,
Fan.mk_π_app, Category.assoc]
slice_lhs 2 4 => erw [← functorMap_commSq f h]
simp
uniq s m
h := by
apply Pi.hom_ext
intro n
simp only [Functor.ofOpSequence_obj, dite_eq_ite, limit.lift_π, Fan.mk_pt, Fan.mk_π_app, ← h ⟨n + 1⟩,
Category.assoc]
slice_rhs 2 3 => erw [cone_π_app_comp_Pi_π_pos f (n + 1) _ (by omega)]
simp
