Constructing finite products from binary products and terminal.

If a category has binary products and a terminal object then it has finite products. If a functor preserves binary products and the terminal object then it preserves finite products.

TODO

Provide the dual results. Show the analogous results for functors which reflect or create (co)limits.

@[simp]

theorem CategoryTheory.extendFan_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Fan fun i => f (Fin.succ i)) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) : (CategoryTheory.extendFan c₁ c₂).pt = c₂.pt

@[simp]

theorem CategoryTheory.extendFan_π_app {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Fan fun i => f (Fin.succ i)) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) : (CategoryTheory.extendFan c₁ c₂).π.app X = Fin.cases (CategoryTheory.Limits.BinaryFan.fst c₂) (fun i => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.snd c₂) (c₁.π.app { as := i })) X.as

def CategoryTheory.extendFan {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Fan fun i => f (Fin.succ i)) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) : CategoryTheory.Limits.Fan f

Given n+1 objects of C, a fan for the last n with point c₁.pt and a binary fan on c₁.pt and f 0, we can build a fan for all n+1.

In extendFanIsLimit we show that if the two given fans are limits, then this fan is also a limit.

def CategoryTheory.extendFanIsLimit {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Fan fun i => f (Fin.succ i)} {c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt} (t₁ : CategoryTheory.Limits.IsLimit c₁) (t₂ : CategoryTheory.Limits.IsLimit c₂) : CategoryTheory.Limits.IsLimit (CategoryTheory.extendFan c₁ c₂)

Show that if the two given fans in extendFan are limits, then the constructed fan is also a limit.

theorem CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasFiniteProducts C

If C has a terminal object and binary products, then it has finite products.

noncomputable def CategoryTheory.preservesFinOfPreservesBinaryAndTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F] [CategoryTheory.Limits.HasFiniteProducts C] (n : ℕ) (f : Fin n → C) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F

If F preserves the terminal object and binary products, then it preserves products indexed by Fin n for any n.

Equations

• One or more equations did not get rendered due to their size.
• CategoryTheory.preservesFinOfPreservesBinaryAndTerminal F 0 = fun f => inferInstance

def CategoryTheory.preservesShapeFinOfPreservesBinaryAndTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F] [CategoryTheory.Limits.HasFiniteProducts C] (n : ℕ) : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete (Fin n)) F

If F preserves the terminal object and binary products, then it preserves limits of shape Discrete (Fin n).

def CategoryTheory.preservesFiniteProductsOfPreservesBinaryAndTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F] [CategoryTheory.Limits.HasFiniteProducts C] (J : Type) [Fintype J] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F

If F preserves the terminal object and binary products then it preserves finite products.

@[simp]

theorem CategoryTheory.extendCofan_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Cofan fun i => f (Fin.succ i)) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) : (CategoryTheory.extendCofan c₁ c₂).pt = c₂.pt

@[simp]

theorem CategoryTheory.extendCofan_ι_app {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Cofan fun i => f (Fin.succ i)) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) : (CategoryTheory.extendCofan c₁ c₂).ι.app X = Fin.cases (CategoryTheory.Limits.BinaryCofan.inl c₂) (fun i => CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := i }) (CategoryTheory.Limits.BinaryCofan.inr c₂)) X.as

def CategoryTheory.extendCofan {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Cofan fun i => f (Fin.succ i)) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) : CategoryTheory.Limits.Cofan f

Given n+1 objects of C, a cofan for the last n with point c₁.pt and a binary cofan on c₁.X and f 0, we can build a cofan for all n+1.

In extendCofanIsColimit we show that if the two given cofans are colimits, then this cofan is also a colimit.

def CategoryTheory.extendCofanIsColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Cofan fun i => f (Fin.succ i)} {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt} (t₁ : CategoryTheory.Limits.IsColimit c₁) (t₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Limits.IsColimit (CategoryTheory.extendCofan c₁ c₂)

Show that if the two given cofans in extendCofan are colimits, then the constructed cofan is also a colimit.

theorem CategoryTheory.hasFiniteCoproducts_of_has_binary_and_initial {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasFiniteCoproducts C

If C has an initial object and binary coproducts, then it has finite coproducts.

noncomputable def CategoryTheory.preservesFinOfPreservesBinaryAndInitial {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) (f : Fin n → C) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) F

If F preserves the initial object and binary coproducts, then it preserves products indexed by Fin n for any n.

Equations

• One or more equations did not get rendered due to their size.
• CategoryTheory.preservesFinOfPreservesBinaryAndInitial F 0 = fun f => inferInstance

def CategoryTheory.preservesShapeFinOfPreservesBinaryAndInitial {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete (Fin n)) F

If F preserves the initial object and binary coproducts, then it preserves colimits of shape Discrete (Fin n).

def CategoryTheory.preservesFiniteCoproductsOfPreservesBinaryAndInitial {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F] [CategoryTheory.Limits.HasFiniteCoproducts C] (J : Type) [Fintype J] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F

If F preserves the initial object and binary coproducts then it preserves finite products.