Theorems · Theorem · category theory

CategoryTheory.IsPushout.of_iso

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P},
  CategoryTheory.IsPushout f g inl inr →
    ∀ {Z' X' Y' P' : C} {f' : Z' ⟶ X'} {g' : Z' ⟶ Y'} {inl' : X' ⟶ P'} {inr' : Y' ⟶ P'} (e₁ : Z ≅ Z') (e₂ : X ≅ X')
      (e₃ : Y ≅ Y') (e₄ : P ≅ P'),
      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.CategoryStruct.comp inl e₄.hom = CategoryTheory.CategoryStruct.comp e₂.hom inl' →
            CategoryTheory.CategoryStruct.comp inr e₄.hom = CategoryTheory.CategoryStruct.comp e₃.hom inr' →
              CategoryTheory.IsPushout f' g' inl' inr'

Defined in

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

Cited by

10 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category