ℕ-indexed products as sequential limits

Given sequences M N : ℕ → C of objects with morphisms f n : M n ⟶ N n for all n, this file exhibits ∏ M as the limit of the tower

⋯ → ∏_{n < m + 1} M n × ∏_{n ≥ m + 1} N n → ∏_{n < m} M n × ∏_{n ≥ m} N n → ⋯ → ∏ N

Further, we prove that the transition maps in this tower are epimorphisms, in the case when each f n is an epimorphism and C has finite biproducts.

theorem CategoryTheory.Limits.SequentialProduct.functorObj_eq_pos {C : Type u_1} {M N : ℕ → C} {n m : ℕ} (h : m < n) : (fun (i : ℕ) => if x : i < n then M i else N i) m = M m

theorem CategoryTheory.Limits.SequentialProduct.functorObj_eq_neg {C : Type u_1} {M N : ℕ → C} {n m : ℕ} (h : ¬m < n) : (fun (i : ℕ) => if x : i < n then M i else N i) m = N m

noncomputable def CategoryTheory.Limits.SequentialProduct.functorObj {C : Type u_1} (M N : ℕ → C) [Category.{u_2, u_1} C] [HasProductsOfShape ℕ C] : ℕ → C

The product of the m first objects of M and the rest of the rest of N

noncomputable def CategoryTheory.Limits.SequentialProduct.functorObjProj_pos {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] [HasProductsOfShape ℕ C] (n m : ℕ) (h : m < n) : functorObj M N n ⟶ M m

The projection map from functorObj M N n to M m, when m < n

noncomputable def CategoryTheory.Limits.SequentialProduct.functorObjProj_neg {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] [HasProductsOfShape ℕ C] (n m : ℕ) (h : ¬m < n) : functorObj M N n ⟶ N m

The projection map from functorObj M N n to N m, when m ≥ n

noncomputable def CategoryTheory.Limits.SequentialProduct.functorMap {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [HasProductsOfShape ℕ C] (n : ℕ) : functorObj M N (n + 1) ⟶ functorObj M N n

The transition maps in the sequential limit of products

theorem CategoryTheory.Limits.SequentialProduct.functorMap_commSq_succ {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [HasProductsOfShape ℕ C] (n : ℕ) : CategoryStruct.comp ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op) (CategoryStruct.comp (Pi.π (fun (m : ℕ) => if x : m < Opposite.unop (Opposite.op n) then M m else N m) n) (eqToHom ⋯)) = CategoryStruct.comp (Pi.π (fun (i : ℕ) => if x : i < n + 1 then M i else N i) n) (CategoryStruct.comp (eqToHom ⋯) (f n))

theorem CategoryTheory.Limits.SequentialProduct.functorMap_commSq_aux {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [HasProductsOfShape ℕ C] {n m k : ℕ} (h : n ≤ m) (hh : ¬k < m) : CategoryStruct.comp ((Functor.ofOpSequence (functorMap f)).map (homOfLE h).op) (CategoryStruct.comp (Pi.π (fun (m : ℕ) => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k) (eqToHom ⋯)) = CategoryStruct.comp (Pi.π (fun (i : ℕ) => if x : i < m then M i else N i) k) (eqToHom ⋯)

theorem CategoryTheory.Limits.SequentialProduct.functorMap_commSq {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [HasProductsOfShape ℕ C] {n m : ℕ} (h : ¬m < n) : CategoryStruct.comp ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op) (CategoryStruct.comp (Pi.π (fun (m : ℕ) => if x : m < Opposite.unop (Opposite.op n) then M m else N m) m) (eqToHom ⋯)) = CategoryStruct.comp (Pi.π (fun (i : ℕ) => if x : i < m + 1 then M i else N i) m) (CategoryStruct.comp (eqToHom ⋯) (f m))

noncomputable def CategoryTheory.Limits.SequentialProduct.cone {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [HasProductsOfShape ℕ C] : Cone (Functor.ofOpSequence (functorMap f))

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.

theorem CategoryTheory.Limits.SequentialProduct.cone_π_app {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [HasProductsOfShape ℕ C] (n : ℕ) : (cone f).π.app (Opposite.op n) = Pi.map fun (m : ℕ) => if h : m < n then eqToHom ⋯ else CategoryStruct.comp (f m) (eqToHom ⋯)

theorem CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [HasProductsOfShape ℕ C] (m n : ℕ) (h : n < m) : CategoryStruct.comp ((cone f).π.app (Opposite.op m)) (Pi.π (fun (i : ℕ) => if x : i < m then M i else N i) n) = CategoryStruct.comp (Pi.π M n) (eqToHom ⋯)

theorem CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos_assoc {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [HasProductsOfShape ℕ C] (m n : ℕ) (h : n < m) {Z : C} (h✝ : (if x : n < m then M n else N n) ⟶ Z) : CategoryStruct.comp ((cone f).π.app (Opposite.op m)) (CategoryStruct.comp (Pi.π (fun (i : ℕ) => if x : i < m then M i else N i) n) h✝) = CategoryStruct.comp (Pi.π M n) (CategoryStruct.comp (eqToHom ⋯) h✝)

theorem CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [HasProductsOfShape ℕ C] (m n : ℕ) (h : ¬n < m) : CategoryStruct.comp ((cone f).π.app (Opposite.op m)) (Pi.π (fun (m_1 : ℕ) => if x : m_1 < Opposite.unop (Opposite.op m) then M m_1 else N m_1) n) = CategoryStruct.comp (Pi.π M n) (CategoryStruct.comp (f n) (eqToHom ⋯))

theorem CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg_assoc {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [HasProductsOfShape ℕ C] (m n : ℕ) (h : ¬n < m) {Z : C} (h✝ : (if x : n < m then M n else N n) ⟶ Z) : CategoryStruct.comp ((cone f).π.app (Opposite.op m)) (CategoryStruct.comp (Pi.π (fun (m_1 : ℕ) => if x : m_1 < m then M m_1 else N m_1) n) h✝) = CategoryStruct.comp (Pi.π M n) (CategoryStruct.comp (f n) (CategoryStruct.comp (eqToHom ⋯) h✝))

noncomputable def CategoryTheory.Limits.SequentialProduct.isLimit {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [HasProductsOfShape ℕ C] : IsLimit (cone f)

The cone over the tower

⋯ → ∏_{n < m} M n × ∏_{n ≥ m} N n → ⋯ → ∏ N

with cone point ∏ M is indeed a limit cone.

theorem CategoryTheory.Limits.SequentialProduct.functorMap_epi {C : Type u_1} {M N : ℕ → C} [Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [HasProductsOfShape ℕ C] [HasZeroMorphisms C] [HasFiniteBiproducts C] [HasCountableProducts C] [∀ (n : ℕ), Epi (f n)] (n : ℕ) : Epi (functorMap f n)