ℕ-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) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasProductsOfShape ℕ C] : ℕ → C

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

Equations

• CategoryTheory.Limits.SequentialProduct.functorObj M N n = ∏ᶜ fun (m : ℕ) => if x : m < n then M m else N m

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

The transition maps in the sequential limit of products

Equations

• One or more equations did not get rendered due to their size.

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

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

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

noncomputable def CategoryTheory.Limits.SequentialProduct.cone {C : Type u_1} {M N : ℕ → C} [CategoryTheory.Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [CategoryTheory.Limits.HasProductsOfShape ℕ C] : CategoryTheory.Limits.Cone (CategoryTheory.Functor.ofOpSequence (CategoryTheory.Limits.SequentialProduct.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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

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

noncomputable def CategoryTheory.Limits.SequentialProduct.isLimit {C : Type u_1} {M N : ℕ → C} [CategoryTheory.Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [CategoryTheory.Limits.HasProductsOfShape ℕ C] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.SequentialProduct.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.

Equations

• One or more equations did not get rendered due to their size.

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