Theorems · Theorem · category theory

CategoryTheory.IsPullback.of_iso

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g →
    ∀ {P' X' Y' Z' : C} {fst' : P' ⟶ X'} {snd' : P' ⟶ Y'} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (e₁ : P ≅ P') (e₂ : X ≅ X')
      (e₃ : Y ≅ Y') (e₄ : Z ≅ Z'),
      CategoryTheory.CategoryStruct.comp fst e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom fst' →
        CategoryTheory.CategoryStruct.comp snd e₃.hom = CategoryTheory.CategoryStruct.comp e₁.hom snd' →
          CategoryTheory.CategoryStruct.comp f e₄.hom = CategoryTheory.CategoryStruct.comp e₂.hom f' →
            CategoryTheory.CategoryStruct.comp g e₄.hom = CategoryTheory.CategoryStruct.comp e₃.hom g' →
              CategoryTheory.IsPullback fst' snd' f' g'

Defined in

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

Cited by

17 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category