Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

CategoryTheory.Limits.HasPullback abbrev

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)

Full source

/-- `HasPullback f g` represents a particular choice of limiting cone
for the pair of morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`.
-/
abbrev HasPullback {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :=
  HasLimit (cospan f g)

Existence of Pullback for Morphisms $f$ and $g$

Informal description

Given a category $C$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $C$, the proposition $\text{HasPullback}(f, g)$ asserts that there exists a pullback (fiber product) of $f$ and $g$, meaning there exists a limit cone for the cospan diagram formed by $f$ and $g$.

CategoryTheory.Limits.HasPushout abbrev

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)

Full source

/-- `HasPushout f g` represents a particular choice of colimiting cocone
for the pair of morphisms `f : X ⟶ Y` and `g : X ⟶ Z`.
-/
abbrev HasPushout {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) :=
  HasColimit (span f g)

Existence of Pushout for Morphisms $f$ and $g$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$, the proposition $\text{HasPushout}(f, g)$ asserts that there exists a pushout (fiber coproduct) of $f$ and $g$, meaning there exists a colimit cocone for the span diagram formed by $f$ and $g$.

CategoryTheory.Limits.pullback abbrev

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]

Full source

/-- `pullback f g` computes the pullback of a pair of morphisms with the same target. -/
abbrev pullback {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] :=
  limit (cospan f g)

Pullback Object of Morphisms $f$ and $g$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ for which a pullback exists (i.e., $\text{HasPullback}(f, g)$ holds), the pullback of $f$ and $g$ is an object $P$ in $\mathcal{C}$ equipped with morphisms $\pi_1 \colon P \to X$ and $\pi_2 \colon P \to Y$ such that the following diagram commutes: ``` P --π₂--> Y | | π₁ g | | v v X --f--> Z ``` and $P$ satisfies the universal property of pullbacks: for any other object $Q$ with morphisms $q_1 \colon Q \to X$ and $q_2 \colon Q \to Y$ making the analogous diagram commute, there exists a unique morphism $u \colon Q \to P$ such that $q_1 = \pi_1 \circ u$ and $q_2 = \pi_2 \circ u$.

CategoryTheory.Limits.pullback.cone abbrev

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] : PullbackCone f g

Full source

/-- The cone associated to the pullback of `f` and `g` -/
abbrev pullback.cone {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] : PullbackCone f g :=
  limit.cone (cospan f g)

Pullback Cone Construction for Morphisms $f$ and $g$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ for which a pullback exists (i.e., $\text{HasPullback}(f, g)$), the pullback cone consists of: - An object $P$ (the pullback object) - Morphisms $\pi_1 \colon P \to X$ and $\pi_2 \colon P \to Y$ such that the following diagram commutes: ``` P --π₂--> Y | | π₁ g | | v v X --f--> Z ```

CategoryTheory.Limits.pushout abbrev

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g]

Full source

/-- `pushout f g` computes the pushout of a pair of morphisms with the same source. -/
abbrev pushout {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] :=
  colimit (span f g)

Pushout Object of Morphisms $f$ and $g$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ for which a pushout exists (i.e., $\text{HasPushout}(f, g)$), the pushout object $\text{pushout}(f, g)$ is the colimit of the span diagram formed by $f$ and $g$. It fits into the following commutative diagram: \[ \begin{CD} X @>{f}>> Y \\ @V{g}VV @VV{\iota_1}V \\ Z @>>{\iota_2}> \text{pushout}(f, g) \end{CD} \] where $\iota_1$ and $\iota_2$ are the canonical morphisms from $Y$ and $Z$ to the pushout object, respectively.

CategoryTheory.Limits.pushout.cocone abbrev

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] : PushoutCocone f g

Full source

/-- The cocone associated to the pullback of `f` and `g` -/
abbrev pushout.cocone {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] : PushoutCocone f g :=
  colimit.cocone (span f g)

Pushout Cocone Construction for Morphisms $f$ and $g$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ for which a pushout exists (i.e., $\text{HasPushout}(f, g)$), the pushout cocone consists of: - An object $P$ (the pushout object) - Morphisms $\iota_1 \colon Y \to P$ and $\iota_2 \colon Z \to P$ such that the following diagram commutes: \[ \begin{CD} X @>{f}>> Y \\ @V{g}VV @VV{\iota_1}V \\ Z @>>{\iota_2}> P \end{CD} \]

CategoryTheory.Limits.pullback.fst abbrev

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] : pullback f g ⟶ X

Full source

/-- The first projection of the pullback of `f` and `g`. -/
abbrev pullback.fst {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] : pullbackpullback f g ⟶ X :=
  limit.π (cospan f g) WalkingCospan.left

First Projection Morphism from Pullback

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ for which a pullback exists, the first projection morphism $\pi_1 \colon \text{pullback}(f,g) \to X$ is the canonical morphism from the pullback object to $X$ that makes the following diagram commute: ``` pullback(f,g) --π₂--> Y | | π₁ g | | v v X -------f-------> Z ```

CategoryTheory.Limits.pullback.snd abbrev

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] : pullback f g ⟶ Y

Full source

/-- The second projection of the pullback of `f` and `g`. -/
abbrev pullback.snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] : pullbackpullback f g ⟶ Y :=
  limit.π (cospan f g) WalkingCospan.right

Second Projection Morphism from Pullback to $Y$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ for which a pullback exists, the second projection morphism $\pi_2 \colon \text{pullback}(f, g) \to Y$ is the canonical morphism from the pullback object to $Y$ that makes the following diagram commute: \[ \begin{CD} \text{pullback}(f, g) @>{\pi_2}>> Y \\ @V{\pi_1}VV @VV{g}V \\ X @>>{f}> Z \end{CD} \]

CategoryTheory.Limits.pushout.inl abbrev

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] : Y ⟶ pushout f g

Full source

/-- The first inclusion into the pushout of `f` and `g`. -/
abbrev pushout.inl {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] : Y ⟶ pushout f g :=
  colimit.ι (span f g) WalkingSpan.left

Left Inclusion Morphism into Pushout of $f$ and $g$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ for which a pushout exists, the morphism $\text{pushout.inl}(f, g) \colon Y \to \text{pushout}(f, g)$ is the canonical inclusion of $Y$ into the pushout object of $f$ and $g$. This fits into the following commutative diagram: \[ \begin{CD} X @>{f}>> Y \\ @V{g}VV @VV{\text{pushout.inl}(f, g)}V \\ Z @>>{\text{pushout.inr}(f, g)}> \text{pushout}(f, g) \end{CD} \]

CategoryTheory.Limits.pushout.inr abbrev

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] : Z ⟶ pushout f g

Full source

/-- The second inclusion into the pushout of `f` and `g`. -/
abbrev pushout.inr {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] : Z ⟶ pushout f g :=
  colimit.ι (span f g) WalkingSpan.right

Right inclusion into pushout of $f$ and $g$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ for which a pushout exists, the morphism $\text{pushout.inr}(f, g) \colon Z \to \text{pushout}(f, g)$ is the canonical inclusion of $Z$ into the pushout object, making the following diagram commute: \[ \begin{CD} X @>{f}>> Y \\ @V{g}VV @VV{\text{pushout.inl}(f, g)}V \\ Z @>>{\text{pushout.inr}(f, g)}> \text{pushout}(f, g) \end{CD} \]

CategoryTheory.Limits.pullback.lift abbrev

 {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y) (w : h ≫ f = k ≫ g) : W ⟶ pullback f g

Full source

/-- 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`. -/
abbrev pullback.lift {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] (h : W ⟶ X)
    (k : W ⟶ Y) (w : h ≫ f = k ≫ g) : W ⟶ pullback f g :=
  limit.lift _ (PullbackCone.mk h k w)

Universal Property of Pullback: Existence of Lifting Morphism

Informal description

Given a category $\mathcal{C}$ with a pullback of morphisms $f \colon X \to Z$ and $g \colon Y \to Z$, and given morphisms $h \colon W \to X$ and $k \colon W \to Y$ such that $h \circ f = k \circ g$, there exists a unique morphism $\mathrm{lift} \colon W \to \mathrm{pullback}\,f\,g$ making the following diagram commute: \[ \begin{tikzcd} W \arrow[dr, dashed, "\mathrm{lift}"] \arrow[ddr, "k"'] \arrow[drr, "h"] & & \\ & \mathrm{pullback}\,f\,g \arrow[r, "\pi_1"] \arrow[d, "\pi_2"'] & X \arrow[d, "f"] \\ & Y \arrow[r, "g"'] & Z \end{tikzcd} \]

CategoryTheory.Limits.pushout.desc abbrev

 {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W) (w : f ≫ h = g ≫ k) : pushout f g ⟶ W

Full source

/-- 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`. -/
abbrev pushout.desc {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W)
    (w : f ≫ h = g ≫ k) : pushoutpushout f g ⟶ W :=
  colimit.desc _ (PushoutCocone.mk h k w)

Universal property of pushout: $\text{pushout}(f,g) \to W$ induced by compatible maps $h$ and $k$

Informal description

Given a category $\mathcal{C}$ with morphisms $f \colon X \to Y$ and $g \colon X \to Z$ that have a pushout, and given morphisms $h \colon Y \to W$ and $k \colon Z \to W$ satisfying $f \circ h = g \circ k$, there exists a unique morphism $\text{pushout.desc}\, h\, k\, w \colon \text{pushout}(f, g) \to W$ making the following diagram commute: \[ \begin{CD} X @>{f}>> Y \\ @V{g}VV @VV{h}V \\ Z @>>{k}> W \\ \end{CD} \]

CategoryTheory.Limits.pullback.isLimit abbrev

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] : IsLimit (pullback.cone f g)

Full source

/-- The cone associated to a pullback is a limit cone. -/
abbrev pullback.isLimit {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] :
    IsLimit (pullback.cone f g) :=
  limit.isLimit (cospan f g)

Universal Property of the Pullback Cone

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ for which a pullback exists, the cone constructed from the pullback of $f$ and $g$ is a limit cone. This means it satisfies the universal property of pullbacks: for any other cone over the cospan formed by $f$ and $g$, there exists a unique morphism from that cone to the pullback cone making the relevant diagrams commute.

CategoryTheory.Limits.pushout.isColimit abbrev

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] : IsColimit (pushout.cocone f g)

Full source

/-- The cocone associated to a pushout is a colimit cone. -/
abbrev pushout.isColimit {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] :
    IsColimit (pushout.cocone f g) :=
  colimit.isColimit (span f g)

Universal Property of Pushout Cocone

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ for which a pushout exists (i.e., $\text{HasPushout}(f, g)$), the cocone $\text{pushout.cocone}(f, g)$ is a colimit cocone. This means it satisfies the universal property of pushouts: for any other cocone $(W, h \colon Y \to W, k \colon Z \to W)$ such that $f \circ h = g \circ k$, there exists a unique morphism $\text{pushout}(f, g) \to W$ making the diagram commute.

CategoryTheory.Limits.PullbackCone.fst_limit_cone theorem

 {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasLimit (cospan f g)] :
  PullbackCone.fst (limit.cone (cospan f g)) = pullback.fst f g

Full source

@[simp]
theorem PullbackCone.fst_limit_cone {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasLimit (cospan f g)] :
    PullbackCone.fst (limit.cone (cospan f g)) = pullback.fst f g := rfl

First Projection of Limit Cone Equals Pullback First Projection

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ for which the limit of the cospan diagram $(f, g)$ exists, the first projection morphism of the limit cone is equal to the canonical first projection morphism from the pullback of $f$ and $g$. That is, $\pi_1(\text{limit.cone}(f,g)) = \pi_1(\text{pullback}(f,g))$.

CategoryTheory.Limits.PullbackCone.snd_limit_cone theorem

 {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasLimit (cospan f g)] :
  PullbackCone.snd (limit.cone (cospan f g)) = pullback.snd f g

Full source

@[simp]
theorem PullbackCone.snd_limit_cone {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasLimit (cospan f g)] :
    PullbackCone.snd (limit.cone (cospan f g)) = pullback.snd f g := rfl

Equality of Second Projections in Pullback Limit Cone

Informal description

For any morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$ that admit a pullback (i.e., `[HasLimit (cospan f g)]`), the second projection morphism of the limit cone for the cospan diagram $(f, g)$ is equal to the canonical second projection morphism from the pullback object to $Y$.

CategoryTheory.Limits.PushoutCocone.inl_colimit_cocone theorem

 {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [HasColimit (span f g)] :
  PushoutCocone.inl (colimit.cocone (span f g)) = pushout.inl _ _

Full source

theorem PushoutCocone.inl_colimit_cocone {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y)
    [HasColimit (span f g)] : PushoutCocone.inl (colimit.cocone (span f g)) = pushout.inl _ _ := rfl

Inclusion Morphism of Colimit Cocone for Span Equals Pushout Inclusion

Informal description

Given morphisms $f \colon Z \to X$ and $g \colon Z \to Y$ in a category $\mathcal{C}$ where the pushout of $f$ and $g$ exists, the inclusion morphism $\mathrm{inl}$ of the colimit cocone for the span $(f, g)$ coincides with the canonical inclusion $\mathrm{pushout.inl}$ into the pushout object.

CategoryTheory.Limits.PushoutCocone.inr_colimit_cocone theorem

 {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [HasColimit (span f g)] :
  PushoutCocone.inr (colimit.cocone (span f g)) = pushout.inr _ _

Full source

theorem PushoutCocone.inr_colimit_cocone {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y)
    [HasColimit (span f g)] : PushoutCocone.inr (colimit.cocone (span f g)) = pushout.inr _ _ := rfl

Equality of Right Inclusion in Pushout Cocone and Canonical Pushout Inclusion

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon Z \to X$ and $g \colon Z \to Y$ in $\mathcal{C}$ for which a pushout exists, the inclusion morphism $\mathrm{inr}$ of the colimit cocone for the span $(f, g)$ coincides with the canonical inclusion $\mathrm{pushout.inr}(f, g) \colon Y \to \mathrm{pushout}(f, g)$. That is, the following equality holds: \[ \mathrm{inr}(\mathrm{colimit.cocone}(\mathrm{span}(f, g))) = \mathrm{pushout.inr}(f, g) \]

CategoryTheory.Limits.pullback.lift_fst theorem

 {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y) (w : h ≫ f = k ≫ g) :
  pullback.lift h k w ≫ pullback.fst f g = h

Full source

@[reassoc]
theorem pullback.lift_fst {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] (h : W ⟶ X)
    (k : W ⟶ Y) (w : h ≫ f = k ≫ g) : pullback.liftpullback.lift h k w ≫ pullback.fst f g = h :=
  limit.lift_π _ _

Commutativity of Pullback Lifting with First Projection

Informal description

Given a category $\mathcal{C}$ with a pullback of morphisms $f \colon X \to Z$ and $g \colon Y \to Z$, and given morphisms $h \colon W \to X$ and $k \colon W \to Y$ such that $h \circ f = k \circ g$, the composition of the lifting morphism $\mathrm{pullback.lift}\,h\,k\,w$ with the first projection $\pi_1 \colon \mathrm{pullback}(f,g) \to X$ equals $h$, i.e., \[ \mathrm{pullback.lift}\,h\,k\,w \circ \pi_1 = h. \]

CategoryTheory.Limits.pullback.lift_snd theorem

 {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y) (w : h ≫ f = k ≫ g) :
  pullback.lift h k w ≫ pullback.snd f g = k

Full source

@[reassoc]
theorem pullback.lift_snd {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] (h : W ⟶ X)
    (k : W ⟶ Y) (w : h ≫ f = k ≫ g) : pullback.liftpullback.lift h k w ≫ pullback.snd f g = k :=
  limit.lift_π _ _

Commutativity of pullback lift with second projection

Informal description

Given a category $\mathcal{C}$ with a pullback of morphisms $f \colon X \to Z$ and $g \colon Y \to Z$, and given morphisms $h \colon W \to X$ and $k \colon W \to Y$ such that $h \circ f = k \circ g$, the composition of the induced morphism $\mathrm{pullback.lift}\,h\,k\,w$ with the second projection $\pi_2 \colon \mathrm{pullback}(f,g) \to Y$ equals $k$, i.e., \[ \mathrm{pullback.lift}\,h\,k\,w \circ \pi_2 = k. \]

CategoryTheory.Limits.pushout.inl_desc theorem

 {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W) (w : f ≫ h = g ≫ k) :
  pushout.inl _ _ ≫ pushout.desc h k w = h

Full source

@[reassoc]
theorem pushout.inl_desc {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] (h : Y ⟶ W)
    (k : Z ⟶ W) (w : f ≫ h = g ≫ k) : pushout.inlpushout.inl _ _ ≫ pushout.desc h k w = h :=
  colimit.ι_desc _ _

Commutativity of Left Pushout Inclusion with Descending Morphism

Informal description

Given a category $\mathcal{C}$ with morphisms $f \colon X \to Y$ and $g \colon X \to Z$ that have a pushout, and given morphisms $h \colon Y \to W$ and $k \colon Z \to W$ satisfying $f \circ h = g \circ k$, the composition of the left inclusion $\iota_1 \colon Y \to \mathrm{pushout}(f,g)$ with the universal morphism $\mathrm{pushout.desc}\,h\,k\,w \colon \mathrm{pushout}(f,g) \to W$ equals $h$, i.e., \[ \iota_1 \circ \mathrm{pushout.desc}\,h\,k\,w = h. \]

CategoryTheory.Limits.pushout.inr_desc theorem

 {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W) (w : f ≫ h = g ≫ k) :
  pushout.inr _ _ ≫ pushout.desc h k w = k

Full source

@[reassoc]
theorem pushout.inr_desc {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] (h : Y ⟶ W)
    (k : Z ⟶ W) (w : f ≫ h = g ≫ k) : pushout.inrpushout.inr _ _ ≫ pushout.desc h k w = k :=
  colimit.ι_desc _ _

Commutativity of pushout right inclusion with descending morphism

Informal description

Given a category $\mathcal{C}$ with morphisms $f \colon X \to Y$ and $g \colon X \to Z$ that have a pushout, and given morphisms $h \colon Y \to W$ and $k \colon Z \to W$ satisfying $f \circ h = g \circ k$, the composition of the right inclusion $\iota_r \colon Z \to \text{pushout}(f,g)$ with the universal morphism $\text{pushout.desc}\, h\, k\, w \colon \text{pushout}(f,g) \to W$ equals $k$, i.e., \[ \iota_r \circ \text{pushout.desc}\, h\, k\, w = k. \]

CategoryTheory.Limits.pullback.lift' definition

 {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y) (w : h ≫ f = k ≫ g) :
  { l : W ⟶ pullback f g // l ≫ pullback.fst f g = h ∧ l ≫ pullback.snd f g = k }

Full source

/-- 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`. -/
def pullback.lift' {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y)
    (w : h ≫ f = k ≫ g) :
      { l : W ⟶ pullback f g // l ≫ pullback.fst f g = h ∧ l ≫ pullback.snd f g = k } :=
  ⟨pullback.lift h k w, pullback.lift_fst _ _ _, pullback.lift_snd _ _ _⟩

Universal property of pullback: existence of lifting morphism with specified projections

Informal description

Given a category $\mathcal{C}$ with a pullback of morphisms $f \colon X \to Z$ and $g \colon Y \to Z$, and given morphisms $h \colon W \to X$ and $k \colon W \to Y$ such that $h \circ f = k \circ g$, there exists a morphism $l \colon W \to \mathrm{pullback}\,f\,g$ satisfying $l \circ \pi_1 = h$ and $l \circ \pi_2 = k$, where $\pi_1$ and $\pi_2$ are the canonical projections from the pullback to $X$ and $Y$ respectively.

CategoryTheory.Limits.pullback.desc' definition

 {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W) (w : f ≫ h = g ≫ k) :
  { l : pushout f g ⟶ W // pushout.inl _ _ ≫ l = h ∧ pushout.inr _ _ ≫ l = k }

Full source

/-- 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`. -/
def pullback.desc' {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W)
    (w : f ≫ h = g ≫ k) :
      { l : pushout f g ⟶ W // pushout.inl _ _ ≫ l = h ∧ pushout.inr _ _ ≫ l = k } :=
  ⟨pushout.desc h k w, pushout.inl_desc _ _ _, pushout.inr_desc _ _ _⟩

Universal property of pushout: induced morphism from pushout to $W$ via compatible maps $h$ and $k$

Informal description

Given a category $\mathcal{C}$ with morphisms $f \colon X \to Y$ and $g \colon X \to Z$ that have a pushout, and given morphisms $h \colon Y \to W$ and $k \colon Z \to W$ satisfying $f \circ h = g \circ k$, there exists a unique morphism $l \colon \text{pushout}(f, g) \to W$ such that $\text{pushout.inl}(f, g) \circ l = h$ and $\text{pushout.inr}(f, g) \circ l = k$.

CategoryTheory.Limits.pullback.condition theorem

{X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] : pullback.fst f g ≫ f = pullback.snd f g ≫ g

Full source

@[reassoc]
theorem pullback.condition {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] :
    pullback.fstpullback.fst f g ≫ f = pullback.sndpullback.snd f g ≫ g :=
  PullbackCone.condition _

Commutativity of Pullback Projections: $\pi_1 \circ f = \pi_2 \circ g$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ that have a pullback, the first projection $\pi_1 \colon \text{pullback}(f,g) \to X$ and the second projection $\pi_2 \colon \text{pullback}(f,g) \to Y$ satisfy the commutativity condition $\pi_1 \circ f = \pi_2 \circ g$. In other words, the following diagram commutes: \[ \begin{CD} \text{pullback}(f,g) @>{\pi_2}>> Y \\ @V{\pi_1}VV @VV{g}V \\ X @>>{f}> Z \end{CD} \]

CategoryTheory.Limits.pushout.condition theorem

{X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] : f ≫ (pushout.inl f g) = g ≫ pushout.inr _ _

Full source

@[reassoc]
theorem pushout.condition {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] :
    f ≫ (pushout.inl f g) = g ≫ pushout.inr _ _ :=
  PushoutCocone.condition _

Commutativity of Pushout Square

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ for which a pushout exists, the following diagram commutes: \[ \begin{CD} X @>{f}>> Y \\ @V{g}VV @VV{\iota_1}V \\ Z @>>{\iota_2}> \text{pushout}(f, g) \end{CD} \] where $\iota_1 = \text{pushout.inl}(f, g)$ and $\iota_2 = \text{pushout.inr}(f, g)$ are the canonical inclusion morphisms into the pushout object. That is, $f \circ \iota_1 = g \circ \iota_2$.

CategoryTheory.Limits.pullback.hom_ext theorem

 {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] {W : C} {k l : W ⟶ pullback f g}
  (h₀ : k ≫ pullback.fst f g = l ≫ pullback.fst f g) (h₁ : k ≫ pullback.snd f g = l ≫ pullback.snd f g) : k = l

Full source

/-- Two morphisms into a pullback are equal if their compositions with the pullback morphisms are
    equal -/
@[ext 1100]
theorem pullback.hom_ext {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] {W : C}
    {k l : W ⟶ pullback f g} (h₀ : k ≫ pullback.fst f g = l ≫ pullback.fst f g)
    (h₁ : k ≫ pullback.snd f g = l ≫ pullback.snd f g) : k = l :=
  limit.hom_ext <| PullbackCone.equalizer_ext _ h₀ h₁

Uniqueness of Morphisms into Pullback via Projections

Informal description

Let $\mathcal{C}$ be a category with morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ that have a pullback. For any object $W$ in $\mathcal{C}$ and any two morphisms $k, l \colon W \to \text{pullback}(f, g)$, if both compositions $k \circ \pi_1 = l \circ \pi_1$ and $k \circ \pi_2 = l \circ \pi_2$ hold (where $\pi_1$ and $\pi_2$ are the pullback projections), then $k = l$.

CategoryTheory.Limits.pullbackIsPullback definition

 {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] :
  IsLimit (PullbackCone.mk (pullback.fst f g) (pullback.snd f g) pullback.condition)

Full source

/-- The pullback cone built from the pullback projections is a pullback. -/
def pullbackIsPullback {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] :
    IsLimit (PullbackCone.mk (pullback.fst f g) (pullback.snd f g) pullback.condition) :=
  PullbackCone.mkSelfIsLimit <| pullback.isLimit f g

Pullback cone is a limit cone

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ for which a pullback exists, the pullback cone formed by the canonical projections $\pi_1 \colon \text{pullback}(f,g) \to X$ and $\pi_2 \colon \text{pullback}(f,g) \to Y$ (satisfying $\pi_1 \circ f = \pi_2 \circ g$) is a limit cone for the cospan diagram formed by $f$ and $g$. This means it satisfies the universal property of pullbacks: for any other cone $(W, q_1 \colon W \to X, q_2 \colon W \to Y)$ with $q_1 \circ f = q_2 \circ g$, there exists a unique morphism $W \to \text{pullback}(f,g)$ making the appropriate diagram commute.

CategoryTheory.Limits.pushout.hom_ext theorem

 {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] {W : C} {k l : pushout f g ⟶ W}
  (h₀ : pushout.inl _ _ ≫ k = pushout.inl _ _ ≫ l) (h₁ : pushout.inr _ _ ≫ k = pushout.inr _ _ ≫ l) : k = l

Full source

/-- Two morphisms out of a pushout are equal if their compositions with the pushout morphisms are
    equal -/
@[ext 1100]
theorem pushout.hom_ext {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] {W : C}
    {k l : pushoutpushout f g ⟶ W} (h₀ : pushout.inlpushout.inl _ _ ≫ k = pushout.inlpushout.inl _ _ ≫ l)
    (h₁ : pushout.inrpushout.inr _ _ ≫ k = pushout.inrpushout.inr _ _ ≫ l) : k = l :=
  colimit.hom_ext <| PushoutCocone.coequalizer_ext _ h₀ h₁

Uniqueness of Morphisms from Pushout via Commuting Inclusions

Informal description

Let $\mathcal{C}$ be a category with morphisms $f \colon X \to Y$ and $g \colon X \to Z$ that have a pushout. For any object $W$ in $\mathcal{C}$ and any pair of morphisms $k, l \colon \text{pushout}(f, g) \to W$, if the compositions $\iota_1 \circ k = \iota_1 \circ l$ and $\iota_2 \circ k = \iota_2 \circ l$ hold (where $\iota_1 \colon Y \to \text{pushout}(f, g)$ and $\iota_2 \colon Z \to \text{pushout}(f, g)$ are the canonical pushout inclusion morphisms), then $k = l$.

CategoryTheory.Limits.pushoutIsPushout definition

 {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] :
  IsColimit (PushoutCocone.mk (pushout.inl f g) (pushout.inr _ _) pushout.condition)

Full source

/-- The pushout cocone built from the pushout coprojections is a pushout. -/
def pushoutIsPushout {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] :
    IsColimit (PushoutCocone.mk (pushout.inl f g) (pushout.inr _ _) pushout.condition) :=
  PushoutCocone.IsColimit.mk _ (fun s => pushout.desc s.inl s.inr s.condition) (by simp) (by simp)
    (by aesop_cat)

Pushout cocone is a colimit cocone

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ for which a pushout exists, the cocone formed by the canonical pushout inclusions $\iota_1 \colon Y \to \text{pushout}(f, g)$ and $\iota_2 \colon Z \to \text{pushout}(f, g)$ (satisfying $f \circ \iota_1 = g \circ \iota_2$) is a colimit cocone for the span diagram formed by $f$ and $g$. This means it satisfies the universal property of pushouts: for any other cocone $(W, h \colon Y \to W, k \colon Z \to W)$ with $f \circ h = g \circ k$, there exists a unique morphism $\text{pushout}(f, g) \to W$ making the appropriate diagram commute.

CategoryTheory.Limits.pullback.lift_fst_snd theorem

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] : lift (fst f g) (snd f g) condition = 𝟙 (pullback f g)

Full source

@[simp]
lemma pullback.lift_fst_snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] :
    lift (fst f g) (snd f g) condition = 𝟙 (pullback f g) := by
  apply hom_ext <;> simp

Identity via Pullback Universal Property: $\mathrm{lift}(\pi_1, \pi_2) = \mathrm{id}$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ that have a pullback, the lifting morphism $\mathrm{lift}(\pi_1, \pi_2, \mathrm{condition})$ (where $\pi_1 \colon \mathrm{pullback}(f,g) \to X$ and $\pi_2 \colon \mathrm{pullback}(f,g) \to Y$ are the pullback projections, and $\mathrm{condition}$ is the proof that $\pi_1 \circ f = \pi_2 \circ g$) is equal to the identity morphism on $\mathrm{pullback}(f,g)$. In other words, applying the universal property of the pullback to the pullback projections themselves yields the identity morphism on the pullback object.

CategoryTheory.Limits.pushout.desc_inl_inr theorem

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] : desc (inl f g) (inr f g) condition = 𝟙 (pushout f g)

Full source

@[simp]
lemma pushout.desc_inl_inr {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] :
    desc (inl f g) (inr f g) condition = 𝟙 (pushout f g) := by
  apply hom_ext <;> simp

Identity Morphism via Pushout Universal Property

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ that have a pushout, the universal morphism $\text{desc}(\iota_1, \iota_2, \text{condition})$ from the pushout object to itself, induced by the canonical inclusions $\iota_1 = \text{pushout.inl}(f, g)$ and $\iota_2 = \text{pushout.inr}(f, g)$, is equal to the identity morphism on $\text{pushout}(f, g)$. Here, $\text{condition}$ refers to the commutativity of the pushout square: \[ f \circ \iota_1 = g \circ \iota_2. \]

CategoryTheory.Limits.pullback.map abbrev

 {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₁ : f₁ ≫ i₃ = i₁ ≫ g₁) (eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) :
  pullback f₁ f₂ ⟶ pullback g₁ g₂

Full source

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

```
W ⟶ Y
  ↘   ↘
  S ⟶ T
  ↗   ↗
X ⟶ Z
```
-/
abbrev pullback.map {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₁ : f₁ ≫ i₃ = i₁ ≫ g₁) (eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) : pullbackpullback f₁ f₂ ⟶ pullback g₁ g₂ :=
  pullback.lift (pullback.fstpullback.fst f₁ f₂ ≫ i₁) (pullback.sndpullback.snd f₁ f₂ ≫ i₂)
    (by simp only [Category.assoc, ← eq₁, ← eq₂, pullback.condition_assoc])

Induced Morphism Between Pullbacks via Commutative Squares

Informal description

Given a category $\mathcal{C}$ and commutative diagrams \[ \begin{tikzcd} W \arrow[r, "f_1"] \arrow[d, "i_1"'] & S \arrow[d, "i_3"] \\ Y \arrow[r, "g_1"'] & T \end{tikzcd} \quad \text{and} \quad \begin{tikzcd} X \arrow[r, "f_2"] \arrow[d, "i_2"'] & S \arrow[d, "i_3"] \\ Z \arrow[r, "g_2"'] & T \end{tikzcd} \] where the pullbacks $W \times_S X$ and $Y \times_T Z$ exist, there exists a unique morphism $W \times_S X \to Y \times_T Z$ induced by the universal property of pullbacks.

CategoryTheory.Limits.pullback.mapDesc abbrev

 {X Y S T : C} (f : X ⟶ S) (g : Y ⟶ S) (i : S ⟶ T) [HasPullback f g] [HasPullback (f ≫ i) (g ≫ i)] :
  pullback f g ⟶ pullback (f ≫ i) (g ≫ i)

Full source

/-- The canonical map `X ×ₛ Y ⟶ X ×ₜ Y` given `S ⟶ T`. -/
abbrev pullback.mapDesc {X Y S T : C} (f : X ⟶ S) (g : Y ⟶ S) (i : S ⟶ T) [HasPullback f g]
    [HasPullback (f ≫ i) (g ≫ i)] : pullbackpullback f g ⟶ pullback (f ≫ i) (g ≫ i) :=
  pullback.map f g (f ≫ i) (g ≫ i) (𝟙 _) (𝟙 _) i (Category.id_comp _).symm (Category.id_comp _).symm

Canonical Morphism Between Pullbacks via Base Change

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to S$, $g \colon Y \to S$, and $i \colon S \to T$ in $\mathcal{C}$ such that the pullbacks $X \times_S Y$ and $X \times_T Y$ exist, there exists a canonical morphism $X \times_S Y \to X \times_T Y$ induced by the composition of $f$ and $g$ with $i$.

CategoryTheory.Limits.pullback.map_comp theorem

 {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₁ e₂ e₃ e₄) :
  pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ ≫ pullback.map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄ =
    pullback.map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) (by rw [reassoc_of% e₁, e₃, Category.assoc])
      (by rw [reassoc_of% e₂, e₄, Category.assoc])

Full source

@[reassoc]
lemma pullback.map_comp {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₁ e₂ e₃ e₄) :
    pullback.mappullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ ≫ pullback.map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄ =
      pullback.map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃)
        (by rw [reassoc_of% e₁, e₃, Category.assoc])
        (by rw [reassoc_of% e₂, e₄, Category.assoc]) := by ext <;> simp

Composition of Induced Pullback Maps via Commutative Diagrams

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$, $g \colon Y \to Z$, $f' \colon X' \to Z'$, $g' \colon Y' \to Z'$, $f'' \colon X'' \to Z''$, $g'' \colon Y'' \to Z''$ with pullbacks existing for each pair, and morphisms $i_1 \colon X \to X'$, $j_1 \colon X' \to X''$, $i_2 \colon Y \to Y'$, $j_2 \colon Y' \to Y''$, $i_3 \colon Z \to Z'$, $j_3 \colon Z' \to Z''$ such that the diagrams commute, the composition of the induced pullback maps satisfies: \[ \text{pullback.map}\, f\, g\, f'\, g'\, i_1\, i_2\, i_3\, e_1\, e_2 \circ \text{pullback.map}\, f'\, g'\, f''\, g''\, j_1\, j_2\, j_3\, e_3\, e_4 = \text{pullback.map}\, f\, g\, f''\, g''\, (i_1 \circ j_1)\, (i_2 \circ j_2)\, (i_3 \circ j_3)\, e_1'\, e_2' \] where $e_1'$ and $e_2'$ are the natural commutativity conditions obtained from $e_1, e_3$ and $e_2, e_4$ respectively.

CategoryTheory.Limits.pullback.map_id theorem

 {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] :
  pullback.map f g f g (𝟙 _) (𝟙 _) (𝟙 _) (by simp) (by simp) = 𝟙 _

Full source

@[simp]
lemma pullback.map_id {X Y Z : C}
    {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] :
    pullback.map f g f g (𝟙 _) (𝟙 _) (𝟙 _) (by simp) (by simp) = 𝟙 _ := by ext <;> simp

Identity Morphism is Preserved by Pullback Construction

Informal description

Let $\mathcal{C}$ be a category with morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ that have a pullback. The induced morphism between the pullback of $f$ and $g$ with itself, via the identity morphisms on $X$, $Y$, and $Z$, is equal to the identity morphism on the pullback object. That is, the following diagram commutes: \[ \begin{tikzcd} X \times_Z Y \arrow[r, "\mathrm{id}"] \arrow[d, "\mathrm{id}"'] & X \times_Z Y \arrow[d, "\mathrm{id}"] \\ X \times_Z Y \arrow[r, "\mathrm{id}"'] & X \times_Z Y \end{tikzcd} \]

CategoryTheory.Limits.pushout.map abbrev

 {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₁ : f₁ ≫ i₁ = i₃ ≫ g₁) (eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂) :
  pushout f₁ f₂ ⟶ pushout g₁ g₂

Full source

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

```
  W ⟶ Y
 ↗   ↗
S ⟶ T
 ↘   ↘
  X ⟶ Z
```
-/
abbrev pushout.map {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₁ : f₁ ≫ i₁ = i₃ ≫ g₁)
    (eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂) : pushoutpushout f₁ f₂ ⟶ pushout g₁ g₂ :=
  pushout.desc (i₁ ≫ pushout.inl _ _) (i₂ ≫ pushout.inr _ _)
    (by simp only [reassoc_of% eq₁, reassoc_of% eq₂, condition])

Induced Morphism Between Pushouts via Compatible Diagrams

Informal description

Given a category $\mathcal{C}$ and commutative diagrams \[ \begin{CD} S @>{f_1}>> W \\ @V{f_2}VV @VV{i_1}V \\ X @>>{i_2}> Y \end{CD} \quad \text{and} \quad \begin{CD} T @>{g_1}>> Y \\ @V{g_2}VV @VV{j_1}V \\ Z @>>{j_2}> Z \end{CD} \] with pushouts $\text{pushout}(f_1, f_2)$ and $\text{pushout}(g_1, g_2)$, respectively, and given morphisms $i_1 \colon W \to Y$, $i_2 \colon X \to Z$, and $i_3 \colon S \to T$ satisfying $f_1 \circ i_1 = i_3 \circ g_1$ and $f_2 \circ i_2 = i_3 \circ g_2$, there exists a unique morphism $\text{pushout.map}\, f_1\, f_2\, g_1\, g_2\, i_1\, i_2\, i_3\, \text{eq}_1\, \text{eq}_2 \colon \text{pushout}(f_1, f_2) \to \text{pushout}(g_1, g_2)$ making the induced diagram commute.

CategoryTheory.Limits.pushout.mapLift abbrev

 {X Y S T : C} (f : T ⟶ X) (g : T ⟶ Y) (i : S ⟶ T) [HasPushout f g] [HasPushout (i ≫ f) (i ≫ g)] :
  pushout (i ≫ f) (i ≫ g) ⟶ pushout f g

Full source

/-- The canonical map `X ⨿ₛ Y ⟶ X ⨿ₜ Y` given `S ⟶ T`. -/
abbrev pushout.mapLift {X Y S T : C} (f : T ⟶ X) (g : T ⟶ Y) (i : S ⟶ T) [HasPushout f g]
    [HasPushout (i ≫ f) (i ≫ g)] : pushoutpushout (i ≫ f) (i ≫ g) ⟶ pushout f g :=
  pushout.map (i ≫ f) (i ≫ g) f g (𝟙 _) (𝟙 _) i (Category.comp_id _) (Category.comp_id _)

Canonical Morphism from Pushout of Composed Morphisms to Pushout of Original Morphisms

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon T \to X$, $g \colon T \to Y$, and $i \colon S \to T$ in $\mathcal{C}$, if pushouts exist for both $(f, g)$ and $(i \circ f, i \circ g)$, then there exists a canonical morphism $\text{pushout}(i \circ f, i \circ g) \to \text{pushout}(f, g)$ induced by the universal property of the pushout.

CategoryTheory.Limits.pushout.map_comp theorem

 {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₁ e₂ e₃ e₄) :
  pushout.map f g f' g' i₂ i₃ i₁ e₁ e₂ ≫ pushout.map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄ =
    pushout.map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) (by rw [reassoc_of% e₁, e₃, Category.assoc])
      (by rw [reassoc_of% e₂, e₄, Category.assoc])

Full source

@[reassoc]
lemma pushout.map_comp {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₁ e₂ e₃ e₄) :
    pushout.mappushout.map f g f' g' i₂ i₃ i₁ e₁ e₂ ≫ pushout.map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄ =
      pushout.map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁)
        (by rw [reassoc_of% e₁, e₃, Category.assoc])
        (by rw [reassoc_of% e₂, e₄, Category.assoc]) := by ext <;> simp

Composition of Induced Pushout Maps

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$, $g \colon X \to Z$ with pushouts, along with morphisms $f' \colon X' \to Y'$, $g' \colon X' \to Z'$ and $f'' \colon X'' \to Y''$, $g'' \colon X'' \to Z''$ with their respective pushouts, and morphisms $i_1 \colon X \to X'$, $j_1 \colon X' \to X''$, $i_2 \colon Y \to Y'$, $j_2 \colon Y' \to Y''$, $i_3 \colon Z \to Z'$, $j_3 \colon Z' \to Z''$ satisfying the commuting conditions $e_1$, $e_2$, $e_3$, $e_4$, the composition of the induced pushout maps satisfies: \[ \text{pushout.map}\, f\, g\, f'\, g'\, i_2\, i_3\, i_1\, e_1\, e_2 \circ \text{pushout.map}\, f'\, g'\, f''\, g''\, j_2\, j_3\, j_1\, e_3\, e_4 = \text{pushout.map}\, f\, g\, f''\, g''\, (i_2 \circ j_2)\, (i_3 \circ j_3)\, (i_1 \circ j_1)\, \text{(adjusted conditions)} \]

CategoryTheory.Limits.pushout.map_id theorem

 {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] : pushout.map f g f g (𝟙 _) (𝟙 _) (𝟙 _) (by simp) (by simp) = 𝟙 _

Full source

@[simp]
lemma pushout.map_id {X Y Z : C}
    {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] :
    pushout.map f g f g (𝟙 _) (𝟙 _) (𝟙 _) (by simp) (by simp) = 𝟙 _ := by ext <;> simp

Identity Morphism is Preserved by Pushout Mapping

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ that have a pushout, the induced morphism $\text{pushout.map}(f, g, f, g, \text{id}_Y, \text{id}_Z, \text{id}_X)$ (where all three identity morphisms satisfy the required commuting conditions) is equal to the identity morphism on $\text{pushout}(f, g)$.

CategoryTheory.Limits.pullback.map_isIso instance

 {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₁ : f₁ ≫ i₃ = i₁ ≫ g₁) (eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) [IsIso i₁] [IsIso i₂]
  [IsIso i₃] : IsIso (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)

Full source

instance pullback.map_isIso {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₁ : f₁ ≫ i₃ = i₁ ≫ g₁) (eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) [IsIso i₁] [IsIso i₂] [IsIso i₃] :
    IsIso (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) := by
  refine ⟨⟨pullback.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
  · rw [IsIso.comp_inv_eq, Category.assoc, eq₁, IsIso.inv_hom_id_assoc]
  · rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]
  · aesop_cat
  · aesop_cat

Induced Pullback Map is an Isomorphism when Component Maps are Isomorphisms

Informal description

Given a category $\mathcal{C}$ and commutative diagrams \[ \begin{tikzcd} W \arrow[r, "f_1"] \arrow[d, "i_1"'] & S \arrow[d, "i_3"] \\ Y \arrow[r, "g_1"'] & T \end{tikzcd} \quad \text{and} \quad \begin{tikzcd} X \arrow[r, "f_2"] \arrow[d, "i_2"'] & S \arrow[d, "i_3"] \\ Z \arrow[r, "g_2"'] & T \end{tikzcd} \] where the pullbacks $W \times_S X$ and $Y \times_T Z$ exist, if $i_1$, $i_2$, and $i_3$ are isomorphisms, then the induced morphism $W \times_S X \to Y \times_T Z$ is also an isomorphism.

CategoryTheory.Limits.pullback.congrHom definition

 {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₂

Full source

/-- If `f₁ = f₂` and `g₁ = g₂`, we may construct a canonical
isomorphism `pullback f₁ g₁ ≅ pullback f₂ g₂` -/
@[simps! hom]
def pullback.congrHom {X Y Z : C} {f₁ f₂ : X ⟶ Z} {g₁ g₂ : Y ⟶ Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂)
    [HasPullback f₁ g₁] [HasPullback f₂ g₂] : pullbackpullback f₁ g₁ ≅ pullback f₂ g₂ :=
  asIso <| pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simp [h₁]) (by simp [h₂])

Canonical isomorphism between pullbacks of equal morphisms

Informal description

Given a category $\mathcal{C}$ and morphisms $f_1, f_2 \colon X \to Z$ and $g_1, g_2 \colon Y \to Z$ in $\mathcal{C}$ such that $f_1 = f_2$ and $g_1 = g_2$, and assuming that the pullbacks of both pairs $(f_1, g_1)$ and $(f_2, g_2)$ exist, there exists a canonical isomorphism between the pullback objects $\text{pullback}(f_1, g_1) \cong \text{pullback}(f_2, g_2)$. This isomorphism is constructed using the identity morphisms on $X$, $Y$, and $Z$.

CategoryTheory.Limits.pullback.congrHom_inv theorem

 {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.congrHom h₁ h₂).inv = pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simp [h₁]) (by simp [h₂])

Full source

@[simp]
theorem pullback.congrHom_inv {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.congrHom h₁ h₂).inv =
      pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simp [h₁]) (by simp [h₂]) := by
  ext <;> simp [Iso.inv_comp_eq]

Inverse of Pullback Isomorphism Equals Identity-Induced Map

Informal description

Given a category $\mathcal{C}$ and morphisms $f_1, f_2 \colon X \to Z$ and $g_1, g_2 \colon Y \to Z$ such that $f_1 = f_2$ and $g_1 = g_2$, and assuming that the pullbacks of both pairs $(f_1, g_1)$ and $(f_2, g_2)$ exist, the inverse of the canonical isomorphism $\text{pullback}(f_1, g_1) \cong \text{pullback}(f_2, g_2)$ is equal to the pullback map induced by the identity morphisms on $X$, $Y$, and $Z$.

CategoryTheory.Limits.pushout.map_isIso instance

 {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₁ : f₁ ≫ i₁ = i₃ ≫ g₁) (eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂) [IsIso i₁] [IsIso i₂]
  [IsIso i₃] : IsIso (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)

Full source

instance pushout.map_isIso {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₁ : f₁ ≫ i₁ = i₃ ≫ g₁) (eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂) [IsIso i₁] [IsIso i₂] [IsIso i₃] :
    IsIso (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) := by
  refine ⟨⟨pushout.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
  · rw [IsIso.comp_inv_eq, Category.assoc, eq₁, IsIso.inv_hom_id_assoc]
  · rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]
  · aesop_cat
  · aesop_cat

Isomorphism of Pushouts via Isomorphic Diagrams

Informal description

Given a category $\mathcal{C}$ and commutative diagrams \[ \begin{CD} S @>{f_1}>> W \\ @V{f_2}VV @VV{i_1}V \\ X @>>{i_2}> Y \end{CD} \quad \text{and} \quad \begin{CD} T @>{g_1}>> Y \\ @V{g_2}VV @VV{j_1}V \\ Z @>>{j_2}> Z \end{CD} \] with pushouts $\text{pushout}(f_1, f_2)$ and $\text{pushout}(g_1, g_2)$, respectively, and given morphisms $i_1 \colon W \to Y$, $i_2 \colon X \to Z$, and $i_3 \colon S \to T$ that are isomorphisms and satisfy $f_1 \circ i_1 = i_3 \circ g_1$ and $f_2 \circ i_2 = i_3 \circ g_2$, the induced morphism $\text{pushout.map}\, f_1\, f_2\, g_1\, g_2\, i_1\, i_2\, i_3$ is also an isomorphism.

CategoryTheory.Limits.pullback.mapDesc_comp theorem

 {X Y S T S' : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) (i' : S ⟶ S') [HasPullback f g] [HasPullback (f ≫ i) (g ≫ i)]
  [HasPullback (f ≫ i ≫ i') (g ≫ i ≫ i')] [HasPullback ((f ≫ i) ≫ i') ((g ≫ i) ≫ i')] :
  pullback.mapDesc f g (i ≫ i') =
    pullback.mapDesc f g i ≫
      pullback.mapDesc _ _ i' ≫ (pullback.congrHom (Category.assoc _ _ _) (Category.assoc _ _ _)).hom

Full source

theorem pullback.mapDesc_comp {X Y S T S' : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) (i' : S ⟶ S')
    [HasPullback f g] [HasPullback (f ≫ i) (g ≫ i)] [HasPullback (f ≫ i ≫ i') (g ≫ i ≫ i')]
    [HasPullback ((f ≫ i) ≫ i') ((g ≫ i) ≫ i')] :
    pullback.mapDesc f g (i ≫ i') = pullback.mapDescpullback.mapDesc f g i ≫ pullback.mapDesc _ _ i' ≫
    (pullback.congrHom (Category.assoc _ _ _) (Category.assoc _ _ _)).hom := by
  aesop_cat

Factorization of Pullback Base Change Morphism via Composition

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to T$, $g \colon Y \to T$, $i \colon T \to S$, and $i' \colon S \to S'$ such that the pullbacks $X \times_T Y$, $X \times_S Y$, $X \times_{S'} Y$, and $X \times_{S'} Y$ (via the compositions $(f \circ i) \circ i'$ and $(g \circ i) \circ i'$) exist, the canonical morphism $\text{pullback.mapDesc}\, f\, g\, (i \circ i')$ from $X \times_T Y$ to $X \times_{S'} Y$ factors as the composition of: 1. $\text{pullback.mapDesc}\, f\, g\, i$ from $X \times_T Y$ to $X \times_S Y$, 2. $\text{pullback.mapDesc}\, (f \circ i)\, (g \circ i)\, i'$ from $X \times_S Y$ to $X \times_{S'} Y$, and 3. The isomorphism $\text{pullback.congrHom}$ induced by associativity of composition.

CategoryTheory.Limits.pushout.congrHom definition

 {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₂

Full source

/-- If `f₁ = f₂` and `g₁ = g₂`, we may construct a canonical
isomorphism `pushout f₁ g₁ ≅ pullback f₂ g₂` -/
@[simps! hom]
def pushout.congrHom {X Y Z : C} {f₁ f₂ : X ⟶ Y} {g₁ g₂ : X ⟶ Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂)
    [HasPushout f₁ g₁] [HasPushout f₂ g₂] : pushoutpushout f₁ g₁ ≅ pushout f₂ g₂ :=
  asIso <| pushout.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simp [h₁]) (by simp [h₂])

Canonical isomorphism between pushouts of equal morphisms

Informal description

Given a category $\mathcal{C}$ and morphisms $f_1, f_2 \colon X \to Y$ and $g_1, g_2 \colon X \to Z$ such that $f_1 = f_2$ and $g_1 = g_2$, and assuming pushouts of $(f_1, g_1)$ and $(f_2, g_2)$ exist, there is a canonical isomorphism $\text{pushout}(f_1, g_1) \cong \text{pushout}(f_2, g_2)$ induced by the identity morphisms on $X$, $Y$, and $Z$.

CategoryTheory.Limits.pushout.congrHom_inv theorem

 {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.congrHom h₁ h₂).inv = pushout.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simp [h₁]) (by simp [h₂])

Full source

@[simp]
theorem pushout.congrHom_inv {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.congrHom h₁ h₂).inv =
      pushout.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simp [h₁]) (by simp [h₂]) := by
  ext <;> simp [Iso.comp_inv_eq]

Inverse of Pushout Isomorphism for Equal Morphisms

Informal description

Given a category $\mathcal{C}$ and morphisms $f_1, f_2 \colon X \to Y$ and $g_1, g_2 \colon X \to Z$ such that $f_1 = f_2$ and $g_1 = g_2$, and assuming pushouts of $(f_1, g_1)$ and $(f_2, g_2)$ exist, the inverse of the canonical isomorphism $\text{pushout}(f_1, g_1) \cong \text{pushout}(f_2, g_2)$ is equal to the morphism induced by the identity morphisms on $X$, $Y$, and $Z$ via the pushout universal property.

CategoryTheory.Limits.pushout.mapLift_comp theorem

 {X Y S T S' : C} (f : T ⟶ X) (g : T ⟶ Y) (i : S ⟶ T) (i' : S' ⟶ S) [HasPushout f g] [HasPushout (i ≫ f) (i ≫ g)]
  [HasPushout (i' ≫ i ≫ f) (i' ≫ i ≫ g)] [HasPushout ((i' ≫ i) ≫ f) ((i' ≫ i) ≫ g)] :
  pushout.mapLift f g (i' ≫ i) =
    (pushout.congrHom (Category.assoc _ _ _) (Category.assoc _ _ _)).hom ≫
      pushout.mapLift _ _ i' ≫ pushout.mapLift f g i

Full source

theorem pushout.mapLift_comp {X Y S T S' : C} (f : T ⟶ X) (g : T ⟶ Y) (i : S ⟶ T) (i' : S' ⟶ S)
    [HasPushout f g] [HasPushout (i ≫ f) (i ≫ g)] [HasPushout (i' ≫ i ≫ f) (i' ≫ i ≫ g)]
    [HasPushout ((i' ≫ i) ≫ f) ((i' ≫ i) ≫ g)] :
    pushout.mapLift f g (i' ≫ i) =
      (pushout.congrHom (Category.assoc _ _ _) (Category.assoc _ _ _)).hom ≫
        pushout.mapLift _ _ i' ≫ pushout.mapLift f g i := by
  aesop_cat

Composition Law for Pushout MapLift Morphisms

Informal description

Let $\mathcal{C}$ be a category with morphisms $f \colon T \to X$ and $g \colon T \to Y$, and let $i \colon S \to T$ and $i' \colon S' \to S$ be additional morphisms. Suppose the pushouts $\text{pushout}(f, g)$, $\text{pushout}(i \circ f, i \circ g)$, $\text{pushout}(i' \circ i \circ f, i' \circ i \circ g)$, and $\text{pushout}((i' \circ i) \circ f, (i' \circ i) \circ g)$ all exist. Then the canonical morphism $\text{pushout.mapLift}\, f\, g\, (i' \circ i)$ is equal to the composition of: 1. The isomorphism $\text{pushout.congrHom}\, (\text{assoc}\, i'\, i\, f)\, (\text{assoc}\, i'\, i\, g)$, 2. The morphism $\text{pushout.mapLift}\, (i \circ f)\, (i \circ g)\, i'$, and 3. The morphism $\text{pushout.mapLift}\, f\, g\, i$. In other words, the following diagram commutes: \[ \text{pushout.mapLift}\, f\, g\, (i' \circ i) = \text{pushout.congrHom}\, (\text{assoc}\, i'\, i\, f)\, (\text{assoc}\, i'\, i\, g) \circ \text{pushout.mapLift}\, (i \circ f)\, (i \circ g)\, i' \circ \text{pushout.mapLift}\, f\, g\, i. \]

CategoryTheory.Limits.pullbackComparison definition

 (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)

Full source

/-- 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`
-/
def pullbackComparison (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) :=
  pullback.lift (G.map (pullback.fst f g)) (G.map (pullback.snd f g))
    (by simp only [← G.map_comp, pullback.condition])

Pullback comparison morphism induced by a functor

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ that have a pullback, the pullback comparison morphism is the canonical morphism from $G(\text{pullback}(f, g))$ to the pullback of $G(f)$ and $G(g)$ in $\mathcal{D}$. This morphism is constructed using the universal property of the pullback in $\mathcal{D}$, ensuring that the following diagram commutes: \[ \begin{tikzcd} G(\text{pullback}(f, g)) \arrow[dr, dashed, "\text{pullbackComparison}\,G\,f\,g"] \arrow[ddr, "G(\pi_2)"'] \arrow[drr, "G(\pi_1)"] & & \\ & \text{pullback}(G(f), G(g)) \arrow[r, "\pi_1"] \arrow[d, "\pi_2"'] & G(X) \arrow[d, "G(f)"] \\ & G(Y) \arrow[r, "G(g)"'] & G(Z) \end{tikzcd} \] where $\pi_1$ and $\pi_2$ are the projection morphisms from the pullback object.

CategoryTheory.Limits.pullbackComparison_comp_fst theorem

 (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPullback (G.map f) (G.map g)] :
  pullbackComparison G f g ≫ pullback.fst _ _ = G.map (pullback.fst f g)

Full source

@[reassoc (attr := simp)]
theorem pullbackComparison_comp_fst (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]
    [HasPullback (G.map f) (G.map g)] :
    pullbackComparisonpullbackComparison G f g ≫ pullback.fst _ _ = G.map (pullback.fst f g) :=
  pullback.lift_fst _ _ _

Commutativity of Pullback Comparison with First Projection: $\text{pullbackComparison}\,G\,f\,g \circ \pi_1 = G(\pi_1)$

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ that have pullbacks, the composition of the pullback comparison morphism $\text{pullbackComparison}\,G\,f\,g$ with the first projection $\pi_1$ from the pullback of $G(f)$ and $G(g)$ in $\mathcal{D}$ equals the image under $G$ of the first projection $\pi_1$ from the pullback of $f$ and $g$ in $\mathcal{C}$. That is, the following diagram commutes: \[ \text{pullbackComparison}\,G\,f\,g \circ \pi_1 = G(\pi_1). \]

CategoryTheory.Limits.pullbackComparison_comp_snd theorem

 (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPullback (G.map f) (G.map g)] :
  pullbackComparison G f g ≫ pullback.snd _ _ = G.map (pullback.snd f g)

Full source

@[reassoc (attr := simp)]
theorem pullbackComparison_comp_snd (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]
    [HasPullback (G.map f) (G.map g)] :
    pullbackComparisonpullbackComparison G f g ≫ pullback.snd _ _ = G.map (pullback.snd f g):=
  pullback.lift_snd _ _ _

Commutativity of pullback comparison with second projection

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ that have pullbacks in both $\mathcal{C}$ and $\mathcal{D}$, the composition of the pullback comparison morphism $\text{pullbackComparison}\,G\,f\,g$ with the second projection $\pi_2 \colon \text{pullback}(G(f), G(g)) \to G(Y)$ equals the image under $G$ of the second projection $\pi_2 \colon \text{pullback}(f, g) \to Y$ in $\mathcal{C}$. That is, the following diagram commutes: \[ \begin{tikzcd} G(\text{pullback}(f, g)) \arrow[r, "\text{pullbackComparison}\,G\,f\,g"] \arrow[dr, "G(\pi_2)"'] & \text{pullback}(G(f), G(g)) \arrow[d, "\pi_2"] \\ & G(Y) \end{tikzcd} \]

CategoryTheory.Limits.map_lift_pullbackComparison theorem

 (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 : h ≫ f = k ≫ g) :
  G.map (pullback.lift _ _ w) ≫ pullbackComparison G f g =
    pullback.lift (G.map h) (G.map k) (by simp only [← G.map_comp, w])

Full source

@[reassoc (attr := simp)]
theorem map_lift_pullbackComparison (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 : h ≫ f = k ≫ g) :
    G.map (pullback.lift _ _ w) ≫ pullbackComparison G f g =
      pullback.lift (G.map h) (G.map k) (by simp only [← G.map_comp, w]) := by
  ext <;> simp [← G.map_comp]

Commuting Diagram for Functoriality of Pullback Lifts: $G(\text{lift}) \circ \text{comparison} = \text{lift}(G(h), G(k))$

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor. Given morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ that have pullbacks in both $\mathcal{C}$ and $\mathcal{D}$, and given morphisms $h \colon W \to X$ and $k \colon W \to Y$ in $\mathcal{C}$ such that $h \circ f = k \circ g$, the following diagram commutes: \[ G(\text{pullback.lift}\, h\, k\, w) \circ \text{pullbackComparison}\, G\, f\, g = \text{pullback.lift}\, (G(h))\, (G(k))\, (\text{by simp only } [\leftarrow G.\text{map\_comp}, w]) \] where $w$ is the proof that $h \circ f = k \circ g$, and $\text{pullbackComparison}\, G\, f\, g$ is the canonical morphism from $G(\text{pullback}(f, g))$ to $\text{pullback}(G(f), G(g))$ in $\mathcal{D}$.

CategoryTheory.Limits.pushoutComparison definition

 (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)

Full source

/-- 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`
-/
def pushoutComparison (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] :
    pushoutpushout (G.map f) (G.map g) ⟶ G.obj (pushout f g) :=
  pushout.desc (G.map (pushout.inl _ _)) (G.map (pushout.inr _ _))
    (by simp only [← G.map_comp, pushout.condition])

Pushout comparison morphism

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ that admit pushouts in both $\mathcal{C}$ and $\mathcal{D}$, the pushout comparison morphism is the canonical morphism from the pushout of $G(f)$ and $G(g)$ in $\mathcal{D}$ to the image under $G$ of the pushout of $f$ and $g$ in $\mathcal{C}$. This morphism is induced by the universal property of the pushout in $\mathcal{D}$ applied to the images under $G$ of the canonical inclusions into the pushout in $\mathcal{C}$.

CategoryTheory.Limits.inl_comp_pushoutComparison theorem

 (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] :
  pushout.inl _ _ ≫ pushoutComparison G f g = G.map (pushout.inl _ _)

Full source

@[reassoc (attr := simp)]
theorem inl_comp_pushoutComparison (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g]
    [HasPushout (G.map f) (G.map g)] : pushout.inlpushout.inl _ _ ≫ pushoutComparison G f g =
      G.map (pushout.inl _ _) :=
  pushout.inl_desc _ _ _

Commutativity of Left Pushout Inclusion with Pushout Comparison Morphism

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ that admit pushouts in both $\mathcal{C}$ and $\mathcal{D}$, the composition of the left inclusion $\iota_1 \colon Y \to \mathrm{pushout}(G(f), G(g))$ with the pushout comparison morphism $\mathrm{pushoutComparison}\,G\,f\,g \colon \mathrm{pushout}(G(f), G(g)) \to G(\mathrm{pushout}(f,g))$ equals the image under $G$ of the left inclusion $\iota_1 \colon Y \to \mathrm{pushout}(f,g)$, i.e., \[ \iota_1 \circ \mathrm{pushoutComparison}\,G\,f\,g = G(\iota_1). \]

CategoryTheory.Limits.inr_comp_pushoutComparison theorem

 (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] :
  pushout.inr _ _ ≫ pushoutComparison G f g = G.map (pushout.inr _ _)

Full source

@[reassoc (attr := simp)]
theorem inr_comp_pushoutComparison (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g]
    [HasPushout (G.map f) (G.map g)] : pushout.inrpushout.inr _ _ ≫ pushoutComparison G f g =
      G.map (pushout.inr _ _) :=
  pushout.inr_desc _ _ _

Commutativity of Right Inclusion with Pushout Comparison Morphism

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ that admit pushouts in both $\mathcal{C}$ and $\mathcal{D}$, the composition of the right inclusion morphism $\iota_r \colon Z \to \text{pushout}(G(f), G(g))$ with the pushout comparison morphism $\text{pushoutComparison}(G, f, g) \colon \text{pushout}(G(f), G(g)) \to G(\text{pushout}(f, g))$ equals the image under $G$ of the right inclusion morphism $G(\iota_r) \colon G(Z) \to G(\text{pushout}(f, g))$. That is, the following diagram commutes: \[ \iota_r \circ \text{pushoutComparison}(G, f, g) = G(\iota_r). \]

CategoryTheory.Limits.pushoutComparison_map_desc theorem

 (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 : f ≫ h = g ≫ k) :
  pushoutComparison G f g ≫ G.map (pushout.desc _ _ w) =
    pushout.desc (G.map h) (G.map k) (by simp only [← G.map_comp, w])

Full source

@[reassoc (attr := simp)]
theorem pushoutComparison_map_desc (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 : f ≫ h = g ≫ k) :
    pushoutComparisonpushoutComparison G f g ≫ G.map (pushout.desc _ _ w) =
      pushout.desc (G.map h) (G.map k) (by simp only [← G.map_comp, w]) := by
  ext <;> simp [← G.map_comp]

Commutativity of Pushout Comparison with Descending Morphism via Functor $G$

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ that admit pushouts in both $\mathcal{C}$ and $\mathcal{D}$, for any object $W$ in $\mathcal{C}$ and morphisms $h \colon Y \to W$ and $k \colon Z \to W$ satisfying $f \circ h = g \circ k$, the following diagram commutes: \[ \text{pushoutComparison}(G, f, g) \circ G(\text{pushout.desc}(h, k, w)) = \text{pushout.desc}(G(h), G(k), \text{by simp only } [\leftarrow G.\text{map\_comp}, w]) \]

CategoryTheory.Limits.hasPullback_symmetry theorem

[HasPullback f g] : HasPullback g f

Full source

/-- Making this a global instance would make the typeclass search go in an infinite loop. -/
theorem hasPullback_symmetry [HasPullback f g] : HasPullback g f :=
  ⟨⟨⟨_, PullbackCone.flipIsLimit (pullbackIsPullback f g)⟩⟩⟩

Existence of Pullback is Symmetric in $f$ and $g$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$, if the pullback of $f$ and $g$ exists (i.e., $\text{HasPullback}(f, g)$ holds), then the pullback of $g$ and $f$ also exists (i.e., $\text{HasPullback}(g, f)$ holds).

CategoryTheory.Limits.pullbackSymmetry definition

[HasPullback f g] : pullback f g ≅ pullback g f

Full source

/-- The isomorphism `X ×[Z] Y ≅ Y ×[Z] X`. -/
def pullbackSymmetry [HasPullback f g] : pullbackpullback f g ≅ pullback g f :=
  IsLimit.conePointUniqueUpToIso
    (PullbackCone.flipIsLimit (pullbackIsPullback f g)) (limit.isLimit _)

Natural isomorphism between pullback(f,g) and pullback(g,f)

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ that have a pullback, there exists a natural isomorphism $\text{pullback}(f,g) \cong \text{pullback}(g,f)$ between their pullback objects. This isomorphism swaps the projection morphisms, satisfying: - The isomorphism composed with the first projection of $\text{pullback}(g,f)$ equals the second projection of $\text{pullback}(f,g)$ - The isomorphism composed with the second projection of $\text{pullback}(g,f)$ equals the first projection of $\text{pullback}(f,g)$

CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst theorem

[HasPullback f g] : (pullbackSymmetry f g).hom ≫ pullback.fst g f = pullback.snd f g

Full source

@[reassoc (attr := simp)]
theorem pullbackSymmetry_hom_comp_fst [HasPullback f g] :
    (pullbackSymmetry f g).hom ≫ pullback.fst g f = pullback.snd f g := by simp [pullbackSymmetry]

Compatibility of pullback symmetry isomorphism with first projection: $\varphi \circ \pi_1' = \pi_2$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ that have a pullback, the homomorphism part of the pullback symmetry isomorphism $\text{pullback}(f,g) \cong \text{pullback}(g,f)$ satisfies: \[ \varphi \circ \pi_1' = \pi_2 \] where: - $\varphi$ is the isomorphism $\text{pullback}(f,g) \to \text{pullback}(g,f)$ - $\pi_1'$ is the first projection from $\text{pullback}(g,f)$ to $Y$ - $\pi_2$ is the second projection from $\text{pullback}(f,g)$ to $Y$

CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd theorem

[HasPullback f g] : (pullbackSymmetry f g).hom ≫ pullback.snd g f = pullback.fst f g

Full source

@[reassoc (attr := simp)]
theorem pullbackSymmetry_hom_comp_snd [HasPullback f g] :
    (pullbackSymmetry f g).hom ≫ pullback.snd g f = pullback.fst f g := by simp [pullbackSymmetry]

Compatibility of pullback symmetry isomorphism with projections: $\varphi \circ \pi_2 = \pi_1$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ that have a pullback, the homomorphism part of the natural isomorphism $\text{pullback}(f,g) \cong \text{pullback}(g,f)$, when composed with the second projection $\pi_2 \colon \text{pullback}(g,f) \to Y$, equals the first projection $\pi_1 \colon \text{pullback}(f,g) \to X$.

CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst theorem

[HasPullback f g] : (pullbackSymmetry f g).inv ≫ pullback.fst f g = pullback.snd g f

Full source

@[reassoc (attr := simp)]
theorem pullbackSymmetry_inv_comp_fst [HasPullback f g] :
    (pullbackSymmetry f g).inv ≫ pullback.fst f g = pullback.snd g f := by simp [Iso.inv_comp_eq]

Pullback symmetry isomorphism inverse compatibility with first projection: $\varphi^{-1} \circ \pi_1 = \pi_2'$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ that have a pullback, the inverse of the pullback symmetry isomorphism $\text{pullback}(f,g) \cong \text{pullback}(g,f)$, when composed with the first projection $\pi_1 \colon \text{pullback}(f,g) \to X$, equals the second projection $\pi_2' \colon \text{pullback}(g,f) \to X$. In symbols: \[ \varphi^{-1} \circ \pi_1 = \pi_2' \] where: - $\varphi^{-1}$ is the inverse isomorphism $\text{pullback}(g,f) \to \text{pullback}(f,g)$ - $\pi_1$ is the first projection from $\text{pullback}(f,g)$ to $X$ - $\pi_2'$ is the second projection from $\text{pullback}(g,f)$ to $X$

CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd theorem

[HasPullback f g] : (pullbackSymmetry f g).inv ≫ pullback.snd f g = pullback.fst g f

Full source

@[reassoc (attr := simp)]
theorem pullbackSymmetry_inv_comp_snd [HasPullback f g] :
    (pullbackSymmetry f g).inv ≫ pullback.snd f g = pullback.fst g f := by simp [Iso.inv_comp_eq]

Compatibility of pullback symmetry inverse with second projection: $\varphi^{-1} \circ \pi_2 = \pi_1'$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$ that have a pullback, the inverse of the pullback symmetry isomorphism $\text{pullback}(f,g) \cong \text{pullback}(g,f)$ satisfies: \[ \varphi^{-1} \circ \pi_2 = \pi_1' \] where: - $\varphi^{-1}$ is the inverse isomorphism $\text{pullback}(g,f) \to \text{pullback}(f,g)$ - $\pi_2$ is the second projection from $\text{pullback}(f,g)$ to $Y$ - $\pi_1'$ is the first projection from $\text{pullback}(g,f)$ to $X$

CategoryTheory.Limits.hasPushout_symmetry theorem

[HasPushout f g] : HasPushout g f

Full source

/-- Making this a global instance would make the typeclass search go in an infinite loop. -/
theorem hasPushout_symmetry [HasPushout f g] : HasPushout g f :=
  ⟨⟨⟨_, PushoutCocone.flipIsColimit (pushoutIsPushout f g)⟩⟩⟩

Existence of Pushout is Symmetric in $f$ and $g$

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ such that the pushout of $f$ and $g$ exists, then the pushout of $g$ and $f$ also exists.

CategoryTheory.Limits.pushoutSymmetry definition

[HasPushout f g] : pushout f g ≅ pushout g f

Full source

/-- The isomorphism `Y ⨿[X] Z ≅ Z ⨿[X] Y`. -/
def pushoutSymmetry [HasPushout f g] : pushoutpushout f g ≅ pushout g f :=
  IsColimit.coconePointUniqueUpToIso
    (PushoutCocone.flipIsColimit (pushoutIsPushout f g)) (colimit.isColimit _)

Natural isomorphism between pushout objects with swapped morphisms

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ for which a pushout exists, there is a natural isomorphism $\text{pushout}(f, g) \cong \text{pushout}(g, f)$ between the pushout objects obtained by swapping the roles of $f$ and $g$. This isomorphism makes the following diagram commute: \[ \begin{CD} Y @>{\iota_1}>> \text{pushout}(f, g) \\ @V{\iota_2}VV @VV{\cong}V \\ Z @>>{\iota_1}> \text{pushout}(g, f) \end{CD} \] where $\iota_1$ and $\iota_2$ are the canonical inclusion morphisms into the respective pushout objects.

CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom theorem

[HasPushout f g] : pushout.inl _ _ ≫ (pushoutSymmetry f g).hom = pushout.inr _ _

Full source

@[reassoc (attr := simp)]
theorem inl_comp_pushoutSymmetry_hom [HasPushout f g] :
    pushout.inlpushout.inl _ _ ≫ (pushoutSymmetry f g).hom = pushout.inr _ _ :=
  (colimit.isColimit (span f g)).comp_coconePointUniqueUpToIso_hom
    (PushoutCocone.flipIsColimit (pushoutIsPushout g f)) _

Compatibility of pushout symmetry with left inclusion

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ for which a pushout exists, the composition of the left inclusion morphism $\iota_1 \colon Y \to \text{pushout}(f, g)$ with the isomorphism $\text{pushoutSymmetry}(f, g).\text{hom} \colon \text{pushout}(f, g) \to \text{pushout}(g, f)$ equals the right inclusion morphism $\iota_2 \colon Z \to \text{pushout}(g, f)$. In symbols: $$ \iota_1 \circ \text{pushoutSymmetry}(f, g).\text{hom} = \iota_2. $$

CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom theorem

[HasPushout f g] : pushout.inr _ _ ≫ (pushoutSymmetry f g).hom = pushout.inl _ _

Full source

@[reassoc (attr := simp)]
theorem inr_comp_pushoutSymmetry_hom [HasPushout f g] :
    pushout.inrpushout.inr _ _ ≫ (pushoutSymmetry f g).hom = pushout.inl _ _ :=
  (colimit.isColimit (span f g)).comp_coconePointUniqueUpToIso_hom
    (PushoutCocone.flipIsColimit (pushoutIsPushout g f)) _

Compatibility of right inclusion with pushout symmetry isomorphism

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ for which a pushout exists, the composition of the right inclusion morphism $\iota_2 \colon Z \to \text{pushout}(f, g)$ with the isomorphism $\text{pushout}(f, g) \cong \text{pushout}(g, f)$ equals the left inclusion morphism $\iota_1 \colon Y \to \text{pushout}(g, f)$. In symbols: $$ \iota_2 \circ \varphi = \iota_1 $$ where $\varphi$ is the isomorphism $\text{pushout}(f, g) \cong \text{pushout}(g, f)$.

CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv theorem

[HasPushout f g] : pushout.inl _ _ ≫ (pushoutSymmetry f g).inv = pushout.inr _ _

Full source

@[reassoc (attr := simp)]
theorem inl_comp_pushoutSymmetry_inv [HasPushout f g] :
    pushout.inlpushout.inl _ _ ≫ (pushoutSymmetry f g).inv = pushout.inr _ _ := by simp [Iso.comp_inv_eq]

Compatibility of pushout symmetry inverse with left inclusion

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ for which a pushout exists, the composition of the left inclusion morphism $\iota_1 \colon Y \to \text{pushout}(f, g)$ with the inverse of the symmetry isomorphism $\text{pushoutSymmetry}(f, g)^{-1} \colon \text{pushout}(f, g) \to \text{pushout}(g, f)$ equals the right inclusion morphism $\iota_2 \colon Z \to \text{pushout}(g, f)$. In symbols: $$ \iota_1 \circ \varphi^{-1} = \iota_2 $$ where $\varphi$ is the isomorphism $\text{pushout}(f, g) \cong \text{pushout}(g, f)$.

CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv theorem

[HasPushout f g] : pushout.inr _ _ ≫ (pushoutSymmetry f g).inv = pushout.inl _ _

Full source

@[reassoc (attr := simp)]
theorem inr_comp_pushoutSymmetry_inv [HasPushout f g] :
    pushout.inrpushout.inr _ _ ≫ (pushoutSymmetry f g).inv = pushout.inl _ _ := by simp [Iso.comp_inv_eq]

Compatibility of right inclusion with inverse pushout symmetry isomorphism

Informal description

Given a category $\mathcal{C}$ and morphisms $f \colon X \to Y$ and $g \colon X \to Z$ in $\mathcal{C}$ for which a pushout exists, the composition of the right inclusion morphism $\iota_2 \colon Z \to \text{pushout}(f, g)$ with the inverse of the symmetry isomorphism $\text{pushoutSymmetry}(f, g)^{-1} \colon \text{pushout}(f, g) \to \text{pushout}(g, f)$ equals the left inclusion morphism $\iota_1 \colon Y \to \text{pushout}(g, f)$. In symbols: $$ \iota_2 \circ \text{pushoutSymmetry}(f, g)^{-1} = \iota_1. $$

CategoryTheory.Limits.HasPullbacks abbrev

Full source

/-- `HasPullbacks` represents a choice of pullback for every pair of morphisms. -/
@[stacks 001W]
abbrev HasPullbacks :=
  HasLimitsOfShape WalkingCospan C

Existence of Pullbacks in a Category

Informal description

A category $\mathcal{C}$ has pullbacks if for every pair of morphisms $f: X \to Z$ and $g: Y \to Z$ in $\mathcal{C}$, there exists a pullback (fiber product) of $f$ and $g$. This means that $\mathcal{C}$ has all limits of shape `WalkingCospan`, the indexing category for pullback diagrams.

CategoryTheory.Limits.HasPushouts abbrev

Full source

/-- `HasPushouts` represents a choice of pushout for every pair of morphisms -/
abbrev HasPushouts :=
  HasColimitsOfShape WalkingSpan C

Existence of Pushouts in a Category

Informal description

A category $\mathcal{C}$ has pushouts if for every pair of morphisms $f: X \to Y$ and $g: X \to Z$ in $\mathcal{C}$, there exists a pushout object $Y \sqcup_X Z$ fitting into the following commutative diagram: \[ \begin{array}{ccc} X & \xrightarrow{f} & Y \\ g \downarrow & & \downarrow \\ Z & \xrightarrow{} & Y \sqcup_X Z \end{array} \] This means that $\mathcal{C}$ has all colimits of shape `WalkingSpan`, the index category for pushout diagrams.

CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan theorem

[∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}, HasLimit (cospan f g)] : HasPullbacks C

Full source

/-- If `C` has all limits of diagrams `cospan f g`, then it has all pullbacks -/
theorem hasPullbacks_of_hasLimit_cospan
    [∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}, HasLimit (cospan f g)] : HasPullbacks C :=
  { has_limit := fun F => hasLimit_of_iso (diagramIsoCospan F).symm }

Existence of Pullbacks from Limits of Cospan Diagrams

Informal description

If a category $\mathcal{C}$ has all limits of cospan diagrams (i.e., for every pair of morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in $\mathcal{C}$, the limit of the diagram $X \xrightarrow{f} Z \xleftarrow{g} Y$ exists), then $\mathcal{C}$ has all pullbacks.

CategoryTheory.Limits.hasPushouts_of_hasColimit_span theorem

[∀ {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}, HasColimit (span f g)] : HasPushouts C

Full source

/-- If `C` has all colimits of diagrams `span f g`, then it has all pushouts -/
theorem hasPushouts_of_hasColimit_span
    [∀ {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}, HasColimit (span f g)] : HasPushouts C :=
  { has_colimit := fun F => hasColimit_of_iso (diagramIsoSpan F) }

Existence of Pushouts from Span Colimits

Informal description

If a category $\mathcal{C}$ has colimits for all diagrams of the form $\mathrm{span}\, f\, g$ (i.e., for every pair of morphisms $f: X \to Y$ and $g: X \to Z$ in $\mathcal{C}$), then $\mathcal{C}$ has all pushouts.

CategoryTheory.Limits.walkingSpanOpEquiv definition

: WalkingSpanᵒᵖ ≌ WalkingCospan

Full source

/-- The duality equivalence `WalkingSpanᵒᵖ ≌ WalkingCospan` -/
@[simps!]
def walkingSpanOpEquiv : WalkingSpanWalkingSpanᵒᵖWalkingSpanᵒᵖ ≌ WalkingCospan :=
  widePushoutShapeOpEquiv _

Duality equivalence between opposite walking span and walking cospan categories

Informal description

The duality equivalence between the opposite of the walking span category and the walking cospan category, establishing a natural isomorphism between these two indexing categories used for pushout and pullback diagrams respectively.

CategoryTheory.Limits.walkingCospanOpEquiv definition

: WalkingCospanᵒᵖ ≌ WalkingSpan

Full source

/-- The duality equivalence `WalkingCospanᵒᵖ ≌ WalkingSpan` -/
@[simps!]
def walkingCospanOpEquiv : WalkingCospanWalkingCospanᵒᵖWalkingCospanᵒᵖ ≌ WalkingSpan :=
  widePullbackShapeOpEquiv _

Duality equivalence between opposite pullback and pushout indexing categories

Informal description

The duality equivalence between the opposite of the indexing category for pullback diagrams (`WalkingCospanᵒᵖ`) and the indexing category for pushout diagrams (`WalkingSpan`). This equivalence establishes that the opposite of a pullback diagram is naturally equivalent to a pushout diagram, and vice versa.

CategoryTheory.Limits.hasPullbacks_of_hasWidePullbacks instance

(D : Type u) [Category.{v} D] [HasWidePullbacks.{w} D] : HasPullbacks.{v, u} D

Full source

/-- Having wide pullback at any universe level implies having binary pullbacks. -/
instance (priority := 100) hasPullbacks_of_hasWidePullbacks (D : Type u) [Category.{v} D]
    [HasWidePullbacks.{w} D] : HasPullbacks.{v,u} D :=
  hasWidePullbacks_shrink WalkingPair

Existence of Binary Pullbacks from Wide Pullbacks

Informal description

For any category $\mathcal{D}$ that has all wide pullbacks (i.e., limits of diagrams with multiple morphisms to a common target), $\mathcal{D}$ also has all binary pullbacks (i.e., limits of diagrams with two morphisms to a common target).

CategoryTheory.Limits.hasPushouts_of_hasWidePushouts instance

(D : Type u) [Category.{v} D] [HasWidePushouts.{w} D] : HasPushouts.{v, u} D

Full source

/-- Having wide pushout at any universe level implies having binary pushouts. -/
instance (priority := 100) hasPushouts_of_hasWidePushouts (D : Type u) [Category.{v} D]
    [HasWidePushouts.{w} D] : HasPushouts.{v,u} D :=
  hasWidePushouts_shrink WalkingPair

Existence of Binary Pushouts from Wide Pushouts

Informal description

For any category $\mathcal{D}$ that has all wide pushouts (i.e., colimits of diagrams with multiple morphisms from a common source), $\mathcal{D}$ also has all binary pushouts (i.e., colimits of diagrams with two morphisms from a common source).

Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Main definitions

Main results & API

References