Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

HasPullback #

HasPullback f g and pullback f g provides API for HasLimit and limit in the case of pullacks.

Main definitions #

  pullback f g ---pullback.snd f g---> Y
      |                                |
      |                                |
pullback.snd f g                       g
      |                                |
      v                                v
      X --------------f--------------> Z
      X --------------f--------------> Y
      |                                |
      g                          pushout.inr f g
      |                                |
      v                                v
      Z ---pushout.inl f g---> pushout f g

Main results & API #

(The dual results for pushouts are also available)

References #

@[reducible, inline]
abbrev CategoryTheory.Limits.HasPullback {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Z) (g : Y Z) :

HasPullback f g represents a particular choice of limiting cone for the pair of morphisms f : X ⟶ Z and g : Y ⟶ Z.

Equations
Instances For
    @[reducible, inline]
    abbrev CategoryTheory.Limits.HasPushout {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Y) (g : X Z) :

    HasPushout f g represents a particular choice of colimiting cocone for the pair of morphisms f : X ⟶ Y and g : X ⟶ Z.

    Equations
    Instances For
      @[reducible, inline]
      abbrev CategoryTheory.Limits.pullback {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Z) (g : Y Z) [HasPullback f g] :
      C

      pullback f g computes the pullback of a pair of morphisms with the same target.

      Equations
      Instances For
        @[reducible, inline]
        abbrev CategoryTheory.Limits.pullback.cone {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Z) (g : Y Z) [HasPullback f g] :

        The cone associated to the pullback of f and g

        Equations
        Instances For
          @[reducible, inline]
          abbrev CategoryTheory.Limits.pushout {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Y) (g : X Z) [HasPushout f g] :
          C

          pushout f g computes the pushout of a pair of morphisms with the same source.

          Equations
          Instances For
            @[reducible, inline]
            abbrev CategoryTheory.Limits.pushout.cocone {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Y) (g : X Z) [HasPushout f g] :

            The cocone associated to the pullback of f and g

            Equations
            Instances For
              @[reducible, inline]
              abbrev CategoryTheory.Limits.pullback.fst {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Z) (g : Y Z) [HasPullback f g] :

              The first projection of the pullback of f and g.

              Equations
              Instances For
                @[reducible, inline]
                abbrev CategoryTheory.Limits.pullback.snd {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Z) (g : Y Z) [HasPullback f g] :

                The second projection of the pullback of f and g.

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev CategoryTheory.Limits.pushout.inl {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Y) (g : X Z) [HasPushout f g] :
                  Y pushout f g

                  The first inclusion into the pushout of f and g.

                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev CategoryTheory.Limits.pushout.inr {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Y) (g : X Z) [HasPushout f g] :
                    Z pushout f g

                    The second inclusion into the pushout of f and g.

                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev CategoryTheory.Limits.pullback.lift {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : X Z} {g : Y Z} [HasPullback f g] (h : W X) (k : W Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) :

                      A pair of morphisms h : W ⟶ X and k : W ⟶ Y satisfying h ≫ f = k ≫ g induces a morphism pullback.lift : W ⟶ pullback f g.

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev CategoryTheory.Limits.pushout.desc {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : X Y} {g : X Z} [HasPushout f g] (h : Y W) (k : Z W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) :
                        pushout f g W

                        A pair of morphisms h : Y ⟶ W and k : Z ⟶ W satisfying f ≫ h = g ≫ k induces a morphism pushout.desc : pushout f g ⟶ W.

                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev CategoryTheory.Limits.pullback.isLimit {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Z) (g : Y Z) [HasPullback f g] :

                          The cone associated to a pullback is a limit cone.

                          Equations
                          Instances For
                            @[reducible, inline]
                            abbrev CategoryTheory.Limits.pushout.isColimit {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Y) (g : X Z) [HasPushout f g] :

                            The cocone associated to a pushout is a colimit cone.

                            Equations
                            Instances For
                              @[simp]
                              theorem CategoryTheory.Limits.PullbackCone.fst_limit_cone {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Z) (g : Y Z) [HasLimit (cospan f g)] :
                              @[simp]
                              theorem CategoryTheory.Limits.PullbackCone.snd_limit_cone {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Z) (g : Y Z) [HasLimit (cospan f g)] :
                              theorem CategoryTheory.Limits.pullback.lift_fst {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : X Z} {g : Y Z} [HasPullback f g] (h : W X) (k : W Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) :
                              CategoryStruct.comp (lift h k w) (fst f g) = h
                              theorem CategoryTheory.Limits.pullback.lift_fst_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : X Z} {g : Y Z} [HasPullback f g] (h : W X) (k : W Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : C} (h✝ : X Z✝) :
                              theorem CategoryTheory.Limits.pullback.lift_snd {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : X Z} {g : Y Z} [HasPullback f g] (h : W X) (k : W Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) :
                              CategoryStruct.comp (lift h k w) (snd f g) = k
                              theorem CategoryTheory.Limits.pullback.lift_snd_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : X Z} {g : Y Z} [HasPullback f g] (h : W X) (k : W Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : C} (h✝ : Y Z✝) :
                              theorem CategoryTheory.Limits.pushout.inl_desc {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : X Y} {g : X Z} [HasPushout f g] (h : Y W) (k : Z W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) :
                              CategoryStruct.comp (inl f g) (desc h k w) = h
                              theorem CategoryTheory.Limits.pushout.inl_desc_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : X Y} {g : X Z} [HasPushout f g] (h : Y W) (k : Z W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Z✝ : C} (h✝ : W Z✝) :
                              theorem CategoryTheory.Limits.pushout.inr_desc {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : X Y} {g : X Z} [HasPushout f g] (h : Y W) (k : Z W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) :
                              CategoryStruct.comp (inr f g) (desc h k w) = k
                              theorem CategoryTheory.Limits.pushout.inr_desc_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : X Y} {g : X Z} [HasPushout f g] (h : Y W) (k : Z W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Z✝ : C} (h✝ : W Z✝) :
                              def CategoryTheory.Limits.pullback.lift' {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : X Z} {g : Y Z} [HasPullback f g] (h : W X) (k : W Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) :
                              { l : W pullback f g // CategoryStruct.comp l (fst f g) = h CategoryStruct.comp l (snd f g) = k }

                              A pair of morphisms h : W ⟶ X and k : W ⟶ Y satisfying h ≫ f = k ≫ g induces a morphism l : W ⟶ pullback f g such that l ≫ pullback.fst = h and l ≫ pullback.snd = k.

                              Equations
                              Instances For
                                def CategoryTheory.Limits.pullback.desc' {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : X Y} {g : X Z} [HasPushout f g] (h : Y W) (k : Z W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) :

                                A pair of morphisms h : Y ⟶ W and k : Z ⟶ W satisfying f ≫ h = g ≫ k induces a morphism l : pushout f g ⟶ W such that pushout.inl _ _ ≫ l = h and pushout.inr _ _ ≫ l = k.

                                Equations
                                Instances For
                                  theorem CategoryTheory.Limits.pullback.condition {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X Z} {g : Y Z} [HasPullback f g] :
                                  theorem CategoryTheory.Limits.pullback.condition_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X Z} {g : Y Z} [HasPullback f g] {Z✝ : C} (h : Z Z✝) :
                                  theorem CategoryTheory.Limits.pushout.condition {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X Y} {g : X Z} [HasPushout f g] :
                                  theorem CategoryTheory.Limits.pushout.condition_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X Y} {g : X Z} [HasPushout f g] {Z✝ : C} (h : pushout f g Z✝) :
                                  theorem CategoryTheory.Limits.pullback.hom_ext {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X Z} {g : Y Z} [HasPullback f g] {W : C} {k l : W pullback f g} (h₀ : CategoryStruct.comp k (fst f g) = CategoryStruct.comp l (fst f g)) (h₁ : CategoryStruct.comp k (snd f g) = CategoryStruct.comp l (snd f g)) :
                                  k = l

                                  Two morphisms into a pullback are equal if their compositions with the pullback morphisms are equal

                                  def CategoryTheory.Limits.pullbackIsPullback {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Z) (g : Y Z) [HasPullback f g] :

                                  The pullback cone built from the pullback projections is a pullback.

                                  Equations
                                  Instances For
                                    theorem CategoryTheory.Limits.pushout.hom_ext {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X Y} {g : X Z} [HasPushout f g] {W : C} {k l : pushout f g W} (h₀ : CategoryStruct.comp (inl f g) k = CategoryStruct.comp (inl f g) l) (h₁ : CategoryStruct.comp (inr f g) k = CategoryStruct.comp (inr f g) l) :
                                    k = l

                                    Two morphisms out of a pushout are equal if their compositions with the pushout morphisms are equal

                                    def CategoryTheory.Limits.pushoutIsPushout {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Y) (g : X Z) [HasPushout f g] :

                                    The pushout cocone built from the pushout coprojections is a pushout.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[reducible, inline]
                                      abbrev CategoryTheory.Limits.pullback.map {C : Type u} [Category.{v, u} C] {W X Y Z S T : C} (f₁ : W S) (f₂ : X S) [HasPullback f₁ f₂] (g₁ : Y T) (g₂ : Z T) [HasPullback g₁ g₂] (i₁ : W Y) (i₂ : X Z) (i₃ : S T) (eq₁ : CategoryStruct.comp f₁ i₃ = CategoryStruct.comp i₁ g₁) (eq₂ : CategoryStruct.comp f₂ i₃ = CategoryStruct.comp i₂ g₂) :
                                      pullback f₁ f₂ pullback g₁ g₂

                                      Given such a diagram, then there is a natural morphism W ×ₛ X ⟶ Y ×ₜ Z.

                                      W ⟶ Y
                                        ↘   ↘
                                        S ⟶ T
                                        ↗   ↗
                                      X ⟶ Z
                                      
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[reducible, inline]

                                        The canonical map X ×ₛ Y ⟶ X ×ₜ Y given S ⟶ T.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          theorem CategoryTheory.Limits.pullback.map_comp {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' X'' Y'' Z'' : C} {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} {f'' : X'' Z''} {g'' : Y'' Z''} (i₁ : X X') (j₁ : X' X'') (i₂ : Y Y') (j₂ : Y' Y'') (i₃ : Z Z') (j₃ : Z' Z'') [HasPullback f g] [HasPullback f' g'] [HasPullback f'' g''] (e₁ : CategoryStruct.comp f i₃ = CategoryStruct.comp i₁ f') (e₂ : CategoryStruct.comp g i₃ = CategoryStruct.comp i₂ g') (e₃ : CategoryStruct.comp f' j₃ = CategoryStruct.comp j₁ f'') (e₄ : CategoryStruct.comp g' j₃ = CategoryStruct.comp j₂ g'') :
                                          CategoryStruct.comp (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄) = map f g f'' g'' (CategoryStruct.comp i₁ j₁) (CategoryStruct.comp i₂ j₂) (CategoryStruct.comp i₃ j₃)
                                          theorem CategoryTheory.Limits.pullback.map_comp_assoc {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' X'' Y'' Z'' : C} {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} {f'' : X'' Z''} {g'' : Y'' Z''} (i₁ : X X') (j₁ : X' X'') (i₂ : Y Y') (j₂ : Y' Y'') (i₃ : Z Z') (j₃ : Z' Z'') [HasPullback f g] [HasPullback f' g'] [HasPullback f'' g''] (e₁ : CategoryStruct.comp f i₃ = CategoryStruct.comp i₁ f') (e₂ : CategoryStruct.comp g i₃ = CategoryStruct.comp i₂ g') (e₃ : CategoryStruct.comp f' j₃ = CategoryStruct.comp j₁ f'') (e₄ : CategoryStruct.comp g' j₃ = CategoryStruct.comp j₂ g'') {Z✝ : C} (h : pullback f'' g'' Z✝) :
                                          CategoryStruct.comp (map f g f' g' i₁ i₂ i₃ e₁ e₂) (CategoryStruct.comp (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄) h) = CategoryStruct.comp (map f g f'' g'' (CategoryStruct.comp i₁ j₁) (CategoryStruct.comp i₂ j₂) (CategoryStruct.comp i₃ j₃) ) h
                                          @[simp]
                                          theorem CategoryTheory.Limits.pullback.map_id {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X Z} {g : Y Z} [HasPullback f g] :
                                          @[reducible, inline]
                                          abbrev CategoryTheory.Limits.pushout.map {C : Type u} [Category.{v, u} C] {W X Y Z S T : C} (f₁ : S W) (f₂ : S X) [HasPushout f₁ f₂] (g₁ : T Y) (g₂ : T Z) [HasPushout g₁ g₂] (i₁ : W Y) (i₂ : X Z) (i₃ : S T) (eq₁ : CategoryStruct.comp f₁ i₁ = CategoryStruct.comp i₃ g₁) (eq₂ : CategoryStruct.comp f₂ i₂ = CategoryStruct.comp i₃ g₂) :
                                          pushout f₁ f₂ pushout g₁ g₂

                                          Given such a diagram, then there is a natural morphism W ⨿ₛ X ⟶ Y ⨿ₜ Z.

                                            W ⟶ Y
                                           ↗   ↗
                                          S ⟶ T
                                           ↘   ↘
                                            X ⟶ Z
                                          
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[reducible, inline]

                                            The canonical map X ⨿ₛ Y ⟶ X ⨿ₜ Y given S ⟶ T.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              theorem CategoryTheory.Limits.pushout.map_comp {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' X'' Y'' Z'' : C} {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} {f'' : X'' Y''} {g'' : X'' Z''} (i₁ : X X') (j₁ : X' X'') (i₂ : Y Y') (j₂ : Y' Y'') (i₃ : Z Z') (j₃ : Z' Z'') [HasPushout f g] [HasPushout f' g'] [HasPushout f'' g''] (e₁ : CategoryStruct.comp f i₂ = CategoryStruct.comp i₁ f') (e₂ : CategoryStruct.comp g i₃ = CategoryStruct.comp i₁ g') (e₃ : CategoryStruct.comp f' j₂ = CategoryStruct.comp j₁ f'') (e₄ : CategoryStruct.comp g' j₃ = CategoryStruct.comp j₁ g'') :
                                              CategoryStruct.comp (map f g f' g' i₂ i₃ i₁ e₁ e₂) (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄) = map f g f'' g'' (CategoryStruct.comp i₂ j₂) (CategoryStruct.comp i₃ j₃) (CategoryStruct.comp i₁ j₁)
                                              theorem CategoryTheory.Limits.pushout.map_comp_assoc {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' X'' Y'' Z'' : C} {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} {f'' : X'' Y''} {g'' : X'' Z''} (i₁ : X X') (j₁ : X' X'') (i₂ : Y Y') (j₂ : Y' Y'') (i₃ : Z Z') (j₃ : Z' Z'') [HasPushout f g] [HasPushout f' g'] [HasPushout f'' g''] (e₁ : CategoryStruct.comp f i₂ = CategoryStruct.comp i₁ f') (e₂ : CategoryStruct.comp g i₃ = CategoryStruct.comp i₁ g') (e₃ : CategoryStruct.comp f' j₂ = CategoryStruct.comp j₁ f'') (e₄ : CategoryStruct.comp g' j₃ = CategoryStruct.comp j₁ g'') {Z✝ : C} (h : pushout f'' g'' Z✝) :
                                              CategoryStruct.comp (map f g f' g' i₂ i₃ i₁ e₁ e₂) (CategoryStruct.comp (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄) h) = CategoryStruct.comp (map f g f'' g'' (CategoryStruct.comp i₂ j₂) (CategoryStruct.comp i₃ j₃) (CategoryStruct.comp i₁ j₁) ) h
                                              @[simp]
                                              theorem CategoryTheory.Limits.pushout.map_id {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X Y} {g : X Z} [HasPushout f g] :
                                              instance CategoryTheory.Limits.pullback.map_isIso {C : Type u} [Category.{v, u} C] {W X Y Z S T : C} (f₁ : W S) (f₂ : X S) [HasPullback f₁ f₂] (g₁ : Y T) (g₂ : Z T) [HasPullback g₁ g₂] (i₁ : W Y) (i₂ : X Z) (i₃ : S T) (eq₁ : CategoryStruct.comp f₁ i₃ = CategoryStruct.comp i₁ g₁) (eq₂ : CategoryStruct.comp f₂ i₃ = CategoryStruct.comp i₂ g₂) [IsIso i₁] [IsIso i₂] [IsIso i₃] :
                                              IsIso (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
                                              def CategoryTheory.Limits.pullback.congrHom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X Z} {g₁ g₂ : Y Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [HasPullback f₁ g₁] [HasPullback f₂ g₂] :
                                              pullback f₁ g₁ pullback f₂ g₂

                                              If f₁ = f₂ and g₁ = g₂, we may construct a canonical isomorphism pullback f₁ g₁ ≅ pullback f₂ g₂

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem CategoryTheory.Limits.pullback.congrHom_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X Z} {g₁ g₂ : Y Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [HasPullback f₁ g₁] [HasPullback f₂ g₂] :
                                                (congrHom h₁ h₂).hom = map f₁ g₁ f₂ g₂ (CategoryStruct.id X) (CategoryStruct.id Y) (CategoryStruct.id Z)
                                                @[simp]
                                                theorem CategoryTheory.Limits.pullback.congrHom_inv {C : Type u} [Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X Z} {g₁ g₂ : Y Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [HasPullback f₁ g₁] [HasPullback f₂ g₂] :
                                                (congrHom h₁ h₂).inv = map f₂ g₂ f₁ g₁ (CategoryStruct.id X) (CategoryStruct.id Y) (CategoryStruct.id Z)
                                                instance CategoryTheory.Limits.pushout.map_isIso {C : Type u} [Category.{v, u} C] {W X Y Z S T : C} (f₁ : S W) (f₂ : S X) [HasPushout f₁ f₂] (g₁ : T Y) (g₂ : T Z) [HasPushout g₁ g₂] (i₁ : W Y) (i₂ : X Z) (i₃ : S T) (eq₁ : CategoryStruct.comp f₁ i₁ = CategoryStruct.comp i₃ g₁) (eq₂ : CategoryStruct.comp f₂ i₂ = CategoryStruct.comp i₃ g₂) [IsIso i₁] [IsIso i₂] [IsIso i₃] :
                                                IsIso (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
                                                def CategoryTheory.Limits.pushout.congrHom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X Y} {g₁ g₂ : X Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [HasPushout f₁ g₁] [HasPushout f₂ g₂] :
                                                pushout f₁ g₁ pushout f₂ g₂

                                                If f₁ = f₂ and g₁ = g₂, we may construct a canonical isomorphism pushout f₁ g₁ ≅ pullback f₂ g₂

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[simp]
                                                  theorem CategoryTheory.Limits.pushout.congrHom_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X Y} {g₁ g₂ : X Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [HasPushout f₁ g₁] [HasPushout f₂ g₂] :
                                                  (congrHom h₁ h₂).hom = map f₁ g₁ f₂ g₂ (CategoryStruct.id Y) (CategoryStruct.id Z) (CategoryStruct.id X)
                                                  @[simp]
                                                  theorem CategoryTheory.Limits.pushout.congrHom_inv {C : Type u} [Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X Y} {g₁ g₂ : X Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [HasPushout f₁ g₁] [HasPushout f₂ g₂] :
                                                  (congrHom h₁ h₂).inv = map f₂ g₂ f₁ g₁ (CategoryStruct.id Y) (CategoryStruct.id Z) (CategoryStruct.id X)
                                                  def CategoryTheory.Limits.pullbackComparison {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Z) (g : Y Z) [HasPullback f g] [HasPullback (G.map f) (G.map g)] :
                                                  G.obj (pullback f g) pullback (G.map f) (G.map g)

                                                  The comparison morphism for the pullback of f,g. This is an isomorphism iff G preserves the pullback of f,g; see Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.Limits.pullbackComparison_comp_fst {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Z) (g : Y Z) [HasPullback f g] [HasPullback (G.map f) (G.map g)] :
                                                    CategoryStruct.comp (pullbackComparison G f g) (pullback.fst (G.map f) (G.map g)) = G.map (pullback.fst f g)
                                                    @[simp]
                                                    theorem CategoryTheory.Limits.pullbackComparison_comp_fst_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Z) (g : Y Z) [HasPullback f g] [HasPullback (G.map f) (G.map g)] {Z✝ : D} (h : G.obj X Z✝) :
                                                    @[simp]
                                                    theorem CategoryTheory.Limits.pullbackComparison_comp_snd {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Z) (g : Y Z) [HasPullback f g] [HasPullback (G.map f) (G.map g)] :
                                                    CategoryStruct.comp (pullbackComparison G f g) (pullback.snd (G.map f) (G.map g)) = G.map (pullback.snd f g)
                                                    @[simp]
                                                    theorem CategoryTheory.Limits.pullbackComparison_comp_snd_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Z) (g : Y Z) [HasPullback f g] [HasPullback (G.map f) (G.map g)] {Z✝ : D} (h : G.obj Y Z✝) :
                                                    @[simp]
                                                    theorem CategoryTheory.Limits.map_lift_pullbackComparison {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Z) (g : Y Z) [HasPullback f g] [HasPullback (G.map f) (G.map g)] {W : C} {h : W X} {k : W Y} (w : CategoryStruct.comp h f = CategoryStruct.comp k g) :
                                                    CategoryStruct.comp (G.map (pullback.lift h k w)) (pullbackComparison G f g) = pullback.lift (G.map h) (G.map k)
                                                    @[simp]
                                                    theorem CategoryTheory.Limits.map_lift_pullbackComparison_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Z) (g : Y Z) [HasPullback f g] [HasPullback (G.map f) (G.map g)] {W : C} {h : W X} {k : W Y} (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : D} (h✝ : pullback (G.map f) (G.map g) Z✝) :
                                                    CategoryStruct.comp (G.map (pullback.lift h k w)) (CategoryStruct.comp (pullbackComparison G f g) h✝) = CategoryStruct.comp (pullback.lift (G.map h) (G.map k) ) h✝
                                                    def CategoryTheory.Limits.pushoutComparison {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Y) (g : X Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] :
                                                    pushout (G.map f) (G.map g) G.obj (pushout f g)

                                                    The comparison morphism for the pushout of f,g. This is an isomorphism iff G preserves the pushout of f,g; see Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem CategoryTheory.Limits.inl_comp_pushoutComparison {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Y) (g : X Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] :
                                                      CategoryStruct.comp (pushout.inl (G.map f) (G.map g)) (pushoutComparison G f g) = G.map (pushout.inl f g)
                                                      @[simp]
                                                      theorem CategoryTheory.Limits.inl_comp_pushoutComparison_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Y) (g : X Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] {Z✝ : D} (h : G.obj (pushout f g) Z✝) :
                                                      @[simp]
                                                      theorem CategoryTheory.Limits.inr_comp_pushoutComparison {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Y) (g : X Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] :
                                                      CategoryStruct.comp (pushout.inr (G.map f) (G.map g)) (pushoutComparison G f g) = G.map (pushout.inr f g)
                                                      @[simp]
                                                      theorem CategoryTheory.Limits.inr_comp_pushoutComparison_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Y) (g : X Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] {Z✝ : D} (h : G.obj (pushout f g) Z✝) :
                                                      @[simp]
                                                      theorem CategoryTheory.Limits.pushoutComparison_map_desc {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Y) (g : X Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] {W : C} {h : Y W} {k : Z W} (w : CategoryStruct.comp f h = CategoryStruct.comp g k) :
                                                      CategoryStruct.comp (pushoutComparison G f g) (G.map (pushout.desc h k w)) = pushout.desc (G.map h) (G.map k)
                                                      @[simp]
                                                      theorem CategoryTheory.Limits.pushoutComparison_map_desc_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : X Y) (g : X Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] {W : C} {h : Y W} {k : Z W} (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Z✝ : D} (h✝ : G.obj W Z✝) :
                                                      CategoryStruct.comp (pushoutComparison G f g) (CategoryStruct.comp (G.map (pushout.desc h k w)) h✝) = CategoryStruct.comp (pushout.desc (G.map h) (G.map k) ) h✝
                                                      theorem CategoryTheory.Limits.hasPullback_symmetry {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Z) (g : Y Z) [HasPullback f g] :

                                                      Making this a global instance would make the typeclass search go in an infinite loop.

                                                      def CategoryTheory.Limits.pullbackSymmetry {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Z) (g : Y Z) [HasPullback f g] :

                                                      The isomorphism X ×[Z] Y ≅ Y ×[Z] X.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        theorem CategoryTheory.Limits.hasPushout_symmetry {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Y) (g : X Z) [HasPushout f g] :

                                                        Making this a global instance would make the typeclass search go in an infinite loop.

                                                        def CategoryTheory.Limits.pushoutSymmetry {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Y) (g : X Z) [HasPushout f g] :

                                                        The isomorphism Y ⨿[X] Z ≅ Z ⨿[X] Y.

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

                                                          HasPushouts represents a choice of pushout for every pair of morphisms

                                                          Equations
                                                          Instances For
                                                            theorem CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan (C : Type u) [Category.{v, u} C] [∀ {X Y Z : C} {f : X Z} {g : Y Z}, HasLimit (cospan f g)] :

                                                            If C has all limits of diagrams cospan f g, then it has all pullbacks

                                                            theorem CategoryTheory.Limits.hasPushouts_of_hasColimit_span (C : Type u) [Category.{v, u} C] [∀ {X Y Z : C} {f : X Y} {g : X Z}, HasColimit (span f g)] :

                                                            If C has all colimits of diagrams span f g, then it has all pushouts

                                                            @[instance 100]

                                                            Having wide pullback at any universe level implies having binary pullbacks.

                                                            @[instance 100]

                                                            Having wide pushout at any universe level implies having binary pushouts.