Documentation

Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Wide pullbacks #

We define the category WidePullbackShape, (resp. WidePushoutShape) which is the category obtained from a discrete category of type J by adjoining a terminal (resp. initial) element. Limits of this shape are wide pullbacks (pushouts). The convenience method wideCospan (wideSpan) constructs a functor from this category, hitting the given morphisms.

We use WidePullbackShape to define ordinary pullbacks (pushouts) by using J := WalkingPair, which allows easy proofs of some related lemmas. Furthermore, wide pullbacks are used to show the existence of limits in the slice category. Namely, if C has wide pullbacks then C/B has limits for any object B in C.

Typeclasses HasWidePullbacks and HasFiniteWidePullbacks assert the existence of wide pullbacks and finite wide pullbacks.

A wide pullback shape for any type J can be written simply as Option J.

Equations
Instances For

    A wide pushout shape for any type J can be written simply as Option J.

    Equations
    Instances For

      The type of arrows for the shape indexing a wide pullback.

      Instances For
        Equations
        • CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom = CategoryTheory.Limits.WidePullbackShape.decEqHom✝
        Equations
        • One or more equations did not get rendered due to their size.
        Equations

        An aesop tactic for bulk cases on morphisms in WidePushoutShape

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • CategoryTheory.Limits.WidePullbackShape.category = CategoryTheory.thin_category
          @[simp]
          theorem CategoryTheory.Limits.WidePullbackShape.wideCospan_map {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : JC) (arrows : (j : J) → objs j B) :
          ∀ {X Y : CategoryTheory.Limits.WidePullbackShape J} (f : X Y), (CategoryTheory.Limits.WidePullbackShape.wideCospan B objs arrows).map f = CategoryTheory.Limits.WidePullbackShape.Hom.casesOn (motive := fun (a a_1 : CategoryTheory.Limits.WidePullbackShape J) (t : a.Hom a_1) => X = aY = a_1HEq f t((fun (j : CategoryTheory.Limits.WidePullbackShape J) => Option.casesOn j B objs) X (fun (j : CategoryTheory.Limits.WidePullbackShape J) => Option.casesOn j B objs) Y)) f (fun (X_1 : CategoryTheory.Limits.WidePullbackShape J) (h : X = X_1) => Eq.ndrec (motive := fun (X_2 : CategoryTheory.Limits.WidePullbackShape J) => Y = X_2HEq f (CategoryTheory.Limits.WidePullbackShape.Hom.id X_2)((fun (j : CategoryTheory.Limits.WidePullbackShape J) => Option.casesOn j B objs) X (fun (j : CategoryTheory.Limits.WidePullbackShape J) => Option.casesOn j B objs) Y)) (fun (h : Y = X) => Eq.ndrec (motive := fun {Y : CategoryTheory.Limits.WidePullbackShape J} => (f : X Y) → HEq f (CategoryTheory.Limits.WidePullbackShape.Hom.id X)((fun (j : CategoryTheory.Limits.WidePullbackShape J) => Option.casesOn j B objs) X (fun (j : CategoryTheory.Limits.WidePullbackShape J) => Option.casesOn j B objs) Y)) (fun (f : X X) (h : HEq f (CategoryTheory.Limits.WidePullbackShape.Hom.id X)) => CategoryTheory.CategoryStruct.id ((fun (j : CategoryTheory.Limits.WidePullbackShape J) => Option.casesOn j B objs) X)) f) h) (fun (j : J) (h : X = some j) => Eq.ndrec (motive := fun {X : CategoryTheory.Limits.WidePullbackShape J} => (f : X Y) → Y = noneHEq f (CategoryTheory.Limits.WidePullbackShape.Hom.term j)((fun (j : CategoryTheory.Limits.WidePullbackShape J) => Option.casesOn j B objs) X (fun (j : CategoryTheory.Limits.WidePullbackShape J) => Option.casesOn j B objs) Y)) (fun (f : some j Y) (h : Y = none) => Eq.ndrec (motive := fun {Y : CategoryTheory.Limits.WidePullbackShape J} => (f : some j Y) → HEq f (CategoryTheory.Limits.WidePullbackShape.Hom.term j)((fun (j : CategoryTheory.Limits.WidePullbackShape J) => Option.casesOn j B objs) (some j) (fun (j : CategoryTheory.Limits.WidePullbackShape J) => Option.casesOn j B objs) Y)) (fun (f : some j none) (h : HEq f (CategoryTheory.Limits.WidePullbackShape.Hom.term j)) => arrows j) f) f)
          @[simp]
          theorem CategoryTheory.Limits.WidePullbackShape.wideCospan_obj {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : JC) (arrows : (j : J) → objs j B) (j : CategoryTheory.Limits.WidePullbackShape J) :

          Construct a functor out of the wide pullback shape given a J-indexed collection of arrows to a fixed object.

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

            Construct a cone over a wide cospan.

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

              Wide pullback diagrams of equivalent index types are equivalent.

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

                Lifting universe and morphism levels preserves wide pullback diagrams.

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

                  The type of arrows for the shape indexing a wide pushout.

                  Instances For
                    Equations
                    • CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom = CategoryTheory.Limits.WidePushoutShape.decEqHom✝
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Equations

                    An aesop tactic for bulk cases on morphisms in WidePushoutShape

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • CategoryTheory.Limits.WidePushoutShape.category = CategoryTheory.thin_category
                      @[simp]
                      theorem CategoryTheory.Limits.WidePushoutShape.wideSpan_map {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : JC) (arrows : (j : J) → B objs j) :
                      ∀ {X Y : CategoryTheory.Limits.WidePushoutShape J} (f : X Y), (CategoryTheory.Limits.WidePushoutShape.wideSpan B objs arrows).map f = CategoryTheory.Limits.WidePushoutShape.Hom.casesOn (motive := fun (a a_1 : CategoryTheory.Limits.WidePushoutShape J) (t : a.Hom a_1) => X = aY = a_1HEq f t((fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) X (fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) Y)) f (fun (X_1 : CategoryTheory.Limits.WidePushoutShape J) (h : X = X_1) => Eq.ndrec (motive := fun (X_2 : CategoryTheory.Limits.WidePushoutShape J) => Y = X_2HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.id X_2)((fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) X (fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) Y)) (fun (h : Y = X) => Eq.ndrec (motive := fun {Y : CategoryTheory.Limits.WidePushoutShape J} => (f : X Y) → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.id X)((fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) X (fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) Y)) (fun (f : X X) (h : HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.id X)) => CategoryTheory.CategoryStruct.id ((fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) X)) f) h) (fun (j : J) (h : X = none) => Eq.ndrec (motive := fun {X : CategoryTheory.Limits.WidePushoutShape J} => (f : X Y) → Y = some jHEq f (CategoryTheory.Limits.WidePushoutShape.Hom.init j)((fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) X (fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) Y)) (fun (f : none Y) (h : Y = some j) => Eq.ndrec (motive := fun {Y : CategoryTheory.Limits.WidePushoutShape J} => (f : none Y) → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.init j)((fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) none (fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) Y)) (fun (f : none some j) (h : HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.init j)) => arrows j) f) f)
                      @[simp]
                      theorem CategoryTheory.Limits.WidePushoutShape.wideSpan_obj {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : JC) (arrows : (j : J) → B objs j) (j : CategoryTheory.Limits.WidePushoutShape J) :

                      Construct a functor out of the wide pushout shape given a J-indexed collection of arrows from a fixed object.

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

                        Construct a cocone over a wide span.

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

                          Wide pushout diagrams of equivalent index types are equivalent.

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

                            Lifting universe and morphism levels preserves wide pushout diagrams.

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

                              HasWidePullbacks represents a choice of wide pullback for every collection of morphisms

                              Equations
                              Instances For
                                @[reducible, inline]

                                HasWidePushouts represents a choice of wide pushout for every collection of morphisms

                                Equations
                                Instances For
                                  @[reducible, inline]
                                  abbrev CategoryTheory.Limits.HasWidePullback {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : JC) (arrows : (j : J) → objs j B) :

                                  HasWidePullback B objs arrows means that wideCospan B objs arrows has a limit.

                                  Equations
                                  Instances For
                                    @[reducible, inline]
                                    abbrev CategoryTheory.Limits.HasWidePushout {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : JC) (arrows : (j : J) → B objs j) :

                                    HasWidePushout B objs arrows means that wideSpan B objs arrows has a colimit.

                                    Equations
                                    Instances For
                                      @[reducible, inline]
                                      noncomputable abbrev CategoryTheory.Limits.widePullback {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : JC) (arrows : (j : J) → objs j B) [CategoryTheory.Limits.HasWidePullback B objs arrows] :
                                      C

                                      A choice of wide pullback.

                                      Equations
                                      Instances For
                                        @[reducible, inline]
                                        noncomputable abbrev CategoryTheory.Limits.widePushout {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : JC) (arrows : (j : J) → B objs j) [CategoryTheory.Limits.HasWidePushout B objs arrows] :
                                        C

                                        A choice of wide pushout.

                                        Equations
                                        Instances For
                                          @[reducible, inline]
                                          noncomputable abbrev CategoryTheory.Limits.WidePullback.π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → objs j B) [CategoryTheory.Limits.HasWidePullback B objs arrows] (j : J) :

                                          The j-th projection from the pullback.

                                          Equations
                                          Instances For
                                            @[reducible, inline]
                                            noncomputable abbrev CategoryTheory.Limits.WidePullback.base {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → objs j B) [CategoryTheory.Limits.HasWidePullback B objs arrows] :

                                            The unique map to the base from the pullback.

                                            Equations
                                            Instances For
                                              @[reducible, inline]
                                              noncomputable abbrev CategoryTheory.Limits.WidePullback.lift {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} {arrows : (j : J) → objs j B} [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X B) (fs : (j : J) → X objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) :

                                              Lift a collection of morphisms to a morphism to the pullback.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem CategoryTheory.Limits.WidePullback.lift_π_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → objs j B) [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X B) (fs : (j : J) → X objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) (j : J) {Z : C} (h : objs j Z) :
                                                theorem CategoryTheory.Limits.WidePullback.lift_π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → objs j B) [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X B) (fs : (j : J) → X objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) (j : J) :
                                                theorem CategoryTheory.Limits.WidePullback.lift_base_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → objs j B) [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X B) (fs : (j : J) → X objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) {Z : C} (h : B Z) :
                                                theorem CategoryTheory.Limits.WidePullback.lift_base {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → objs j B) [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X B) (fs : (j : J) → X objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) :
                                                theorem CategoryTheory.Limits.WidePullback.eq_lift_of_comp_eq {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → objs j B) [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X B) (fs : (j : J) → X objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) (g : X CategoryTheory.Limits.widePullback B objs arrows) :
                                                @[reducible, inline]
                                                noncomputable abbrev CategoryTheory.Limits.WidePushout.ι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → B objs j) [CategoryTheory.Limits.HasWidePushout B objs arrows] (j : J) :

                                                The j-th inclusion to the pushout.

                                                Equations
                                                Instances For
                                                  @[reducible, inline]
                                                  noncomputable abbrev CategoryTheory.Limits.WidePushout.head {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → B objs j) [CategoryTheory.Limits.HasWidePushout B objs arrows] :

                                                  The unique map from the head to the pushout.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    @[reducible, inline]
                                                    noncomputable abbrev CategoryTheory.Limits.WidePushout.desc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} {arrows : (j : J) → B objs j} [CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C} (f : B X) (fs : (j : J) → objs j X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f) :

                                                    Descend a collection of morphisms to a morphism from the pushout.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      theorem CategoryTheory.Limits.WidePushout.ι_desc_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → B objs j) [CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C} (f : B X) (fs : (j : J) → objs j X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f) (j : J) {Z : C} (h : X Z) :
                                                      theorem CategoryTheory.Limits.WidePushout.ι_desc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → B objs j) [CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C} (f : B X) (fs : (j : J) → objs j X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f) (j : J) :
                                                      theorem CategoryTheory.Limits.WidePushout.head_desc_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → B objs j) [CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C} (f : B X) (fs : (j : J) → objs j X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f) {Z : C} (h : X Z) :
                                                      theorem CategoryTheory.Limits.WidePushout.head_desc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → B objs j) [CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C} (f : B X) (fs : (j : J) → objs j X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f) :
                                                      theorem CategoryTheory.Limits.WidePushout.eq_desc_of_comp_eq {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : JC} (arrows : (j : J) → B objs j) [CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C} (f : B X) (fs : (j : J) → objs j X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f) (g : CategoryTheory.Limits.widePushout B objs arrows X) :

                                                      The obvious functor WidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ

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

                                                        The obvious functor WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ

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

                                                          The inverse of the unit isomorphism of the equivalence widePushoutShapeOpEquiv : (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J

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

                                                            The counit isomorphism of the equivalence widePullbackShapeOpEquiv : (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J

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

                                                              The inverse of the unit isomorphism of the equivalence widePullbackShapeOpEquiv : (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J

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

                                                                The counit isomorphism of the equivalence widePushoutShapeOpEquiv : (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J

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

                                                                  The duality equivalence (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J

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

                                                                    The duality equivalence (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J

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

                                                                      If a category has wide pushouts on a higher universe level it also has wide pushouts on a lower universe level.

                                                                      If a category has wide pullbacks on a higher universe level it also has wide pullbacks on a lower universe level.