Documentation

Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

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.

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

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

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

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

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

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

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

      source
      theorem CategoryTheory.Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) [PreservesLimitsOfShape (Discrete WalkingPair) F] [PreservesLimitsOfShape (Discrete PEmpty.{1}) F] [HasFiniteProducts C] :
      PreservesFiniteProducts F

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

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

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

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

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

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

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

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

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

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

          source
          theorem CategoryTheory.PreservesFiniteCoproducts.of_preserves_binary_and_initial {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) [Limits.PreservesColimitsOfShape (Discrete Limits.WalkingPair) F] [Limits.PreservesColimitsOfShape (Discrete PEmpty.{1}) F] [Limits.HasFiniteCoproducts C] (J : Type u_1) [Finite J] :
          Limits.PreservesColimitsOfShape (Discrete J) F

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

          source
          @[deprecated CategoryTheory.PreservesFiniteCoproducts.of_preserves_binary_and_initial (since := "2026-03-10")]
          theorem CategoryTheory.preservesFiniteCoproductsOfPreservesBinaryAndInitial {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) [Limits.PreservesColimitsOfShape (Discrete Limits.WalkingPair) F] [Limits.PreservesColimitsOfShape (Discrete PEmpty.{1}) F] [Limits.HasFiniteCoproducts C] (J : Type u_1) [Finite J] :
          Limits.PreservesColimitsOfShape (Discrete J) F

          Alias of CategoryTheory.PreservesFiniteCoproducts.of_preserves_binary_and_initial.

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