Documentation

Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Products in the over category #

Shows that products in the over category can be derived from wide pullbacks in the base category. The main result is over_product_of_widePullback, which says that if C has J-indexed wide pullbacks, then Over B has J-indexed products.

Note that the binary case is done separately to ensure defeqs with the pullback in the base category.

TODO #

Binary products #

In this section we construct binary products in Over X and binary coproducts in Under X explicitly as the pullbacks and pushouts of binary (co)fans in the base category.

For Over X, one could construct these binary products from the general theory of arbitrary products from the next section, ie

(Cones.postcomposeEquivalence (diagramIsoCospan _).symm).trans
  (Over.ConstructProducts.conesEquiv _ (pair (Over.mk f) (Over.mk g)))

but this gives worse defeqs.

For Under X, there is currently no general theory of arbitrary coproducts.

Pullback cones to X are the same thing as binary fans in Over X.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_map_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y X} {g : Z X} {c₁ c₂ : PullbackCone f g} (a : c₁ c₂) :
    @[simp]
    theorem CategoryTheory.Limits.pullbackConeEquivBinaryFan_counitIso {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y X} {g : Z X} :
    pullbackConeEquivBinaryFan.counitIso = NatIso.ofComponents (fun (X_1 : BinaryFan (Over.mk f) (Over.mk g)) => BinaryFan.ext (Over.isoMk (Iso.refl (({ obj := fun (c : BinaryFan (Over.mk f) (Over.mk g)) => PullbackCone.mk c.fst.left c.snd.left , map := fun {c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)} (a : c₁ c₂) => { hom := a.hom.left, w := }, map_id := , map_comp := }.comp { obj := fun (c : PullbackCone f g) => BinaryFan.mk (Over.homMk c.fst ) (Over.homMk c.snd ), map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ c₂) => { hom := Over.homMk a.hom , w := }, map_id := , map_comp := }).obj X_1).pt.left) ) )
    @[simp]
    theorem CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_map_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : Y X} {g : Z X} {c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)} (a : c₁ c₂) :

    A binary fan in Over X is a limit if its corresponding pullback cone to X is a limit.

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

      A pullback cone to X is a limit if its corresponding binary fan in Over X is a limit.

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

        Pushout cocones from X are the same thing as binary cofans in Under X.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_counitIso {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X Y} {g : X Z} :
          pushoutCoconeEquivBinaryCofan.counitIso = NatIso.ofComponents (fun (X_1 : BinaryCofan (Under.mk f) (Under.mk g)) => BinaryCofan.ext (Under.isoMk (Iso.refl (({ obj := fun (c : BinaryCofan (Under.mk f) (Under.mk g)) => PushoutCocone.mk c.inl.right c.inr.right , map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ c₂) => { hom := a.hom.right, w := }, map_id := , map_comp := }.comp { obj := fun (c : PushoutCocone f g) => BinaryCofan.mk (Under.homMk c.inl ) (Under.homMk c.inr ), map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ c₂) => { hom := Under.homMk a.hom , w := }, map_id := , map_comp := }).obj X_1).pt.right) ) )
          @[simp]
          @[simp]
          theorem CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_map_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X Y} {g : X Z} {c₁ c₂ : PushoutCocone f g} (a : c₁ c₂) :

          A binary cofan in Under X is a colimit if its corresponding pushout cocone from X is a colimit.

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

            A pushout cocone from X is a colimit if its corresponding binary cofan in Under X is a colimit.

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

              The product of Y and Z in Over X is isomorpic to Y ×ₓ Z.

              Equations
              Instances For

                Arbitrary products #

                In this section, we prove that J-indexed products in Over X correspond to J-indexed pullbacks in C.

                @[reducible, inline]

                (Implementation) Given a product diagram in C/B, construct the corresponding wide pullback diagram in C.

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

                  (Impl) A preliminary definition to avoid timeouts.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]

                    (Impl) A preliminary definition to avoid timeouts.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Over.ConstructProducts.conesEquivInverse_map_hom {C : Type u} [Category.{v, u} C] (B : C) {J : Type w} (F : Functor (Discrete J) (Over B)) {X✝ Y✝ : Limits.Cone F} (f : X✝ Y✝) :

                      (Impl) A preliminary definition to avoid timeouts.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        @[simp]
                        theorem CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_π_app {C : Type u} [Category.{v, u} C] (B : C) {J : Type w} (F : Functor (Discrete J) (Over B)) (c : Limits.Cone (widePullbackDiagramOfDiagramOver B F)) (x✝ : Discrete J) :
                        ((conesEquivFunctor B F).obj c).π.app x✝ = match x✝ with | { as := j } => homMk (c.π.app (some j))

                        (Impl) A preliminary definition to avoid timeouts.

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

                          (Impl) A preliminary definition to avoid timeouts.

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

                            (Impl) Establish an equivalence between the category of cones for F and for the "grown" F.

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

                              Given a pullback in C, construct a binary product in C/B.

                              Given all wide pullbacks in C, construct products in C/B.

                              Given all finite wide pullbacks in C, construct finite products in C/B.

                              Construct terminal object in the over category. This isn't an instance as it's not typically the way we want to define terminal objects. (For instance, this gives a terminal object which is different from the generic one given by over_product_of_widePullback above.)