Theorems · Theorem · category theory

CategoryTheory.IsPullback.paste_twist_right

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z S : C} {f : X ⟶ S} {g : Y ⟶ S} {i : Z ⟶ S} {Pfg : C}
  {fstfg : Pfg ⟶ X} {sndfg : Pfg ⟶ Y},
  CategoryTheory.IsPullback fstfg sndfg f g →
    ∀ {Pfi : C} {fstfi : Pfi ⟶ X} {sndfi : Pfi ⟶ Z},
      CategoryTheory.IsPullback fstfi sndfi f i →
        ∀ {R : C} (rY : R ⟶ Y) (rZ : R ⟶ Z),
          CategoryTheory.CategoryStruct.comp rY g = CategoryTheory.CategoryStruct.comp rZ i →
            ∀ {Psndfgr : C} (fstsndfgr : Psndfgr ⟶ Pfg) (sndsndfgr : Psndfgr ⟶ R),
              CategoryTheory.IsPullback fstsndfgr sndsndfgr sndfg rY →
                ∀ {t : Psndfgr ⟶ Pfi},
                  CategoryTheory.CategoryStruct.comp t fstfi = CategoryTheory.CategoryStruct.comp fstsndfgr fstfg →
                    CategoryTheory.CategoryStruct.comp t sndfi = CategoryTheory.CategoryStruct.comp sndsndfgr rZ →
                      CategoryTheory.IsPullback t sndsndfgr sndfi rZ

The main objects in this lemma fit in the following commutative diagram: `` Pfg -> X < - Pfi | | | | f | ↓ ↓ ↓ Y g --> S <-- i Z \ / -- -- \ / -- R -- ` Suppose the two squares are cartesian, then Pfg ×[Y] R is the pullback of Pfi ⟶ Z and R ⟶ Z`.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Cited by

1 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category