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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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 : Fin n) => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) :
    (CategoryTheory.extendFan c₁ c₂).pt = c₂.pt
    source
    @[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 : Fin n) => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) :
    (CategoryTheory.extendFan c₁ c₂).π.app X = Fin.cases c₂.fst (fun (i : Fin n) => CategoryTheory.CategoryStruct.comp c₂.snd (c₁.π.app { as := i })) X.as
    source
    def CategoryTheory.extendFanIsLimit {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Fan fun (i : Fin n) => f i.succ} {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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      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.

      source
      theorem 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.

      source
      theorem CategoryTheory.preservesShape_fin_of_preserves_binary_and_terminal {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).

      source
      theorem CategoryTheory.preservesFiniteProducts_of_preserves_binary_and_terminal {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 u_1) [Fintype J] :
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F

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

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[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 : Fin n) => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) :
        (CategoryTheory.extendCofan c₁ c₂).pt = c₂.pt
        source
        @[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 : Fin n) => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) :
        (CategoryTheory.extendCofan c₁ c₂).ι.app X = Fin.cases c₂.inl (fun (i : Fin n) => CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := i }) c₂.inr) X.as
        source
        def CategoryTheory.extendCofanIsColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Cofan fun (i : Fin n) => f i.succ} {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.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          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.

          source
          theorem CategoryTheory.preserves_fin_of_preserves_binary_and_initial {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.

          source
          theorem CategoryTheory.preservesShape_fin_of_preserves_binary_and_initial {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).

          source
          theorem 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 u_1) [Fintype J] :
          CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F

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