Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

CategoryTheory.Limits.PullbackCone abbrev

(f : X ⟶ Z) (g : Y ⟶ Z)

Full source

/-- A pullback cone is just a cone on the cospan formed by two morphisms `f : X ⟶ Z` and
    `g : Y ⟶ Z`. -/
abbrev PullbackCone (f : X ⟶ Z) (g : Y ⟶ Z) :=
  Cone (cospan f g)

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

Informal description

Given morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, a *pullback cone* for $f$ and $g$ consists of: - An object $P$ (called the *cone point*) - 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.PullbackCone.fst abbrev

(t : PullbackCone f g) : t.pt ⟶ X

Full source

/-- The first projection of a pullback cone. -/
abbrev fst (t : PullbackCone f g) : t.pt ⟶ X :=
  t.π.app WalkingCospan.left

First Projection of Pullback Cone

Informal description

Given a pullback cone $t$ for morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, the first projection morphism $\pi_1 \colon t.pt \to X$ satisfies the commutative diagram: ``` t.pt --π₂--> Y | | π₁ g | | v v X --f--> Z ```

CategoryTheory.Limits.PullbackCone.snd abbrev

(t : PullbackCone f g) : t.pt ⟶ Y

Full source

/-- The second projection of a pullback cone. -/
abbrev snd (t : PullbackCone f g) : t.pt ⟶ Y :=
  t.π.app WalkingCospan.right

Second Projection of Pullback Cone

Informal description

Given a pullback cone $t$ for morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, the second projection morphism $\pi_2 \colon t.pt \to Y$ satisfies the commutative diagram: ``` t.pt --π₂--> Y | | π₁ g | | v v X --f--> Z ```

CategoryTheory.Limits.PullbackCone.π_app_left theorem

(c : PullbackCone f g) : c.π.app WalkingCospan.left = c.fst

Full source

@[simp]
theorem π_app_left (c : PullbackCone f g) : c.π.app WalkingCospan.left = c.fst := rfl

Natural Transformation at Left Object Equals First Projection in Pullback Cone

Informal description

For any pullback cone $c$ of morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, the natural transformation $\pi$ evaluated at the left object of the walking cospan indexing category equals the first projection morphism of the cone, i.e., $\pi(\text{left}) = \pi_1$.

CategoryTheory.Limits.PullbackCone.π_app_right theorem

(c : PullbackCone f g) : c.π.app WalkingCospan.right = c.snd

Full source

@[simp]
theorem π_app_right (c : PullbackCone f g) : c.π.app WalkingCospan.right = c.snd := rfl

Naturality condition for pullback cone at right object: $c.\pi_{\mathrm{right}} = c.\mathrm{snd}$

Informal description

For any pullback cone $c$ of morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, the component of the natural transformation $c.\pi$ at the right object of the walking cospan indexing category equals the second projection morphism $c.\mathrm{snd} \colon c.\mathrm{pt} \to Y$.

CategoryTheory.Limits.PullbackCone.condition_one theorem

(t : PullbackCone f g) : t.π.app WalkingCospan.one = t.fst ≫ f

Full source

@[simp]
theorem condition_one (t : PullbackCone f g) : t.π.app WalkingCospan.one = t.fst ≫ f := by
  have w := t.π.naturality WalkingCospan.Hom.inl
  dsimp at w; simpa using w

Commutativity condition for pullback cone at central object

Informal description

For any pullback cone $t$ of morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, the morphism $t.\pi$ evaluated at the central object of the walking cospan category equals the composition $t.\pi_1 \circ f$, where $\pi_1 \colon t.pt \to X$ is the first projection of the cone.

CategoryTheory.Limits.PullbackCone.mk definition

{W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) : PullbackCone f g

Full source

/-- A pullback cone on `f` and `g` is determined by morphisms `fst : W ⟶ X` and `snd : W ⟶ Y`
    such that `fst ≫ f = snd ≫ g`. -/
@[simps]
def mk {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) : PullbackCone f g where
  pt := W
  π := { app := fun j => Option.casesOn j (fst ≫ f) fun j' => WalkingPair.casesOn j' fst snd
         naturality := by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) j <;> cases j <;> dsimp <;> simp [eq] }

Pullback cone constructor

Informal description

Given morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, the constructor `PullbackCone.mk` builds a pullback cone consisting of: - An object $W$ (the cone point) - Morphisms $\pi_1 \colon W \to X$ and $\pi_2 \colon W \to Y$ (called `fst` and `snd` respectively) - A proof that the diagram commutes: $\pi_1 \circ f = \pi_2 \circ g$ This constructs a cone over the cospan diagram formed by $f$ and $g$.

CategoryTheory.Limits.PullbackCone.mk_π_app_left theorem

{W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) : (mk fst snd eq).π.app WalkingCospan.left = fst

Full source

@[simp]
theorem mk_π_app_left {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) :
    (mk fst snd eq).π.app WalkingCospan.left = fst := rfl

Left Projection of Constructed Pullback Cone Equals First Morphism

Informal description

Given a pullback cone constructed via `PullbackCone.mk` with morphisms $fst \colon W \to X$ and $snd \colon W \to Y$ satisfying $fst \circ f = snd \circ g$, the projection morphism from the cone point $W$ to the left object $X$ (via the left leg of the cospan) is equal to $fst$.

CategoryTheory.Limits.PullbackCone.mk_π_app_right theorem

{W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) : (mk fst snd eq).π.app WalkingCospan.right = snd

Full source

@[simp]
theorem mk_π_app_right {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) :
    (mk fst snd eq).π.app WalkingCospan.right = snd := rfl

Right component of pullback cone natural transformation equals second projection

Informal description

Given objects $X, Y, Z$ and morphisms $f \colon X \to Z$, $g \colon Y \to Z$ in a category $\mathcal{C}$, for any object $W$ with morphisms $\pi_1 \colon W \to X$ and $\pi_2 \colon W \to Y$ satisfying $\pi_1 \circ f = \pi_2 \circ g$, the component of the pullback cone's natural transformation at the right object of the walking cospan diagram equals $\pi_2$. In symbols: If $t = \text{PullbackCone.mk}(\pi_1, \pi_2, \text{eq})$, then $t.\pi(\text{right}) = \pi_2$.

CategoryTheory.Limits.PullbackCone.mk_π_app_one theorem

 {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) : (mk fst snd eq).π.app WalkingCospan.one = fst ≫ f

Full source

@[simp]
theorem mk_π_app_one {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) :
    (mk fst snd eq).π.app WalkingCospan.one = fst ≫ f := rfl

Component of Pullback Cone at Central Object Equals Composition

Informal description

Given objects $X, Y, Z$ and morphisms $f \colon X \to Z$, $g \colon Y \to Z$ in a category $\mathcal{C}$, for any object $W$ with morphisms $\pi_1 \colon W \to X$ and $\pi_2 \colon W \to Y$ satisfying $\pi_1 \circ f = \pi_2 \circ g$, the component of the pullback cone's natural transformation at the central object of the walking cospan diagram equals $\pi_1 \circ f$.

CategoryTheory.Limits.PullbackCone.mk_fst theorem

{W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) : (mk fst snd eq).fst = fst

Full source

@[simp]
theorem mk_fst {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) :
    (mk fst snd eq).fst = fst := rfl

First Projection of Constructed Pullback Cone Equals Given Morphism

Informal description

Given objects $X, Y, Z$ in a category $\mathcal{C}$ and morphisms $f \colon X \to Z$, $g \colon Y \to Z$, for any object $W$ and morphisms $\pi_1 \colon W \to X$, $\pi_2 \colon W \to Y$ satisfying $\pi_1 \circ f = \pi_2 \circ g$, the first projection of the pullback cone constructed via `PullbackCone.mk` equals $\pi_1$. In other words, $(\text{mk } \pi_1 \pi_2 \text{ eq}).\text{fst} = \pi_1$.

CategoryTheory.Limits.PullbackCone.mk_snd theorem

{W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) : (mk fst snd eq).snd = snd

Full source

@[simp]
theorem mk_snd {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g) :
    (mk fst snd eq).snd = snd := rfl

Second Projection of Constructed Pullback Cone Equals Given Morphism

Informal description

Given morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, and morphisms $\pi_1 \colon W \to X$ and $\pi_2 \colon W \to Y$ such that $\pi_1 \circ f = \pi_2 \circ g$, the second projection $\pi_2$ of the pullback cone constructed via `PullbackCone.mk` equals the given morphism $\pi_2$.

CategoryTheory.Limits.PullbackCone.condition theorem

(t : PullbackCone f g) : fst t ≫ f = snd t ≫ g

Full source

@[reassoc]
theorem condition (t : PullbackCone f g) : fstfst t ≫ f = sndsnd t ≫ g :=
  (t.w inl).trans (t.w inr).symm

Commutativity Condition for Pullback Cone Projections

Informal description

For any pullback cone $t$ of morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, the first projection $\pi_1 \colon t.pt \to X$ and the second projection $\pi_2 \colon t.pt \to Y$ satisfy the commutativity condition $\pi_1 \circ f = \pi_2 \circ g$.

CategoryTheory.Limits.PullbackCone.equalizer_ext theorem

 (t : PullbackCone f g) {W : C} {k l : W ⟶ t.pt} (h₀ : k ≫ fst t = l ≫ fst t) (h₁ : k ≫ snd t = l ≫ snd t) :
  ∀ j : WalkingCospan, k ≫ t.π.app j = l ≫ t.π.app j

Full source

/-- To check whether two morphisms are equalized by the maps of a pullback cone, it suffices to
check it for `fst t` and `snd t` -/
theorem equalizer_ext (t : PullbackCone f g) {W : C} {k l : W ⟶ t.pt} (h₀ : k ≫ fst t = l ≫ fst t)
    (h₁ : k ≫ snd t = l ≫ snd t) : ∀ j : WalkingCospan, k ≫ t.π.app j = l ≫ t.π.app j
  | somesome WalkingPair.left => h₀
  | somesome WalkingPair.right => h₁
  | none => by rw [← t.w inl, reassoc_of% h₀]

Equalizer Condition for Morphisms into Pullback Cone

Informal description

Given a pullback cone $t$ for morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, and two morphisms $k, l \colon W \to t.pt$ such that: 1. $k \circ \pi_1 = l \circ \pi_1$ (where $\pi_1$ is the first projection of $t$) 2. $k \circ \pi_2 = l \circ \pi_2$ (where $\pi_2$ is the second projection of $t$) then for every object $j$ in the walking cospan indexing category, the compositions $k \circ t.\pi_j$ and $l \circ t.\pi_j$ are equal.

CategoryTheory.Limits.PullbackCone.eta definition

(t : PullbackCone f g) : t ≅ mk t.fst t.snd t.condition

Full source

/-- The natural isomorphism between a pullback cone and the corresponding pullback cone
reconstructed using `PullbackCone.mk`. -/
@[simps!]
def eta (t : PullbackCone f g) : t ≅ mk t.fst t.snd t.condition :=
  PullbackCone.ext (Iso.refl _)

Natural isomorphism between a pullback cone and its reconstructed version

Informal description

For any pullback cone $t$ of morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, there is a natural isomorphism between $t$ and the pullback cone constructed from its projections $\pi_1 \colon t.pt \to X$ and $\pi_2 \colon t.pt \to Y$ with the commutativity condition $\pi_1 \circ f = \pi_2 \circ g$.

CategoryTheory.Limits.PullbackCone.isLimitAux definition

 (t : PullbackCone f g) (lift : ∀ s : PullbackCone f g, s.pt ⟶ t.pt)
  (fac_left : ∀ s : PullbackCone f g, lift s ≫ t.fst = s.fst)
  (fac_right : ∀ s : PullbackCone f g, lift s ≫ t.snd = s.snd)
  (uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt) (_ : ∀ j : WalkingCospan, m ≫ t.π.app j = s.π.app j), m = lift s) :
  IsLimit t

Full source

/-- This is a slightly more convenient method to verify that a pullback cone is a limit cone. It
    only asks for a proof of facts that carry any mathematical content -/
def isLimitAux (t : PullbackCone f g) (lift : ∀ s : PullbackCone f g, s.pt ⟶ t.pt)
    (fac_left : ∀ s : PullbackCone f g, lift s ≫ t.fst = s.fst)
    (fac_right : ∀ s : PullbackCone f g, lift s ≫ t.snd = s.snd)
    (uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt)
      (_ : ∀ j : WalkingCospan, m ≫ t.π.app j = s.π.app j), m = lift s) : IsLimit t :=
  { lift
    fac := fun s j => Option.casesOn j (by
        rw [← s.w inl, ← t.w inl, ← Category.assoc]
        congr
        exact fac_left s)
      fun j' => WalkingPair.casesOn j' (fac_left s) (fac_right s)
    uniq := uniq }

Verification Criterion for Pullback Cone as Limit

Informal description

Given a pullback cone $ t $ for morphisms $ f \colon X \to Z $ and $ g \colon Y \to Z $ in a category $ \mathcal{C} $, to verify that $ t $ is a limit cone, it suffices to provide: 1. A lifting function $ \text{lift} $ that for any other pullback cone $ s $, constructs a morphism $ \text{lift}(s) \colon s.pt \to t.pt $. 2. Proofs that $ \text{lift}(s) $ satisfies: - $ \text{lift}(s) \circ t.fst = s.fst $ (left compatibility) - $ \text{lift}(s) \circ t.snd = s.snd $ (right compatibility) 3. A uniqueness condition: for any morphism $ m \colon s.pt \to t.pt $ that satisfies $ m \circ t.\pi_j = s.\pi_j $ for all $ j $ in the indexing category, we have $ m = \text{lift}(s) $. This auxiliary construction simplifies the verification of limit cones by focusing on the essential properties.

CategoryTheory.Limits.PullbackCone.isLimitAux' definition

 (t : PullbackCone f g)
  (create :
    ∀ s : PullbackCone f g,
      { l // l ≫ t.fst = s.fst ∧ l ≫ t.snd = s.snd ∧ ∀ {m}, m ≫ t.fst = s.fst → m ≫ t.snd = s.snd → m = l }) :
  Limits.IsLimit t

Full source

/-- This is another convenient method to verify that a pullback cone is a limit cone. It
    only asks for a proof of facts that carry any mathematical content, and allows access to the
    same `s` for all parts. -/
def isLimitAux' (t : PullbackCone f g)
    (create :
      ∀ s : PullbackCone f g,
        { l //
          l ≫ t.fst = s.fst ∧
            l ≫ t.snd = s.snd ∧ ∀ {m}, m ≫ t.fst = s.fst → m ≫ t.snd = s.snd → m = l }) :
    Limits.IsLimit t :=
  PullbackCone.isLimitAux t (fun s => (create s).1) (fun s => (create s).2.1)
    (fun s => (create s).2.2.1) fun s _ w =>
    (create s).2.2.2 (w WalkingCospan.left) (w WalkingCospan.right)

Alternative verification criterion for pullback cone as limit

Informal description

Given a pullback cone $ t $ for morphisms $ f \colon X \to Z $ and $ g \colon Y \to Z $ in a category $ \mathcal{C} $, to verify that $ t $ is a limit cone, it suffices to provide a construction that for any other pullback cone $ s $, produces a morphism $ l \colon s.pt \to t.pt $ satisfying: 1. $ l \circ t.fst = s.fst $ 2. $ l \circ t.snd = s.snd $ 3. For any morphism $ m \colon s.pt \to t.pt $, if $ m \circ t.fst = s.fst $ and $ m \circ t.snd = s.snd $, then $ m = l $. This is a convenient alternative method for verifying limit cones, focusing on the essential universal properties while allowing access to the same cone $ s $ throughout the verification.

CategoryTheory.Limits.PullbackCone.IsLimit.mk definition

 {W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (eq : fst ≫ f = snd ≫ g) (lift : ∀ s : PullbackCone f g, s.pt ⟶ W)
  (fac_left : ∀ s : PullbackCone f g, lift s ≫ fst = s.fst) (fac_right : ∀ s : PullbackCone f g, lift s ≫ snd = s.snd)
  (uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ W) (_ : m ≫ fst = s.fst) (_ : m ≫ snd = s.snd), m = lift s) :
  IsLimit (mk fst snd eq)

Full source

/-- This is a more convenient formulation to show that a `PullbackCone` constructed using
`PullbackCone.mk` is a limit cone.
-/
def IsLimit.mk {W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (eq : fst ≫ f = snd ≫ g)
    (lift : ∀ s : PullbackCone f g, s.pt ⟶ W)
    (fac_left : ∀ s : PullbackCone f g, lift s ≫ fst = s.fst)
    (fac_right : ∀ s : PullbackCone f g, lift s ≫ snd = s.snd)
    (uniq :
      ∀ (s : PullbackCone f g) (m : s.pt ⟶ W) (_ : m ≫ fst = s.fst) (_ : m ≫ snd = s.snd),
        m = lift s) :
    IsLimit (mk fst snd eq) :=
  isLimitAux _ lift fac_left fac_right fun s m w =>
    uniq s m (w WalkingCospan.left) (w WalkingCospan.right)

Universal property of pullback cone constructed from compatible morphisms

Informal description

Given morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, to construct a limit pullback cone with vertex $W$ and morphisms $\pi_1 \colon W \to X$ and $\pi_2 \colon W \to Y$ satisfying $\pi_1 \circ f = \pi_2 \circ g$, it suffices to provide: 1. A lifting function that for any other pullback cone $s$ constructs a morphism $\text{lift}(s) \colon s.pt \to W$; 2. Proofs that $\text{lift}(s)$ satisfies: - $\text{lift}(s) \circ \pi_1 = s.\pi_1$ (left compatibility) - $\text{lift}(s) \circ \pi_2 = s.\pi_2$ (right compatibility); 3. A uniqueness condition: for any morphism $m \colon s.pt \to W$ satisfying $m \circ \pi_1 = s.\pi_1$ and $m \circ \pi_2 = s.\pi_2$, we have $m = \text{lift}(s)$. This constructs a limit cone from the given data, verifying the universal property of pullbacks.

CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext theorem

 {t : PullbackCone f g} (ht : IsLimit t) {W : C} {k l : W ⟶ t.pt} (h₀ : k ≫ fst t = l ≫ fst t)
  (h₁ : k ≫ snd t = l ≫ snd t) : k = l

Full source

theorem IsLimit.hom_ext {t : PullbackCone f g} (ht : IsLimit t) {W : C} {k l : W ⟶ t.pt}
    (h₀ : k ≫ fst t = l ≫ fst t) (h₁ : k ≫ snd t = l ≫ snd t) : k = l :=
  ht.hom_ext <| equalizer_ext _ h₀ h₁

Uniqueness of Morphisms into Limit Pullback Cone via Commutativity Conditions

Informal description

Let $t$ be a pullback cone for morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, and suppose $t$ is a limit cone. For any object $W$ in $\mathcal{C}$ and any two morphisms $k, l \colon W \to t.pt$, if both of the following conditions hold: 1. $k \circ \pi_1 = l \circ \pi_1$ (where $\pi_1 \colon t.pt \to X$ is the first projection) 2. $k \circ \pi_2 = l \circ \pi_2$ (where $\pi_2 \colon t.pt \to Y$ is the second projection) then $k = l$.

CategoryTheory.Limits.PullbackCone.IsLimit.lift definition

{t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : h ≫ f = k ≫ g) : W ⟶ t.pt

Full source

/-- If `t` is a limit pullback cone over `f` and `g` and `h : W ⟶ X` and `k : W ⟶ Y` are such that
    `h ≫ f = k ≫ g`, then we get `l : W ⟶ t.pt`, which satisfies `l ≫ fst t = h`
    and `l ≫ snd t = k`, see `IsLimit.lift_fst` and `IsLimit.lift_snd`. -/
def IsLimit.lift {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y)
    (w : h ≫ f = k ≫ g) : W ⟶ t.pt :=
  ht.lift <| PullbackCone.mk _ _ w

Universal property of pullback cone

Informal description

Given a limit pullback cone $t$ for morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, 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 $l \colon W \to t.pt$ satisfying $l \circ \pi_1 = h$ and $l \circ \pi_2 = k$, where $\pi_1$ and $\pi_2$ are the cone morphisms of $t$.

CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst theorem

 {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : h ≫ f = k ≫ g) :
  IsLimit.lift ht h k w ≫ fst t = h

Full source

@[reassoc (attr := simp)]
lemma IsLimit.lift_fst {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y)
    (w : h ≫ f = k ≫ g) : IsLimit.liftIsLimit.lift ht h k w ≫ fst t = h := ht.fac _ _

Universal Property of Pullback: First Projection Condition

Informal description

Given a pullback cone $t$ for morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, if $t$ is a limit cone, then for any object $W$ and morphisms $h \colon W \to X$ and $k \colon W \to Y$ satisfying $h \circ f = k \circ g$, the composition of the induced morphism $l \colon W \to t.pt$ (from the universal property) with the first projection $\pi_1 \colon t.pt \to X$ equals $h$, i.e., $l \circ \pi_1 = h$.

CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd theorem

 {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : h ≫ f = k ≫ g) :
  IsLimit.lift ht h k w ≫ snd t = k

Full source

@[reassoc (attr := simp)]
lemma IsLimit.lift_snd {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y)
    (w : h ≫ f = k ≫ g) : IsLimit.liftIsLimit.lift ht h k w ≫ snd t = k := ht.fac _ _

Second Projection Property of Pullback Cone Universal Morphism

Informal description

Given a limit pullback cone $t$ for morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, 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 $l \colon W \to t.pt$ (from the universal property of $t$) with the second projection $\pi_2 \colon t.pt \to Y$ equals $k$, i.e., $l \circ \pi_2 = k$.

CategoryTheory.Limits.PullbackCone.IsLimit.lift' definition

 {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : h ≫ f = k ≫ g) :
  { l : W ⟶ t.pt // l ≫ fst t = h ∧ l ≫ snd t = k }

Full source

/-- If `t` is a limit pullback cone over `f` and `g` and `h : W ⟶ X` and `k : W ⟶ Y` are such that
`h ≫ f = k ≫ g`, then we have `l : W ⟶ t.pt` satisfying `l ≫ fst t = h` and `l ≫ snd t = k`.
-/
def IsLimit.lift' {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y)
    (w : h ≫ f = k ≫ g) : { l : W ⟶ t.pt // l ≫ fst t = h ∧ l ≫ snd t = k } :=
  ⟨IsLimit.lift ht h k w, by simp⟩

Universal property of limit pullback cone (bundled)

Informal description

Given a limit pullback cone $ t $ for morphisms $ f \colon X \to Z $ and $ g \colon Y \to Z $ in a category $ \mathcal{C} $, 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 t.pt $ satisfying $ l \circ \pi_1 = h $ and $ l \circ \pi_2 = k $, where $ \pi_1 $ and $ \pi_2 $ are the cone morphisms of $ t $. This is a bundled version of the universal property of the limit pullback cone, providing both the morphism $ l $ and the proof that it satisfies the required commutativity conditions.

CategoryTheory.Limits.PullbackCone.mkSelfIsLimit definition

{t : PullbackCone f g} (ht : IsLimit t) : IsLimit (mk t.fst t.snd t.condition)

Full source

/-- The pullback cone reconstructed using `PullbackCone.mk` from a pullback cone that is a
limit, is also a limit. -/
def mkSelfIsLimit {t : PullbackCone f g} (ht : IsLimit t) : IsLimit (mk t.fst t.snd t.condition) :=
  IsLimit.ofIsoLimit ht (eta t)

Limit property of reconstructed pullback cone

Informal description

Given a pullback cone $t$ for morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, if $t$ is a limit cone, then the pullback cone reconstructed from its projections $\pi_1 \colon t.pt \to X$ and $\pi_2 \colon t.pt \to Y$ with the commutativity condition $\pi_1 \circ f = \pi_2 \circ g$ is also a limit cone.

CategoryTheory.Limits.PullbackCone.flip definition

: PullbackCone g f

Full source

/-- The pullback cone obtained by flipping `fst` and `snd`. -/
def flip : PullbackCone g f := PullbackCone.mk _ _ t.condition.symm

Flipped pullback cone

Informal description

Given a pullback cone $t$ for morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, the *flipped pullback cone* is obtained by swapping the projection morphisms $\pi_1$ and $\pi_2$ of $t$, resulting in a new pullback cone for $g$ and $f$ with the same cone point and the commutative condition $\pi_2 \circ g = \pi_1 \circ f$.

CategoryTheory.Limits.PullbackCone.flip_pt theorem

: t.flip.pt = t.pt

Full source

@[simp] lemma flip_pt : t.flip.pt = t.pt := rfl

Cone Point Invariance Under Pullback Cone Flip

Informal description

For any pullback cone $t$ of morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, the cone point of the flipped pullback cone $t.\mathrm{flip}$ is equal to the original cone point $t.\mathrm{pt}$.

CategoryTheory.Limits.PullbackCone.flip_fst theorem

: t.flip.fst = t.snd

Full source

@[simp] lemma flip_fst : t.flip.fst = t.snd := rfl

First Projection of Flipped Pullback Cone Equals Second Projection

Informal description

Given a pullback cone $t$ for morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, the first projection morphism of the flipped pullback cone $t.\text{flip}$ is equal to the second projection morphism of $t$, i.e., $\pi_1^{t.\text{flip}} = \pi_2^t$.

CategoryTheory.Limits.PullbackCone.flip_snd theorem

: t.flip.snd = t.fst

Full source

@[simp] lemma flip_snd : t.flip.snd = t.fst := rfl

Second Projection of Flipped Pullback Cone Equals First Projection

Informal description

Given a pullback cone $t$ for morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, the second projection morphism of the flipped pullback cone $t.\mathrm{flip}$ is equal to the first projection morphism of $t$, i.e., $\pi_2^{t.\mathrm{flip}} = \pi_1^t$.

CategoryTheory.Limits.PullbackCone.flipFlipIso definition

: t.flip.flip ≅ t

Full source

/-- Flipping a pullback cone twice gives an isomorphic cone. -/
def flipFlipIso : t.flip.flip ≅ t := PullbackCone.ext (Iso.refl _) (by simp) (by simp)

Double flip isomorphism of a pullback cone

Informal description

The isomorphism between a pullback cone $t$ and its double flip $t.\mathrm{flip}.\mathrm{flip}$, where the underlying morphism is the identity isomorphism on the cone point, and the projections satisfy $\pi_1^{t.\mathrm{flip}.\mathrm{flip}} = \pi_1^t$ and $\pi_2^{t.\mathrm{flip}.\mathrm{flip}} = \pi_2^t$.

CategoryTheory.Limits.PullbackCone.flipIsLimit definition

(ht : IsLimit t) : IsLimit t.flip

Full source

/-- The flip of a pullback square is a pullback square. -/
def flipIsLimit (ht : IsLimit t) : IsLimit t.flip :=
  IsLimit.mk _ (fun s => ht.lift s.flip) (by simp) (by simp) (fun s m h₁ h₂ => by
    apply IsLimit.hom_ext ht <;> simp [h₁, h₂])

Flipped pullback cone is limit when original is limit

Informal description

Given a pullback cone $t$ for morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, if $t$ is a limit cone, then the flipped pullback cone $t.\mathrm{flip}$ (obtained by swapping the projection morphisms) is also a limit cone.

CategoryTheory.Limits.PullbackCone.isLimitOfFlip definition

(ht : IsLimit t.flip) : IsLimit t

Full source

/-- A square is a pullback square if its flip is. -/
def isLimitOfFlip (ht : IsLimit t.flip) : IsLimit t :=
  IsLimit.ofIsoLimit (flipIsLimit ht) t.flipFlipIso

Pullback cone is limit when its flip is limit

Informal description

Given a pullback cone $t$ for morphisms $f \colon X \to Z$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, if the flipped pullback cone $t.\mathrm{flip}$ (obtained by swapping the projection morphisms) is a limit cone, then $t$ itself is also a limit cone.

CategoryTheory.Limits.Cone.ofPullbackCone definition

{F : WalkingCospan ⥤ C} (t : PullbackCone (F.map inl) (F.map inr)) : Cone F

Full source

/-- This is a helper construction that can be useful when verifying that a category has all
    pullbacks. Given `F : WalkingCospan ⥤ C`, which is really the same as
    `cospan (F.map inl) (F.map inr)`, and a pullback cone on `F.map inl` and `F.map inr`, we
    get a cone on `F`.

    If you're thinking about using this, have a look at `hasPullbacks_of_hasLimit_cospan`,
    which you may find to be an easier way of achieving your goal. -/
@[simps]
def Cone.ofPullbackCone {F : WalkingCospanWalkingCospan ⥤ C} (t : PullbackCone (F.map inl) (F.map inr)) :
    Cone F where
  pt := t.pt
  π := t.π ≫ (diagramIsoCospan F).inv

Cone construction from a pullback cone

Informal description

Given a functor $F \colon \mathrm{WalkingCospan} \to \mathcal{C}$ and a pullback cone $t$ for the morphisms $F(\mathrm{inl})$ and $F(\mathrm{inr})$, this constructs a cone over $F$ with: - The same cone point $t.\mathrm{pt}$ as the pullback cone - A natural transformation whose components are given by composing $t.\pi$ with the inverse of the natural isomorphism between $F$ and its associated cospan diagram.

CategoryTheory.Limits.PullbackCone.ofCone definition

{F : WalkingCospan ⥤ C} (t : Cone F) : PullbackCone (F.map inl) (F.map inr)

Full source

/-- Given `F : WalkingCospan ⥤ C`, which is really the same as `cospan (F.map inl) (F.map inr)`,
    and a cone on `F`, we get a pullback cone on `F.map inl` and `F.map inr`. -/
@[simps]
def PullbackCone.ofCone {F : WalkingCospanWalkingCospan ⥤ C} (t : Cone F) :
    PullbackCone (F.map inl) (F.map inr) where
  pt := t.pt
  π := t.π ≫ (diagramIsoCospan F).hom

Pullback cone construction from a general cone over a cospan diagram

Informal description

Given a functor $F$ from the walking cospan category to a category $\mathcal{C}$ and a cone $t$ over $F$, this constructs a pullback cone for the morphisms $F(\mathrm{inl})$ and $F(\mathrm{inr})$, where $\mathrm{inl}$ and $\mathrm{inr}$ are the left and right inclusion morphisms in the walking cospan category. The pullback cone consists of: - The same cone point $t.\mathrm{pt}$ as the original cone - Morphisms $\pi_1 := t.\pi(\mathrm{left})$ and $\pi_2 := t.\pi(\mathrm{right})$ making the following diagram commute: ``` t.pt --π₂--> F(right) | | π₁ F(inr) | | v v F(left) --F(inl)--> F(one) ```

CategoryTheory.Limits.PullbackCone.isoMk definition

 {F : WalkingCospan ⥤ C} (t : Cone F) :
  (Cones.postcompose (diagramIsoCospan.{v} _).hom).obj t ≅
    PullbackCone.mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right)
      ((t.π.naturality inl).symm.trans (t.π.naturality inr :))

Full source

/-- A diagram `WalkingCospan ⥤ C` is isomorphic to some `PullbackCone.mk` after
composing with `diagramIsoCospan`. -/
@[simps!]
def PullbackCone.isoMk {F : WalkingCospanWalkingCospan ⥤ C} (t : Cone F) :
    (Cones.postcompose (diagramIsoCospan.{v} _).hom).obj t ≅
      PullbackCone.mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right)
        ((t.π.naturality inl).symm.trans (t.π.naturality inr :)) :=
  Cones.ext (Iso.refl _) <| by
    rintro (_ | (_ | _)) <;>
      · dsimp
        simp

Isomorphism between postcomposed cone and pullback cone construction

Informal description

Given a functor $F \colon \mathrm{WalkingCospan} \to \mathcal{C}$ and a cone $t$ over $F$, there is an isomorphism between: 1. The cone obtained by postcomposing $t$ with the natural isomorphism $\mathrm{diagramIsoCospan}\, F$ 2. The pullback cone constructed from the components $t.\pi(\mathrm{left})$ and $t.\pi(\mathrm{right})$ of the natural transformation $t.\pi$, where the commutativity condition follows from the naturality of $t.\pi$.

CategoryTheory.Limits.PushoutCocone abbrev

(f : X ⟶ Y) (g : X ⟶ Z)

Full source

/-- A pushout cocone is just a cocone on the span formed by two morphisms `f : X ⟶ Y` and
    `g : X ⟶ Z`. -/
abbrev PushoutCocone (f : X ⟶ Y) (g : X ⟶ Z) :=
  Cocone (span f g)

Pushout Cocone Construction

Informal description

Given morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, a pushout cocone consists of: - An object $P$ (called the cocone point) - Morphisms $\iota_1 : Y \to P$ and $\iota_2 : 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.PushoutCocone.inl abbrev

(t : PushoutCocone f g) : Y ⟶ t.pt

Full source

/-- The first inclusion of a pushout cocone. -/
abbrev inl (t : PushoutCocone f g) : Y ⟶ t.pt :=
  t.ι.app WalkingSpan.left

First inclusion morphism of a pushout cocone

Informal description

Given a pushout cocone $t$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, the morphism $\mathrm{inl}_t : Y \to t.\mathrm{pt}$ is the first inclusion map from $Y$ to the cocone point of $t$.

CategoryTheory.Limits.PushoutCocone.inr abbrev

(t : PushoutCocone f g) : Z ⟶ t.pt

Full source

/-- The second inclusion of a pushout cocone. -/
abbrev inr (t : PushoutCocone f g) : Z ⟶ t.pt :=
  t.ι.app WalkingSpan.right

Second inclusion morphism of a pushout cocone

Informal description

Given a pushout cocone $t$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, the morphism $\mathrm{inr}_t : Z \to t.\mathrm{pt}$ is the second inclusion map from $Z$ to the cocone point of $t$.

CategoryTheory.Limits.PushoutCocone.ι_app_left theorem

(c : PushoutCocone f g) : c.ι.app WalkingSpan.left = c.inl

Full source

@[simp]
theorem ι_app_left (c : PushoutCocone f g) : c.ι.app WalkingSpan.left = c.inl := rfl

Naturality condition for left inclusion in pushout cocone

Informal description

For any pushout cocone $c$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, the component of the cocone's natural transformation at the left object of the walking span category equals the first inclusion morphism of the cocone, i.e., $c.\iota(\mathrm{left}) = c.\mathrm{inl}$.

CategoryTheory.Limits.PushoutCocone.ι_app_right theorem

(c : PushoutCocone f g) : c.ι.app WalkingSpan.right = c.inr

Full source

@[simp]
theorem ι_app_right (c : PushoutCocone f g) : c.ι.app WalkingSpan.right = c.inr := rfl

Naturality condition for pushout cocone at right object

Informal description

For any pushout cocone $c$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, the component of the cocone's natural transformation at the right object of the walking span diagram equals the second inclusion morphism $c.\mathrm{inr} : Z \to c.\mathrm{pt}$.

CategoryTheory.Limits.PushoutCocone.condition_zero theorem

(t : PushoutCocone f g) : t.ι.app WalkingSpan.zero = f ≫ t.inl

Full source

@[simp]
theorem condition_zero (t : PushoutCocone f g) : t.ι.app WalkingSpan.zero = f ≫ t.inl := by
  have w := t.ι.naturality WalkingSpan.Hom.fst
  dsimp at w; simpa using w.symm

Commutativity condition at apex for pushout cocone

Informal description

For any pushout cocone $t$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, the morphism $\iota_t$ evaluated at the apex object of the walking span diagram equals the composition $f \circ \mathrm{inl}_t$, where $\mathrm{inl}_t : Y \to t.\mathrm{pt}$ is the first inclusion morphism of the cocone.

CategoryTheory.Limits.PushoutCocone.mk definition

{W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) : PushoutCocone f g

Full source

/-- A pushout cocone on `f` and `g` is determined by morphisms `inl : Y ⟶ W` and `inr : Z ⟶ W` such
    that `f ≫ inl = g ↠ inr`. -/
@[simps]
def mk {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) : PushoutCocone f g where
  pt := W
  ι := { app := fun j => Option.casesOn j (f ≫ inl) fun j' => WalkingPair.casesOn j' inl inr
         naturality := by
          rintro (⟨⟩|⟨⟨⟩⟩) (⟨⟩|⟨⟨⟩⟩) <;> intro f <;> cases f <;> dsimp <;> aesop }

Pushout cocone construction

Informal description

Given objects $X, Y, Z$ and morphisms $f : X \to Y$, $g : X \to Z$ in a category $\mathcal{C}$, the construction `PushoutCocone.mk` creates a pushout cocone with: - A cocone point $W$ - Morphisms $\iota_1 : Y \to W$ (called `inl`) and $\iota_2 : Z \to W$ (called `inr`) - The condition that $f \circ \iota_1 = g \circ \iota_2$ (expressed by the equation `eq`) This forms a commutative diagram: \[ \begin{CD} X @>{f}>> Y \\ @V{g}VV @VV{\iota_1}V \\ Z @>>{\iota_2}> W \end{CD} \]

CategoryTheory.Limits.PushoutCocone.mk_ι_app_left theorem

{W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) : (mk inl inr eq).ι.app WalkingSpan.left = inl

Full source

@[simp]
theorem mk_ι_app_left {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) :
    (mk inl inr eq).ι.app WalkingSpan.left = inl := rfl

Pushout Cocone Left Component Equals Inl Morphism

Informal description

Given objects $X, Y, Z$ and morphisms $f : X \to Y$, $g : X \to Z$ in a category $\mathcal{C}$, for any pushout cocone constructed with cocone point $W$ and morphisms $\iota_1 : Y \to W$ (called `inl`) and $\iota_2 : Z \to W$ (called `inr`) satisfying $f \circ \iota_1 = g \circ \iota_2$, the component of the cocone's natural transformation at the left object of the walking span diagram equals $\iota_1$. In other words, $\iota_{\text{left}} = \iota_1$.

CategoryTheory.Limits.PushoutCocone.mk_ι_app_right theorem

{W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) : (mk inl inr eq).ι.app WalkingSpan.right = inr

Full source

@[simp]
theorem mk_ι_app_right {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) :
    (mk inl inr eq).ι.app WalkingSpan.right = inr := rfl

Pushout cocone natural transformation at right object equals right inclusion

Informal description

Given objects $X, Y, Z$ and morphisms $f : X \to Y$, $g : X \to Z$ in a category $\mathcal{C}$, for any pushout cocone constructed with a cocone point $W$ and morphisms $\iota_1 : Y \to W$ (called `inl`) and $\iota_2 : Z \to W$ (called `inr`) satisfying $f \circ \iota_1 = g \circ \iota_2$, the cocone's natural transformation applied to the right object of the walking span indexing category equals $\iota_2$. In other words, if $t$ is the pushout cocone constructed via `PushoutCocone.mk` with components $\iota_1$ and $\iota_2$, then $t.\iota(\text{right}) = \iota_2$.

CategoryTheory.Limits.PushoutCocone.mk_ι_app_zero theorem

 {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) : (mk inl inr eq).ι.app WalkingSpan.zero = f ≫ inl

Full source

@[simp]
theorem mk_ι_app_zero {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) :
    (mk inl inr eq).ι.app WalkingSpan.zero = f ≫ inl := rfl

Natural transformation at apex in pushout cocone construction equals $f \circ \iota_1$

Informal description

Given objects $X, Y, Z$ and morphisms $f : X \to Y$, $g : X \to Z$ in a category $\mathcal{C}$, for any pushout cocone constructed via `PushoutCocone.mk` with: - A cocone point $W$ - Morphisms $\iota_1 : Y \to W$ (called `inl`) and $\iota_2 : Z \to W$ (called `inr`) - The condition $f \circ \iota_1 = g \circ \iota_2$ (expressed by the equation `eq`) the natural transformation $\iota$ evaluated at the apex object (`WalkingSpan.zero`) of the walking span diagram equals the composition $f \circ \iota_1$ (which also equals $g \circ \iota_2$ by the cocone condition).

CategoryTheory.Limits.PushoutCocone.mk_inl theorem

{W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) : (mk inl inr eq).inl = inl

Full source

@[simp]
theorem mk_inl {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) :
    (mk inl inr eq).inl = inl := rfl

First Inclusion Morphism of Pushout Cocone Construction

Informal description

Given objects $X, Y, Z$ and morphisms $f : X \to Y$, $g : X \to Z$ in a category $\mathcal{C}$, for any object $W$ and morphisms $\iota_1 : Y \to W$ and $\iota_2 : Z \to W$ satisfying $f \circ \iota_1 = g \circ \iota_2$, the first inclusion morphism of the pushout cocone constructed via `PushoutCocone.mk` equals $\iota_1$, i.e., $(\mathrm{mk}\ \iota_1\ \iota_2\ \mathrm{eq}).\mathrm{inl} = \iota_1$.

CategoryTheory.Limits.PushoutCocone.mk_inr theorem

{W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) : (mk inl inr eq).inr = inr

Full source

@[simp]
theorem mk_inr {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr) :
    (mk inl inr eq).inr = inr := rfl

Second Inclusion Morphism of Pushout Cocone Construction

Informal description

Given objects $X, Y, Z$ and morphisms $f : X \to Y$, $g : X \to Z$ in a category $\mathcal{C}$, for any object $W$ and morphisms $\iota_1 : Y \to W$, $\iota_2 : Z \to W$ satisfying $f \circ \iota_1 = g \circ \iota_2$, the second inclusion morphism of the pushout cocone constructed via `PushoutCocone.mk` equals $\iota_2$, i.e., $(\mathrm{mk}\ \iota_1\ \iota_2\ \mathrm{eq}).\mathrm{inr} = \iota_2$.

CategoryTheory.Limits.PushoutCocone.condition theorem

(t : PushoutCocone f g) : f ≫ inl t = g ≫ inr t

Full source

@[reassoc]
theorem condition (t : PushoutCocone f g) : f ≫ inl t = g ≫ inr t :=
  (t.w fst).trans (t.w snd).symm

Commutativity Condition for Pushout Cocone

Informal description

For any pushout cocone $t$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, the diagram \[ \begin{CD} X @>{f}>> Y \\ @V{g}VV @VV{\mathrm{inl}_t}V \\ Z @>>{\mathrm{inr}_t}> t.\mathrm{pt} \end{CD} \] commutes, i.e., $f \circ \mathrm{inl}_t = g \circ \mathrm{inr}_t$.

CategoryTheory.Limits.PushoutCocone.coequalizer_ext theorem

 (t : PushoutCocone f g) {W : C} {k l : t.pt ⟶ W} (h₀ : inl t ≫ k = inl t ≫ l) (h₁ : inr t ≫ k = inr t ≫ l) :
  ∀ j : WalkingSpan, t.ι.app j ≫ k = t.ι.app j ≫ l

Full source

/-- To check whether a morphism is coequalized by the maps of a pushout cocone, it suffices to check
  it for `inl t` and `inr t` -/
theorem coequalizer_ext (t : PushoutCocone f g) {W : C} {k l : t.pt ⟶ W}
    (h₀ : inlinl t ≫ k = inlinl t ≫ l) (h₁ : inrinr t ≫ k = inrinr t ≫ l) :
    ∀ j : WalkingSpan, t.ι.app j ≫ k = t.ι.app j ≫ l
  | somesome WalkingPair.left => h₀
  | somesome WalkingPair.right => h₁
  | none => by rw [← t.w fst, Category.assoc, Category.assoc, h₀]

Morphism Equality Condition for Pushout Cocone via Inclusion Maps

Informal description

Given a pushout cocone $t$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, and two morphisms $k, l : t.\mathrm{pt} \to W$ such that: 1. $\mathrm{inl}_t \circ k = \mathrm{inl}_t \circ l$ 2. $\mathrm{inr}_t \circ k = \mathrm{inr}_t \circ l$ then for every object $j$ in the walking span category, the compositions $t.\iota_j \circ k$ and $t.\iota_j \circ l$ are equal.

CategoryTheory.Limits.PushoutCocone.eta definition

(t : PushoutCocone f g) : t ≅ mk t.inl t.inr t.condition

Full source

/-- The natural isomorphism between a pushout cocone and the corresponding pushout cocone
reconstructed using `PushoutCocone.mk`. -/
@[simps!]
def eta (t : PushoutCocone f g) : t ≅ mk t.inl t.inr t.condition :=
  PushoutCocone.ext (Iso.refl _)

Natural isomorphism between a pushout cocone and its reconstruction

Informal description

For any pushout cocone $t$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, there is a natural isomorphism between $t$ and the pushout cocone reconstructed using its inclusion maps $\mathrm{inl}_t : Y \to t.\mathrm{pt}$ and $\mathrm{inr}_t : Z \to t.\mathrm{pt}$ along with the commutativity condition $f \circ \mathrm{inl}_t = g \circ \mathrm{inr}_t$.

CategoryTheory.Limits.PushoutCocone.isColimitAux definition

 (t : PushoutCocone f g) (desc : ∀ s : PushoutCocone f g, t.pt ⟶ s.pt)
  (fac_left : ∀ s : PushoutCocone f g, t.inl ≫ desc s = s.inl)
  (fac_right : ∀ s : PushoutCocone f g, t.inr ≫ desc s = s.inr)
  (uniq : ∀ (s : PushoutCocone f g) (m : t.pt ⟶ s.pt) (_ : ∀ j : WalkingSpan, t.ι.app j ≫ m = s.ι.app j), m = desc s) :
  IsColimit t

Full source

/-- This is a slightly more convenient method to verify that a pushout cocone is a colimit cocone.
    It only asks for a proof of facts that carry any mathematical content -/
def isColimitAux (t : PushoutCocone f g) (desc : ∀ s : PushoutCocone f g, t.pt ⟶ s.pt)
    (fac_left : ∀ s : PushoutCocone f g, t.inl ≫ desc s = s.inl)
    (fac_right : ∀ s : PushoutCocone f g, t.inr ≫ desc s = s.inr)
    (uniq : ∀ (s : PushoutCocone f g) (m : t.pt ⟶ s.pt)
    (_ : ∀ j : WalkingSpan, t.ι.app j ≫ m = s.ι.app j), m = desc s) : IsColimit t :=
  { desc
    fac := fun s j =>
      Option.casesOn j (by simp [← s.w fst, ← t.w fst, fac_left s]) fun j' =>
        WalkingPair.casesOn j' (fac_left s) (fac_right s)
    uniq := uniq }

Colimit condition for pushout cocones

Informal description

Given a pushout cocone $ t $ constructed from morphisms $ f : X \to Y $ and $ g : X \to Z $ in a category $ \mathcal{C} $, the cocone $ t $ is a colimit cocone if there exists a morphism $ \text{desc}(s) : t.\text{pt} \to s.\text{pt} $ for every pushout cocone $ s $ such that: 1. The left inclusion satisfies $ t.\text{inl} \circ \text{desc}(s) = s.\text{inl} $, 2. The right inclusion satisfies $ t.\text{inr} \circ \text{desc}(s) = s.\text{inr} $, 3. For any morphism $ m : t.\text{pt} \to s.\text{pt} $ that makes the diagram commute for all objects in the walking span, $ m $ must equal $ \text{desc}(s) $.

CategoryTheory.Limits.PushoutCocone.isColimitAux' definition

 (t : PushoutCocone f g)
  (create :
    ∀ s : PushoutCocone f g,
      { l // t.inl ≫ l = s.inl ∧ t.inr ≫ l = s.inr ∧ ∀ {m}, t.inl ≫ m = s.inl → t.inr ≫ m = s.inr → m = l }) :
  IsColimit t

Full source

/-- This is another convenient method to verify that a pushout cocone is a colimit cocone. It
    only asks for a proof of facts that carry any mathematical content, and allows access to the
    same `s` for all parts. -/
def isColimitAux' (t : PushoutCocone f g)
    (create :
      ∀ s : PushoutCocone f g,
        { l //
          t.inl ≫ l = s.inl ∧
            t.inr ≫ l = s.inr ∧ ∀ {m}, t.inl ≫ m = s.inl → t.inr ≫ m = s.inr → m = l }) :
    IsColimit t :=
  isColimitAux t (fun s => (create s).1) (fun s => (create s).2.1) (fun s => (create s).2.2.1)
    fun s _ w => (create s).2.2.2 (w WalkingCospan.left) (w WalkingCospan.right)

Colimit condition for pushout cocones (auxiliary version)

Informal description

Given a pushout cocone $ t $ constructed from morphisms $ f : X \to Y $ and $ g : X \to Z $ in a category $ \mathcal{C} $, the cocone $ t $ is a colimit cocone if for every pushout cocone $ s $, there exists a morphism $ l : t.\text{pt} \to s.\text{pt} $ such that: 1. The left inclusion satisfies $ t.\text{inl} \circ l = s.\text{inl} $, 2. The right inclusion satisfies $ t.\text{inr} \circ l = s.\text{inr} $, 3. Any morphism $ m : t.\text{pt} \to s.\text{pt} $ satisfying $ t.\text{inl} \circ m = s.\text{inl} $ and $ t.\text{inr} \circ m = s.\text{inr} $ must equal $ l $.

CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext theorem

 {t : PushoutCocone f g} (ht : IsColimit t) {W : C} {k l : t.pt ⟶ W} (h₀ : inl t ≫ k = inl t ≫ l)
  (h₁ : inr t ≫ k = inr t ≫ l) : k = l

Full source

theorem IsColimit.hom_ext {t : PushoutCocone f g} (ht : IsColimit t) {W : C} {k l : t.pt ⟶ W}
    (h₀ : inlinl t ≫ k = inlinl t ≫ l) (h₁ : inrinr t ≫ k = inrinr t ≫ l) : k = l :=
  ht.hom_ext <| coequalizer_ext _ h₀ h₁

Uniqueness of Morphisms from Pushout via Commuting Diagrams

Informal description

Let $\mathcal{C}$ be a category, and let $f : X \to Y$ and $g : X \to Z$ be morphisms in $\mathcal{C}$. Given a pushout cocone $t$ of $f$ and $g$ that is a colimit (i.e., $ht : \text{IsColimit } t$), and two morphisms $k, l : t.\text{pt} \to W$ for some object $W$ in $\mathcal{C}$, if both compositions $t.\text{inl} \circ k = t.\text{inl} \circ l$ and $t.\text{inr} \circ k = t.\text{inr} \circ l$ hold, then $k = l$.

CategoryTheory.Limits.PushoutCocone.IsColimit.desc definition

{t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W) (w : f ≫ h = g ≫ k) : t.pt ⟶ W

Full source

/-- If `t` is a colimit pushout cocone over `f` and `g` and `h : Y ⟶ W` and `k : Z ⟶ W` are
    morphisms satisfying `f ≫ h = g ≫ k`, then we have a factorization `l : t.pt ⟶ W` such that
    `inl t ≫ l = h` and `inr t ≫ l = k`, see `IsColimit.inl_desc` and `IsColimit.inr_desc`. -/
def IsColimit.desc {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W)
    (w : f ≫ h = g ≫ k) : t.pt ⟶ W :=
  ht.desc (PushoutCocone.mk _ _ w)

Universal property of pushout cocones

Informal description

Given a pushout cocone $ t $ of morphisms $ f : X \to Y $ and $ g : X \to Z $ in a category $ \mathcal{C} $, if $ t $ is a colimit cocone (i.e., $ ht : \text{IsColimit } t $), then for any object $ W $ and morphisms $ h : Y \to W $ and $ k : Z \to W $ satisfying $ f \circ h = g \circ k $, there exists a unique morphism $ l : t.\text{pt} \to W $ such that $ \text{inl } t \circ l = h $ and $ \text{inr } t \circ l = k $. This morphism $ l $ is called the *descending morphism* induced by the universal property of the pushout.

CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc theorem

 {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W) (w : f ≫ h = g ≫ k) :
  inl t ≫ IsColimit.desc ht h k w = h

Full source

@[reassoc (attr := simp)]
lemma IsColimit.inl_desc {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W)
    (w : f ≫ h = g ≫ k) : inlinl t ≫ IsColimit.desc ht h k w = h :=
  ht.fac _ _

Commutativity of first inclusion in pushout universal property

Informal description

Given a pushout cocone $t$ of morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, if $t$ is a colimit cocone (i.e., $ht : \text{IsColimit } t$), then for any object $W$ and morphisms $h : Y \to W$ and $k : Z \to W$ satisfying $f \circ h = g \circ k$, the composition of the first inclusion map $\iota_1 : Y \to t.\text{pt}$ with the descending morphism $l : t.\text{pt} \to W$ equals $h$, i.e., $\iota_1 \circ l = h$.

CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc theorem

 {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W) (w : f ≫ h = g ≫ k) :
  inr t ≫ IsColimit.desc ht h k w = k

Full source

@[reassoc (attr := simp)]
lemma IsColimit.inr_desc {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W)
    (w : f ≫ h = g ≫ k) : inrinr t ≫ IsColimit.desc ht h k w = k :=
  ht.fac _ _

Commutativity of Second Inclusion in Pushout Universal Property

Informal description

Given a pushout cocone $t$ of morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, if $t$ is a colimit cocone (i.e., $ht : \text{IsColimit } t$), then for any object $W$ and morphisms $h : Y \to W$ and $k : Z \to W$ satisfying $f \circ h = g \circ k$, the composition of the second inclusion morphism $\text{inr}_t : Z \to t.\text{pt}$ with the descending morphism $\text{IsColimit.desc } ht\, h\, k\, w : t.\text{pt} \to W$ equals $k$.

CategoryTheory.Limits.PushoutCocone.IsColimit.desc' definition

 {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W) (w : f ≫ h = g ≫ k) :
  { l : t.pt ⟶ W // inl t ≫ l = h ∧ inr t ≫ l = k }

Full source

/-- If `t` is a colimit pushout cocone over `f` and `g` and `h : Y ⟶ W` and `k : Z ⟶ W` are
    morphisms satisfying `f ≫ h = g ≫ k`, then we have a factorization `l : t.pt ⟶ W` such that
    `inl t ≫ l = h` and `inr t ≫ l = k`. -/
def IsColimit.desc' {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W)
    (w : f ≫ h = g ≫ k) : { l : t.pt ⟶ W // inl t ≫ l = h ∧ inr t ≫ l = k } :=
  ⟨IsColimit.desc ht h k w, by simp⟩

Universal property of pushout cocones (dependent pair version)

Informal description

Given a pushout cocone $ t $ of morphisms $ f : X \to Y $ and $ g : X \to Z $ in a category $ \mathcal{C} $, if $ t $ is a colimit cocone (i.e., $ ht : \text{IsColimit } t $), then for any object $ W $ and morphisms $ h : Y \to W $ and $ k : Z \to W $ satisfying $ f \circ h = g \circ k $, there exists a morphism $ l : t.\text{pt} \to W $ such that $ \text{inl } t \circ l = h $ and $ \text{inr } t \circ l = k $. This morphism $ l $ is constructed as a dependent pair, providing both the morphism and the proof that it satisfies the required commutativity conditions.

CategoryTheory.Limits.PushoutCocone.IsColimit.mk definition

 {W : C} {inl : Y ⟶ W} {inr : Z ⟶ W} (eq : f ≫ inl = g ≫ inr) (desc : ∀ s : PushoutCocone f g, W ⟶ s.pt)
  (fac_left : ∀ s : PushoutCocone f g, inl ≫ desc s = s.inl) (fac_right : ∀ s : PushoutCocone f g, inr ≫ desc s = s.inr)
  (uniq : ∀ (s : PushoutCocone f g) (m : W ⟶ s.pt) (_ : inl ≫ m = s.inl) (_ : inr ≫ m = s.inr), m = desc s) :
  IsColimit (mk inl inr eq)

Full source

/-- This is a more convenient formulation to show that a `PushoutCocone` constructed using
`PushoutCocone.mk` is a colimit cocone.
-/
def IsColimit.mk {W : C} {inl : Y ⟶ W} {inr : Z ⟶ W} (eq : f ≫ inl = g ≫ inr)
    (desc : ∀ s : PushoutCocone f g, W ⟶ s.pt)
    (fac_left : ∀ s : PushoutCocone f g, inl ≫ desc s = s.inl)
    (fac_right : ∀ s : PushoutCocone f g, inr ≫ desc s = s.inr)
    (uniq :
      ∀ (s : PushoutCocone f g) (m : W ⟶ s.pt) (_ : inl ≫ m = s.inl) (_ : inr ≫ m = s.inr),
        m = desc s) :
    IsColimit (mk inl inr eq) :=
  isColimitAux _ desc fac_left fac_right fun s m w =>
    uniq s m (w WalkingCospan.left) (w WalkingCospan.right)

Colimit condition for pushout cocones constructed via `mk`

Informal description

Given morphisms $ f : X \to Y $ and $ g : X \to Z $ in a category $\mathcal{C}$, a pushout cocone with cocone point $ W $ and morphisms $ \iota_1 : Y \to W $ and $ \iota_2 : Z \to W $ satisfying $ f \circ \iota_1 = g \circ \iota_2 $ is a colimit cocone if: 1. For every pushout cocone $ s $, there exists a morphism $ \text{desc}(s) : W \to s.\text{pt} $ such that: - $ \iota_1 \circ \text{desc}(s) = s.\iota_1 $, - $ \iota_2 \circ \text{desc}(s) = s.\iota_2 $. 2. Any morphism $ m : W \to s.\text{pt} $ satisfying $ \iota_1 \circ m = s.\iota_1 $ and $ \iota_2 \circ m = s.\iota_2 $ must equal $ \text{desc}(s) $.

CategoryTheory.Limits.PushoutCocone.mkSelfIsColimit definition

{t : PushoutCocone f g} (ht : IsColimit t) : IsColimit (mk t.inl t.inr t.condition)

Full source

/-- The pushout cocone reconstructed using `PushoutCocone.mk` from a pushout cocone that is a
colimit, is also a colimit. -/
def mkSelfIsColimit {t : PushoutCocone f g} (ht : IsColimit t) :
    IsColimit (mk t.inl t.inr t.condition) :=
  IsColimit.ofIsoColimit ht (eta t)

Colimit property preserved under pushout cocone reconstruction

Informal description

Given a pushout cocone $ t $ constructed from morphisms $ f : X \to Y $ and $ g : X \to Z $ in a category $\mathcal{C}$, if $ t $ is a colimit cocone (i.e., $ ht : \text{IsColimit } t $), then the pushout cocone reconstructed using `PushoutCocone.mk` with the same inclusion maps $ \iota_1 : Y \to t.\text{pt} $ and $ \iota_2 : Z \to t.\text{pt} $ and the commutativity condition $ f \circ \iota_1 = g \circ \iota_2 $ is also a colimit cocone.

CategoryTheory.Limits.PushoutCocone.flip definition

: PushoutCocone g f

Full source

/-- The pushout cocone obtained by flipping `inl` and `inr`. -/
def flip : PushoutCocone g f := PushoutCocone.mk _ _ t.condition.symm

Flipped pushout cocone

Informal description

Given a pushout cocone $t$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, the operation `flip` produces a new pushout cocone where the roles of the inclusion morphisms $\iota_1 : Y \to t.\mathrm{pt}$ and $\iota_2 : Z \to t.\mathrm{pt}$ are swapped, i.e., $\iota_1$ becomes $\iota_2$ and vice versa. This new cocone is constructed for the swapped morphisms $g : X \to Z$ and $f : X \to Y$, and it satisfies the same commutativity condition as the original cocone.

CategoryTheory.Limits.PushoutCocone.flip_pt theorem

: t.flip.pt = t.pt

Full source

@[simp] lemma flip_pt : t.flip.pt = t.pt := rfl

Cocone Point Preservation under Pushout Cocone Flip

Informal description

For any pushout cocone $t$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, the cocone point of the flipped pushout cocone $t.\mathrm{flip}$ is equal to the original cocone point $t.\mathrm{pt}$.

CategoryTheory.Limits.PushoutCocone.flip_inl theorem

: t.flip.inl = t.inr

Full source

@[simp] lemma flip_inl : t.flip.inl = t.inr := rfl

First inclusion of flipped pushout cocone equals second inclusion of original cocone

Informal description

Given a pushout cocone $t$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, the first inclusion morphism of the flipped cocone $t.\mathrm{flip}$ is equal to the second inclusion morphism of the original cocone $t$, i.e., $t.\mathrm{flip}.\mathrm{inl} = t.\mathrm{inr}$.

CategoryTheory.Limits.PushoutCocone.flip_inr theorem

: t.flip.inr = t.inl

Full source

@[simp] lemma flip_inr : t.flip.inr = t.inl := rfl

Equality of inclusion morphisms in flipped pushout cocone: $t.\mathrm{flip}.\mathrm{inr} = t.\mathrm{inl}$

Informal description

Given a pushout cocone $t$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, the second inclusion morphism of the flipped cocone $t.\mathrm{flip}$ is equal to the first inclusion morphism of the original cocone $t$, i.e., $t.\mathrm{flip}.\mathrm{inr} = t.\mathrm{inl}$.

CategoryTheory.Limits.PushoutCocone.flipFlipIso definition

: t.flip.flip ≅ t

Full source

/-- Flipping a pushout cocone twice gives an isomorphic cocone. -/
def flipFlipIso : t.flip.flip ≅ t := PushoutCocone.ext (Iso.refl _) (by simp) (by simp)

Double flip isomorphism for pushout cocones

Informal description

The isomorphism between a pushout cocone $t$ and its double flip $t.\mathrm{flip}.\mathrm{flip}$ is given by the identity isomorphism on the cocone point, with the cocone legs satisfying the obvious equalities.

CategoryTheory.Limits.PushoutCocone.flipIsColimit definition

(ht : IsColimit t) : IsColimit t.flip

Full source

/-- The flip of a pushout square is a pushout square. -/
def flipIsColimit (ht : IsColimit t) : IsColimit t.flip :=
  IsColimit.mk _ (fun s => ht.desc s.flip) (by simp) (by simp) (fun s m h₁ h₂ => by
    apply IsColimit.hom_ext ht <;> simp [h₁, h₂])

Flipped pushout cocone preserves colimit property

Informal description

Given a pushout cocone $t$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, if $t$ is a colimit cocone, then its flipped version $t.\mathrm{flip}$ (where the roles of $Y$ and $Z$ are swapped) is also a colimit cocone.

CategoryTheory.Limits.PushoutCocone.isColimitOfFlip definition

(ht : IsColimit t.flip) : IsColimit t

Full source

/-- A square is a pushout square if its flip is. -/
def isColimitOfFlip (ht : IsColimit t.flip) : IsColimit t :=
  IsColimit.ofIsoColimit (flipIsColimit ht) t.flipFlipIso

Pushout cocone is colimit if its flip is colimit

Informal description

Given a pushout cocone $t$ constructed from morphisms $f : X \to Y$ and $g : X \to Z$ in a category $\mathcal{C}$, if the flipped pushout cocone $t.\mathrm{flip}$ (where the roles of $Y$ and $Z$ are swapped) is a colimit cocone, then the original cocone $t$ is also a colimit cocone.

CategoryTheory.Limits.Cocone.ofPushoutCocone definition

{F : WalkingSpan ⥤ C} (t : PushoutCocone (F.map fst) (F.map snd)) : Cocone F

Full source

/-- This is a helper construction that can be useful when verifying that a category has all
    pushout. Given `F : WalkingSpan ⥤ C`, which is really the same as
    `span (F.map fst) (F.map snd)`, and a pushout cocone on `F.map fst` and `F.map snd`,
    we get a cocone on `F`.

    If you're thinking about using this, have a look at `hasPushouts_of_hasColimit_span`, which
    you may find to be an easier way of achieving your goal. -/
@[simps]
def Cocone.ofPushoutCocone {F : WalkingSpanWalkingSpan ⥤ C} (t : PushoutCocone (F.map fst) (F.map snd)) :
    Cocone F where
  pt := t.pt
  ι := (diagramIsoSpan F).hom ≫ t.ι

Cocone construction from a pushout cocone

Informal description

Given a functor $F$ from the walking span category to a category $\mathcal{C}$ and a pushout cocone $t$ on the morphisms $F(\mathrm{fst})$ and $F(\mathrm{snd})$, this constructs a cocone over $F$ where: - The cocone point is $t.pt$ - The natural transformation is obtained by composing the natural isomorphism $(F \cong \mathrm{span}\, (F(\mathrm{fst}))\, (F(\mathrm{snd})))$ with the pushout cocone's natural transformation $t.\iota$ This cocone makes the appropriate diagrams commute with respect to the original functor $F$.

CategoryTheory.Limits.PushoutCocone.ofCocone definition

{F : WalkingSpan ⥤ C} (t : Cocone F) : PushoutCocone (F.map fst) (F.map snd)

Full source

/-- Given `F : WalkingSpan ⥤ C`, which is really the same as `span (F.map fst) (F.map snd)`,
    and a cocone on `F`, we get a pushout cocone on `F.map fst` and `F.map snd`. -/
@[simps]
def PushoutCocone.ofCocone {F : WalkingSpanWalkingSpan ⥤ C} (t : Cocone F) :
    PushoutCocone (F.map fst) (F.map snd) where
  pt := t.pt
  ι := (diagramIsoSpan F).inv ≫ t.ι

Pushout cocone from a general cocone over a span

Informal description

Given a functor $F$ from the walking span category to a category $\mathcal{C}$ and a cocone $t$ over $F$, this constructs a pushout cocone where: - The cocone point is $t.pt$ - The morphisms are obtained by composing the natural isomorphism $(F \cong \mathrm{span}\, (F(\mathrm{fst}))\, (F(\mathrm{snd})))$ with the cocone's natural transformation $t.\iota$ This pushout cocone has morphisms $F(\mathrm{fst}) \to t.pt$ and $F(\mathrm{snd}) \to t.pt$ making the appropriate diagram commute.

CategoryTheory.Limits.PushoutCocone.isoMk definition

 {F : WalkingSpan ⥤ C} (t : Cocone F) :
  (Cocones.precompose (diagramIsoSpan.{v} _).inv).obj t ≅
    PushoutCocone.mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right)
      ((t.ι.naturality fst).trans (t.ι.naturality snd).symm)

Full source

/-- A diagram `WalkingSpan ⥤ C` is isomorphic to some `PushoutCocone.mk` after composing with
`diagramIsoSpan`. -/
@[simps!]
def PushoutCocone.isoMk {F : WalkingSpanWalkingSpan ⥤ C} (t : Cocone F) :
    (Cocones.precompose (diagramIsoSpan.{v} _).inv).obj t ≅
      PushoutCocone.mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right)
        ((t.ι.naturality fst).trans (t.ι.naturality snd).symm) :=
  Cocones.ext (Iso.refl _) <| by
    rintro (_ | (_ | _)) <;>
      · dsimp
        simp

Isomorphism between precomposed cocone and pushout cocone construction

Informal description

Given a functor $F$ from the walking span category to a category $\mathcal{C}$ and a cocone $t$ over $F$, there is an isomorphism between: 1. The cocone obtained by precomposing $t$ with the inverse of the natural isomorphism $(F \cong \mathrm{span}\, (F(\mathrm{fst}))\, (F(\mathrm{snd})))$ 2. The pushout cocone constructed from the cocone legs $t.\iota$ at the left and right objects of the walking span, with the commutativity condition derived from the naturality of $t.\iota$ with respect to the span morphisms $\mathrm{fst}$ and $\mathrm{snd}$ This isomorphism is witnessed by the identity morphism on the cocone point $t.pt$, and it commutes with the cocone legs at all objects of the walking span category.

Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Main definitions

API

References