Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products

Preserving products #

Constructions to relate the notions of preserving products and reflecting products to concrete fans.

In particular, we show that piComparison G f is an isomorphism iff G preserves the limit of f.

def CategoryTheory.Limits.isLimitMapConeFanMkEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) {P : C} (g : (j : J) → P f j) :
IsLimit (G.mapCone (Fan.mk P g)) IsLimit (Fan.mk (G.obj P) fun (j : J) => G.map (g j))

The map of a fan is a limit iff the fan consisting of the mapped morphisms is a limit. This essentially lets us commute Fan.mk with Functor.mapCone.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def CategoryTheory.Limits.isLimitFanMkObjOfIsLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) [PreservesLimit (Discrete.functor f) G] {P : C} (g : (j : J) → P f j) (t : IsLimit (Fan.mk P g)) :
    IsLimit (Fan.mk (G.obj P) fun (j : J) => G.map (g j))

    The property of preserving products expressed in terms of fans.

    Equations
    Instances For
      def CategoryTheory.Limits.isLimitOfIsLimitFanMkObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) [ReflectsLimit (Discrete.functor f) G] {P : C} (g : (j : J) → P f j) (t : IsLimit (Fan.mk (G.obj P) fun (j : J) => G.map (g j))) :

      The property of reflecting products expressed in terms of fans.

      Equations
      Instances For
        def CategoryTheory.Limits.isLimitOfHasProductOfPreservesLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) [HasProduct f] [PreservesLimit (Discrete.functor f) G] :
        IsLimit (Fan.mk (G.obj (∏ᶜ f)) fun (j : J) => G.map (Pi.π f j))

        If G preserves products and C has them, then the fan constructed of the mapped projection of a product is a limit.

        Equations
        Instances For
          theorem CategoryTheory.Limits.PreservesProduct.of_iso_comparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) [HasProduct f] [HasProduct fun (j : J) => G.obj (f j)] [i : IsIso (piComparison G f)] :

          If pi_comparison G f is an isomorphism, then G preserves the limit of f.

          def CategoryTheory.Limits.PreservesProduct.iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) [HasProduct f] [HasProduct fun (j : J) => G.obj (f j)] [PreservesLimit (Discrete.functor f) G] :
          G.obj (∏ᶜ f) ∏ᶜ fun (j : J) => G.obj (f j)

          If G preserves limits, we have an isomorphism from the image of a product to the product of the images.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.Limits.PreservesProduct.iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) [HasProduct f] [HasProduct fun (j : J) => G.obj (f j)] [PreservesLimit (Discrete.functor f) G] :
            (iso G f).hom = piComparison G f
            instance CategoryTheory.Limits.instIsIsoPiComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) [HasProduct f] [HasProduct fun (j : J) => G.obj (f j)] [PreservesLimit (Discrete.functor f) G] :
            def CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) {P : C} (g : (j : J) → f j P) :
            IsColimit (G.mapCocone (Cofan.mk P g)) IsColimit (Cofan.mk (G.obj P) fun (j : J) => G.map (g j))

            The map of a cofan is a colimit iff the cofan consisting of the mapped morphisms is a colimit. This essentially lets us commute Cofan.mk with Functor.mapCocone.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def CategoryTheory.Limits.isColimitCofanMkObjOfIsColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) [PreservesColimit (Discrete.functor f) G] {P : C} (g : (j : J) → f j P) (t : IsColimit (Cofan.mk P g)) :
              IsColimit (Cofan.mk (G.obj P) fun (j : J) => G.map (g j))

              The property of preserving coproducts expressed in terms of cofans.

              Equations
              Instances For
                def CategoryTheory.Limits.isColimitOfIsColimitCofanMkObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) [ReflectsColimit (Discrete.functor f) G] {P : C} (g : (j : J) → f j P) (t : IsColimit (Cofan.mk (G.obj P) fun (j : J) => G.map (g j))) :

                The property of reflecting coproducts expressed in terms of cofans.

                Equations
                Instances For

                  If G preserves coproducts and C has them, then the cofan constructed of the mapped inclusion of a coproduct is a colimit.

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

                    If sigma_comparison G f is an isomorphism, then G preserves the colimit of f.

                    def CategoryTheory.Limits.PreservesCoproduct.iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) [HasCoproduct f] [HasCoproduct fun (j : J) => G.obj (f j)] [PreservesColimit (Discrete.functor f) G] :
                    G.obj ( f) fun (j : J) => G.obj (f j)

                    If G preserves colimits, we have an isomorphism from the image of a coproduct to the coproduct of the images.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Limits.PreservesCoproduct.inv_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) [HasCoproduct f] [HasCoproduct fun (j : J) => G.obj (f j)] [PreservesColimit (Discrete.functor f) G] :
                      instance CategoryTheory.Limits.instIsIsoSigmaComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : JC) [HasCoproduct f] [HasCoproduct fun (j : J) => G.obj (f j)] [PreservesColimit (Discrete.functor f) G] :

                      If F preserves the limit of every Discrete.functor f, it preserves all limits of shape Discrete J.

                      If F preserves the colimit of every Discrete.functor f, it preserves all colimits of shape Discrete J.